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

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

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

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

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

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

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

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

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

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

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

Во-первых, учитывая частично заказанный набор D = (D, ≤), непустое подмножество Икс ⊆ D является направленный если ∀ х, у ∈ Икс ∃ z ∈ Икс где Икс≤ z & у ≤ z.

D это полный частичный заказ (cpo) если:

· Каждое направленное X ⊆D имеет супремум, и:

∃ дно элемент ⊥ ∈ D такой, что ∀ Икс ∈ D ⊥ ≤ Икс.

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

О ⊆ D является открыто если:

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

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

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

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

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

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

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

Доказательство: Учитывая два открытых набора, U и V, мы определяем W = U∩V. Если W = ∅, тогда W открыт. Если не пусто, скажи б ∈ upset (W) (верхнее множество W), то для некоторого а ∈ W, а ≤ б. поскольку а ∈ U∩V, и б элемент верхнего набора обоих U и V, тогда б ∈ W.

Наконец, если D направленное множество с супремумом в W, то по предположению sup (D) ∈ ${\displaystyle U\cap V}$. Так что есть а ∈ ${\displaystyle U\cap D}$ и б ∈ ${\displaystyle V\cap D}$. поскольку D направлен туда c ∈ D с участием ${\displaystyle a\leq c,b\leq c}$; и с тех пор U и V верхние наборы, c ∈ ${\displaystyle U\cap V}$ также.

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

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

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

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

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

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

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

час(sup (F)) = sup (F)(Икс)

= sup ({ж(Икс) | ж ∈ F} )

= sup ({час(ж) | ж ∈ F} )

= sup ( час(F) )

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

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

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

= f (sup ((x,${\displaystyle x_{0}^{'}}$) | x ∈ X}))

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

= sup ({f (x,${\displaystyle x_{0}^{'}}$) | x ∈ X})

= sup (g (X))

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

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

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

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

(я) ${\displaystyle {\check {f}}}$ непрерывно, что означает ${\displaystyle {\check {f}}}$ ∈ ${\displaystyle [D\rightarrow [D^{'}\rightarrow D^{''}]}$

(ii) λ ${\displaystyle f.{\check {f}}:[D\times D^{'}\rightarrow D^{''}]\rightarrow [D\rightarrow [D^{'}\rightarrow D^{''}]}$ непрерывно.

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

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

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

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

= sup (${\displaystyle {\check {f}}}$(ИКС))

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

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

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

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

= sup (L (F))

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

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

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

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

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

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

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

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

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

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

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

${\displaystyle BT(M)(\langle \ \rangle )=\perp ,}$

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

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

BT (M) (<>) = λ x_ {1} ${\displaystyle \cdots x_{n}.y}$

БТ (М) (${\displaystyle \langle k\rangle *\alpha }$) = BT (M_k) (${\displaystyle \alpha }$) ${\displaystyle \forall \alpha }$ и k

= undefined ${\displaystyle \forall \alpha }$ и k ≥ m

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

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

Установлено, что Дерево Бема позволяет непрерывное отображение от топологии дерева к топологии Скотта. Более конкретно:

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

BT:${\displaystyle \Gamma \rightarrow }$B.

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

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

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

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

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

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

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

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

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

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

· W демонстрирует комбинаторную полноту (см. полнота базиса С-К ). Более конкретно: для каждого члена A ∈ множество членов W, и ${\displaystyle x_{1},...,x_{n}}$ со свободными переменными A внутри ${\displaystyle {x_{1},...,x_{n}}}$ тогда:

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

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

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

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

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

${\displaystyle \forall {\vec {y}}}$ ${\displaystyle \exists b}$ s.t. Ьх = А (х, ${\displaystyle {\vec {y}}}$).

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

${\displaystyle \forall x}$ B (${\displaystyle {\vec {y}}}$) х = А (х, ${\displaystyle {\vec {y}}}$).

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

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

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

${\displaystyle (\beta )}$ (λ * x.A) x = A

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

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

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

a ∈ W ${\displaystyle \Rightarrow c_{a}\in \Gamma (W)}$

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

M, N ∈ ${\displaystyle \Gamma (W)\Rightarrow }$ (MN) ∈ ${\displaystyle \Gamma (W)}$

M ∈ ${\displaystyle \Gamma (W)\Rightarrow }$ (λx.M) ∈ ${\displaystyle \Gamma (W)}$

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

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

(MN) * = M * N *

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

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

λx. (λy.yx)${\displaystyle c_{a}}$ = λx.${\displaystyle c_{a}}$х в λ(W).

В итоге мы получаем полную λ-алгебра через следующее определение:

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

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

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

использованная литература

1. Церковь 1934 г .: 90 сноск в Дэвисе 1952 г.
2. Тьюринг 1936-7 в Davis 1952: 149
3. Барендрегт Х.П. Синтаксис и семантика лямбда-исчисления. Издательская компания Северной Голландии. 1981
4. Барендрегт Х.П. Синтаксис и семантика лямбда-исчисления. Издательская компания Северной Голландии. 1981 г.
5. Д. С. Скотт. Модели для λ-исчисления. Неофициально распространено, 1969 г. Примечания, декабрь 1969 г., Oxford Univ.
6. Гордон, M.J.C., Денотационное описание языков программирования. Springer Verlag, Берлин. 1979 г.
7. Скотт, Д. С., Стрейчи, К. К математической семантике компьютерных языков, Proc. Symp. по компьютерам и автоматам, Политехнический институт Бруклина, 21, стр. 19 46. 1971.
8. Берри Г. Последовательные алгоритмы на конкретных структурах данных, Теоретическая информатика 20, 265 321 (1982).
9. Д. С. Скотт. «Сплошные решетки». Вычислительная лаборатория Оксфордского университета, август 1971 года.