Вычислимая топология

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

Топология лямбда-исчисления

Как показали Алан Тьюринг и Алонсо Чёрч , λ-исчисление достаточно сильное, чтобы описать все механически вычислимые функции (см. тезис Чёрча – Тьюринга ). Таким образом, лямбда-исчисление фактически является языком программирования, на основе которого могут быть созданы другие языки. По этой причине при рассмотрении топологии вычислений принято сосредотачиваться на топологии λ-исчисления. Обратите внимание, что это не обязательно полное описание топологии вычислений, поскольку функции, эквивалентные в смысле Чёрча-Тьюринга, все равно могут иметь разные топологии.

Топологией λ λ-исчисления является топология Скотта , и когда оно ограничено непрерывными функциями, -исчисление без типов представляет собой топологическое пространство, зависящее от древовидной топологии . И топологии Скотта, и Древа демонстрируют непрерывность относительно бинарных операторов применения ( f применительно к a = fa ) и абстракции ((λx.t(x))a = t(a)) с модульным отношением эквивалентности, основанным на конгруэнтность . λ-алгебра, описывающая алгебраическую структуру лямбда-исчисления, оказывается расширением комбинаторной алгебры с элементом, введенным для обеспечения абстракции.

без типов λ-исчисление рассматривает функции как правила и не различает функции и объекты, к которым они применяются, то есть λ-исчисление не имеет типов . Побочным продуктом λ-исчисления без типов является эффективная вычислимость, эквивалентная общей рекурсии и машинам Тьюринга . Набор λ-термов можно рассматривать как функциональную топологию, в которую может быть встроено функциональное пространство , то есть λ-отображения внутри пространства X таковы, что λ:X → X. Представленная в ноябре 1969 года нетипизированная теоретико-множественная модель Даны Скотт построила правильную топологию для любой модели λ-исчисления, функциональное пространство которой ограничено непрерывными функциями. Результатом топологии непрерывного λ-исчисления Скотта является функциональное пространство, построенное на семантике программирования, допускающей комбинаторику с фиксированной точкой, такую ​​​​как Y-комбинатор , и типы данных. К 1971 году λ-исчисление было способно определять любые последовательные вычисления и могло быть легко адаптировано к параллельным вычислениям. Сводимость всех вычислений к λ-исчислению позволяет этим λ-топологическим свойствам быть принятыми всеми языками программирования.

Вычислительная алгебра из алгебры λ-исчисления

На основе операторов лямбда-исчисления , применения и абстракции можно разработать алгебру, групповая структура которой использует применение и абстракцию в качестве бинарных операторов. Применение определяется как операция между лямбда-терминами , создающая λ-термин, например, применение λ к лямбда-термину a дает лямбда-термин λa . Абстракция включает неопределенные переменные, обозначая λx.t(x) как функцию, присваивающую переменную a лямбда-терму со значением t(a) посредством операции ((λ xt(x))a = t(a)). Наконец, возникает отношение эквивалентности , которое идентифицирует λ-термины по модулю конвертируемых термов, примером является бета-нормальная форма .

Топология Скотта

Топология Скотта важна для понимания топологической структуры вычислений, выраженной через λ-исчисление. Скотт обнаружил, что после построения функционального пространства с использованием λ-исчисления можно получить пространство Колмогорова , $T_{o}$ топологическое пространство, которое демонстрирует поточечную сходимость , короче говоря, топологию произведения . Именно способность самогомеоморфизма, а также способность вкладывать каждое пространство в такое пространство, обозначенное как непрерывное Скотта , как описано ранее, позволяет топологии Скотта быть применимой к логике и теории рекурсивных функций. Скотт приближается к своему выводу, используя полную решетку , что приводит к топологии, зависящей от структуры решетки. Обобщить теорию Скотта можно с использованием полных частичных порядков . По этой причине более общее понимание вычислительной топологии обеспечивается посредством полных частичных порядков. Мы повторим это еще раз, чтобы ознакомиться с обозначениями, которые будут использоваться при обсуждении топологии Скотта.

