WikiDer > Информационная система Скотта

В теория предметной области, филиал математика и Информатика, а Информационная система Скотта это примитивный вид логического дедуктивная система часто используется как альтернативный способ представления Скотт домены.

Определение

А Информационная система Скотта, А, является упорядоченной тройкой ${displaystyle (T, Con, vdash)}$

• ${displaystyle T {mbox {- это набор токенов (основные единицы информации)}}}$
• ${displaystyle Consubseteq {mathcal {P}} _ {f} (T) {mbox {конечные подмножества}} T}$
• ${displaystyle {vdash} substeq (Consetminus lbrace emptyset brace) imes T}$

удовлетворение

1. ${displaystyle {mbox {If}} ain Xin Con {mbox {then}} Xvdash a}$
2. ${displaystyle {mbox {If}} Xvdash Y {mbox {и}} Yvdash a {mbox {, then}} Xvdash a}$
3. ${displaystyle {mbox {If}} Xvdash a {mbox {then}} Xcup {a} in Con}$
4. ${displaystyle forall ain T: {a} in Con}$
5. ${displaystyle {mbox {If}} Xin Con {mbox {and}} X ^ {prime}, substeq X {mbox {then}} X ^ {prime} in Con.}$

Здесь ${displaystyle Xvdash Y}$ средства ${displaystyle forall ain Y, Xvdash a.}$

Примеры

Натуральные числа

Возвращаемое значение частичная рекурсивная функция, которая либо возвращает натуральное число, либо переходит в бесконечную рекурсию, может быть выражена как простая информационная система Скотта следующим образом:

• ${displaystyle T: = mathbb {N}}$
• ${displaystyle Con: = {emptyset} чашка {{n} mid nin mathbb {N}}}$
• ${displaystyle Xvdash aiff ain X.}$

То есть результатом может быть натуральное число, представленное одноэлементным набором ${displaystyle {n}}$, или «бесконечная рекурсия», представленная ${displaystyle emptyset}$.

Конечно, такую ​​же конструкцию можно провести с любым другим набором вместо ${displaystyle mathbb {N}}$.

Исчисление высказываний

В пропозициональное исчисление дает нам очень простую информационную систему Скотта:

• ${displaystyle T: = {phi mid phi {mbox {удовлетворительно}}}}$
• ${displaystyle Con: = {Xin {mathcal {P}} _ {f} (T) mid X {mbox {согласуется}}}}$
• ${displaystyle Xvdash aiff Xvdash a {mbox {в исчислении высказываний}}.}$

Скотт домены

Позволять D быть Скотт домен. Тогда мы можем определить информационную систему следующим образом

• ${displaystyle T: = D ^ {0}}$ набор компактные элементы из ${displaystyle D}$
• ${displaystyle Con: = {Xin {mathcal {P}} _ {f} (T) mid X {mbox {имеет верхнюю границу}}}}$
• ${displaystyle Xvdash diff dsqsubseteq igsqcup X.}$

Позволять ${displaystyle {mathcal {I}}}$ быть отображением, которое выводит нас из области Скотта, D, в указанную выше информационную систему.

Информационные системы и домены Скотта

Учитывая информационную систему, ${displaystyle A = (T, Con, vdash)}$, мы можем построить Скотт домен следующее.

• Определение: ${displaystyle xsubseteq T}$ является точкой тогда и только тогда, когда
  • ${displaystyle {mbox {If}} Xsubseteq _ {f} x {mbox {then}} Xin Con}$
  • ${displaystyle {mbox {If}} Xvdash a {mbox {and}} Xsubseteq _ {f} x {mbox {then}} ain x.}$

Позволять ${displaystyle {mathcal {D}} (A)}$ обозначим множество точек А с упорядочением подмножеств. ${displaystyle {mathcal {D}} (A)}$ будет счетным доменом Скотта, когда Т счетно. В общем, для любого домена Скотта D и информационная система А

• ${displaystyle {mathcal {D}} ({mathcal {I}} (D)) cong D}$
• ${displaystyle {mathcal {I}} ({mathcal {D}} (A)) cong A}$

где второе сравнение дается формулой аппроксимируемые отображения.

Смотрите также

• Скотт домен
• Теория предметной области

Рекомендации

• Глинн Винскель: "Формальная семантика языков программирования: введение", MIT Press, 1993 (глава 12)