Полные частичные заказы определяются следующим образом:

Во-первых, для частично упорядоченного множества D=(D,妻) непустое подмножество X ⊆ D является направленным , если ∀ x,y ∈ X ∃ z ∈ X, где x ⩽ z & y ⩽ z .

D является полным частичным порядком (cpo), если:

⋅ Каждое направленное X ⊆D имеет верхнюю грань и:

∃ нижний элемент ⊥ ∈ D такой, что ∀ x ∈ D ⊥ ≤ x .

Теперь мы можем определить топологию Скотта над cpo (D, ≤).

O ⊆ D открыт , если:

1. если x ∈ O и x ≤ y, то y ∈ O, т. е. O — верхнее множество .
2. для направленного множества X ⊆ D и супремума (X) ∈ O, то X ∩ O ≠ ∅.

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

⋅∅ и D, т. е. пустое множество и все пространство, открыты.

⋅Произвольные объединения открытых множеств открыты:

Доказательство : предположим $U_{i}$ открыт там, где i ∈ I, где I — набор индексов. Определим U = ∪{ $U_{i}$ ; я € I}. Возьмем b как элемент верхнего множества U, поэтому a ⩽ b для некоторого a ∈ U. Должно быть, что a ∈ $U_{i}$ для некоторого i аналогично b ∈ расстроен( $U_{i}$). Следовательно, U также должно быть верхним, поскольку $U_{i}$ € У.

Аналогично, если D — ориентированное множество с супремумом в U, то по предположению sup(D) ∈ $U_{i}$где $U_{i}$открыт. Таким образом, существует a b ∈ D, где b ∈ $U_{i}\cap D\subseteq U\cap D$. Объединение открытых множеств $U_{i}$поэтому открыт.

⋅Открытые множества под пересечением открыты:

Доказательство . Для двух открытых множеств, и V , определим W = U ∩ V. U Если W = ∅, то W открыт. Если непусто, скажем, b ∈ беспорядка(W) (верхнее множество W), то для некоторого a ∈ W , a ⩽ b . Поскольку a ∈ U ∩ V и b — элемент верхнего множества как U так и V , то b ∈ W. ,

Наконец, если D — направленное множество с супремумом в W , то по предположению sup( D ) ∈ $U\cap V$. Итак, существует a ∈ $U\cap D$ и b ∈ $V\cap D$. Поскольку D направлено, существует c ∈ D такой, что $a\leq c,b\leq c$; и поскольку U и V — верхние множества, c ∈ $U\cap V$ также.

Хотя здесь это не показано, но это тот случай, когда карта $f:D\rightarrow D^{'}$ является непрерывным тогда и только тогда, когда f (sup( X )) = sup( f ( X )) для всех направленных X ⊆ D , где f ( X ) = { f ( x ) | x ∈ X } и вторая верхняя грань в $D^{'}$.

Прежде чем мы начнем объяснять, что применение, обычное для λ-исчисления, непрерывно в топологии Скотта, нам потребуется определенное понимание поведения супремумов над непрерывными функциями, а также условий, необходимых для того, чтобы произведение пространств было непрерывным, а именно:

1. С ${f_{i}}_{i}\subseteq [D\rightarrow D^{'}]$ быть ориентированным семейством отображений, тогда $f(x)=\cup _{i}f_{i}(x)$ если они четко определены и непрерывны.
2. Если Ф $\subseteq [D\rightarrow D^{'}]$ направлен и cpo и $[D\rightarrow D^{'}]$ cpo, где sup({ f ( x ) | f ∈ F }).

Теперь мы покажем непрерывность применения . Используя определение приложения следующим образом:

Ап: $[D\rightarrow D^{'}]\times D\rightarrow D^{'}$ где Ap ( ж , Икс ) = Ж ( Икс ).

Ap непрерывен относительно топологии Скотта на произведении ( $[D\rightarrow D^{'}]\times D\rightarrow D^{'}$) :

Доказательство : λx.f(x) = f непрерывно. Пусть h = λ ff(x). Для направленного F $\subseteq [D\rightarrow D^{'}]$

час (суп( F )) = суп( F )( Икс )

знак равно суп ( { ж ( Икс ) | ж ∈ F } )

знак равно суп ( { час ( ж ) | ж ∈ F } )

знак равно суп( час ( F ) )

По определению непрерывности Скотта h было показано непрерывным. Все, что теперь требуется доказать, это то, что приложение является непрерывным, когда его отдельные аргументы непрерывны, т.е. $[D\rightarrow D^{'}]$и $D\rightarrow D^{'}$непрерывны, в нашем случае f и h .

Теперь абстрагируем наш аргумент, чтобы показать $f:D\times D^{'}\rightarrow D^{''}$ с $g=\lambda x.f(x,x_{0})$ и $d=\lambda x^{'}.f(x_{0},x^{'})$ в качестве аргументов в пользу D и $D^{'}$ соответственно, то для направленного X ⊆ D

$g(\sup(X))=f(\sup(X),x_{0}^{'}))$

= f( суп( (x, $x_{0}^{'}$) | х € X} ))

(поскольку f непрерывна и {(x, $x_{0}^{'}$) | x ∈ X}) направлен):

= суп( {f(x, $x_{0}^{'}$) | х € X})

= суп(г(Х))

поэтому g непрерывен. Тот же процесс можно использовать, чтобы показать, что d непрерывен.

Теперь было показано, что приложение является непрерывным в топологии Скотта.

Чтобы продемонстрировать, что топология Скотта подходит для λ-исчисления, необходимо доказать, что абстракция остается непрерывной в топологии Скотта. После завершения будет показано, что математическая основа λ-исчисления представляет собой четко определенную и подходящую функциональную парадигму-кандидата для топологии Скотта.

С $f\in [D\times D^{'}\rightarrow D^{''}]$ мы определяем ${\check {f}}$ (x) =λ y ∈ $D^{'}$f(x,y)Покажем:

(я) ${\check {f}}$ является непрерывным, то есть ${\check {f}}$ ∈ $[D\rightarrow [D^{'}\rightarrow D^{''}]$

(ii) л $f.{\check {f}}:[D\times D^{'}\rightarrow D^{''}]\rightarrow [D\rightarrow [D^{'}\rightarrow D^{''}]$ является непрерывным.

Доказательство (i): пусть X ⊆ D направлено, тогда

${\check {f}}$(sup(X)) = λyf(sup(X),y)

= λ у. $\sup _{x\in X}$( е (х, у) )

= $\sup _{x\in X}$( λy.f(x,y) )

= суп( ${\check {f}}$(Х))

Доказательство (ii): определение L = λ $f.{\check {f}}$ тогда для Ф $\subseteq [D\times D^{'}\rightarrow D^{''}]$ направленный

L(sup(F)) = λ x λ y. (sup(F))(x,y))

= λ х λ у. $\sup _{y\in F}$е (х, у)

= $\sup _{y\in F}$λx λy.f(x,y)

= суп(L(F))

Не было продемонстрировано, как и почему λ-исчисление определяет топологию Скотта.

Деревья Бема и вычислительная топология

Деревья Бема , легко представленные графически, выражают вычислительное поведение лямбда-члена . Функциональность данного лямбда-выражения можно предсказать, обратившись к соответствующему ему дереву Бема. Деревья Бема можно рассматривать как нечто аналогичное $\mathbb {R}$ где дерево Бема данного набора похоже на непрерывную дробь действительного числа, и, более того, дерево Бема, соответствующее последовательности в нормальной форме , конечно, подобно рациональному подмножеству действительных чисел.

Деревья Бема определяются отображением элементов внутри последовательности чисел с порядком (≤, lh) и бинарным оператором * в набор символов. Тогда дерево Бема представляет собой отношение между набором символов посредством частичного отображения ψ.

Неформально деревья Бема можно представить следующим образом:

Дано: Σ = $\perp \cup$ { λ x_{1} $\cdots$x_{n} . и | n ∈ $\mathbb {N} ,x_{1}...x_{n}$y — переменные, и обозначая BT(M) как дерево Бема для лямбда-терма M, мы тогда имеем:

BT(M) = ⊥, если M неразрешима (следовательно, один узел)

БТ(М) = λ ${\vec {x}}$.и
                  /    \
БТ( $M_{1})$ БТ( $M_{m}$ ) ; если M разрешимо

Более формально:

Σ определяется как набор символов. Дерево Бёма λ-терма M, обозначаемого BT(M), представляет собой дерево с меткой Σ, определяемое следующим образом:

Если M неразрешимо:

$BT(M)(\langle \ \rangle )=\perp ,$

БТ(М)( $\langle k\rangle *\alpha$) неразрешима $\forall k,\alpha$

Если M разрешимо, где M = λ x_{1} $\cdots x_{n}.yM_{0}\cdots M_{m-1}$:

ВТ(М)(< >) = λ x_{1} $\cdots x_{n}.y$

БТ(М)( $\langle k\rangle *\alpha$) = БТ(M_k)( $\alpha$) $\forall \alpha$ и к < м

= не определено $\forall \alpha$ и k ≥ m

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

Дерево Бема и древовидная топология.

Обнаружено, что деревья Бёма допускают непрерывное отображение древесной топологии в топологию Скотта. Более конкретно:

Начнем с cpo B = (B,⊆) в топологии Скотта, с упорядочивания деревьев Бёма, обозначаемых M⊆ N, что означает, что M, N являются деревьями, а M являются результатами N. Древовидная топология на множестве Ɣ — это наименьшее множество позволяющая создать непрерывную карту

БТ: $\Gamma \rightarrow$Б. ​

Эквивалентным определением было бы сказать, что открытые множества Ɣ являются образом обратного дерева Бема. $BT^{-1}$ (O) где O — Скотт, открытый B. в

Применимость деревьев Бёма и древовидной топологии имеет множество интересных последствий для λ-членов, выраженных топологически:

Обнаружено, что нормальные формы существуют как изолированные точки.

Неразрешимые λ-члены являются точками компактификации.

Приложение и абстракция, подобно топологии Скотта, непрерывны в древовидной топологии.

Алгебраическая структура вычислений

Новые методы интерпретации λ-исчисления не только интересны сами по себе, но и позволяют по-новому взглянуть на поведение информатики. Бинарный оператор в λ-алгебре A является прикладным. Приложение обозначается ⋅ и считается, что оно дает структуру $A=(X,\cdot )$. Комбинаторная алгебра допускает использование оператора приложения и выступает в качестве полезной отправной точки, но остается недостаточной для λ-исчисления, поскольку не может выразить абстракцию. Алгебра λ становится комбинаторной алгеброй M в сочетании с синтаксическим оператором λ*, который преобразует терм B(x,y) с константами из M в C( ${\hat {y}}$)≡ λ* xB(x, ${\hat {y}}$). Также возможно определить модель расширения , чтобы обойти необходимость использования оператора λ*, разрешив ∀x (fx =gx) ⇒ f =g. Построение λ-алгебры путем введения оператора абстракции происходит следующим образом:

Мы должны построить алгебру, которая допускает решения таких уравнений, как axy = xyy, такие, что a = λ xy.xyy, и возникает необходимость в комбинаторной алгебре. Соответствующими атрибутами комбинаторной алгебры являются:

В рамках комбинаторной алгебры существуют аппликативные структуры . Аппликативная структура W представляет собой комбинаторную алгебру при условии:

⋅W нетривиален, то есть мощность W > 1.

⋅W обладает комбинаторной полнотой (см. полноту базиса SK ). Более конкретно: для каждого терма A ∈ множества термов W и $x_{1},...,x_{n}$ со свободными переменными A внутри ${x_{1},...,x_{n}}$ затем:

$\exists f\forall x_{1}\cdot \cdot \cdot x_{n}$ где $fx_{1}\cdot \cdot \cdot x_{n}=A$

Комбинаторная алгебра – это:

• Никогда не коммутативен
• Не ассоциативно.
• Никогда не ограничен.
• Никогда не рекурсивно.

Комбинаторные алгебры по-прежнему не могут выступать в качестве алгебраической структуры для λ-исчисления, а отсутствие рекурсии является основным недостатком. Однако существование аппликативного термина $A(x,{\vec {y}}$) обеспечивает хорошую отправную точку для построения алгебры λ-исчисления. Что необходимо, так это введение лямбда-члена , т.е. включить λx.A(x, ${\vec {y}}$).

Начнем с использования того факта, что в комбинаторной алгебре M с A(x, ${\vec {y}}$) внутри множества слагаемых, то:

$\forall {\vec {y}}$ $\exists b$ st bx = A(x, ${\vec {y}}$).

Затем мы требуем, чтобы b зависело от ${\vec {y}}$ в результате чего:

$\forall x$ Б( ${\vec {y}}$)x = A(x, ${\vec {y}}$).

Б( ${\vec {y}}$) становится эквивалентным члену λ и поэтому подходящим образом определяется следующим образом: B( ${\vec {y}})\equiv$ л*.

) . Теперь можно определить пре-λ-алгебру (pλA

pλA — аппликативная структура W = (X,⋅) такая, что для каждого терма A внутри множества термов внутри W и для каждого x существует терм λ*xA ∈ T(W) (T(W) ≡ термы из W) где (множество свободных переменных λ*xA) = (множество свободных переменных A) — {x}. W также должен продемонстрировать:

$(\beta )$ (λ*xA)x = А

$\alpha _{1}$λ*xA≡ λ*xA[x:=y] при условии, что y не является свободной переменной A

$\alpha _{2}$(λ*xA)[y:=z]≡λ*xA[x:=y] при условии, что y,z ≠ x и z не является свободной переменной A

Прежде чем определить полную λ-алгебру, мы должны ввести следующее определение множества λ-термов внутри W, обозначаемых $\Gamma (W)$ со следующими требованиями:

а € W $\Rightarrow c_{a}\in \Gamma (W)$

х € $\Gamma (W)$ для x ∈ ( $v_{0},v_{1},...$)

M,N ∈ $\Gamma (W)\Rightarrow$ (МН) ∈ $\Gamma (W)$

М € $\Gamma (W)\Rightarrow$ (λx.M) ∈ $\Gamma (W)$

Сопоставление терминов внутри $\Gamma (W)$ всем членам λ внутри W, обозначенным * : $\Gamma (W)\rightarrow \mathrm {T} (W)$, то можно спроектировать следующим образом:

$v_{i}^{*}=w_{i},c_{a}^{*}=c_{a}$

(МН)* = М* Н*

(λx.M)* = λ* x*.M*

Теперь мы определяем λ (M) для обозначения расширения после оценки членов внутри $\Gamma (W)$.

λx.(λy.yx) $c_{a}$ = λx. $c_{a}$x в λ (Вт).

Наконец, мы получаем полную λ-алгебру посредством следующего определения:

(1) λ-алгебра – это pλA W такая, что для M,N ∈ Ɣ(W):

λ (W) ⊢ M = N ⇒ W ⊨ M = N.

Несмотря на трудности, была заложена основа для правильной алгебраической структуры, в которой λ-исчисление и, следовательно, вычисления могут быть исследованы теоретико-групповым способом.