Лямбда-куб

В математической логике и теории типов λ -куб (также называемый лямбда-куб ) — это основа, представленная Хенком Барендрегтом. ^[1]исследовать различные измерения, в которых исчисление конструкций является обобщением просто типизированного λ-исчисления . Каждое измерение куба соответствует новому виду зависимости между терминами и типами. Здесь «зависимость» относится к способности термина или типа связывать термин или тип. Соответствующие размеры λ-куба соответствуют:

ось X ( $\rightarrow$ ): типы, которые могут связывать термины, соответствующие зависимым типам .
ось Y ( $\uparrow$ ): термины, которые могут связывать типы, соответствующие полиморфизму .
ось Z ( $\nearrow$ ): типы, которые могут связывать типы, соответствующие операторам типа (привязки) .

Различные способы объединения этих трех измерений дают 8 вершин куба, каждая из которых соответствует разному типу типизированной системы. λ-куб можно обобщить до понятия системы чистого типа .

Примеры систем [ править ]

(λ→) Просто напечатанное лямбда-исчисление [ править ]

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

${\frac {\Gamma ,x:\sigma \;\vdash \;t:\tau }{\Gamma \;\vdash \;\lambda x.t:\sigma \to \tau }}$

(λ2) Система F [ править ]

В системе F (также называемой λ2 для «типизированного лямбда-исчисления второго порядка») ^[2] есть другой тип абстракции, написанный с помощью $\Lambda$ , что позволяет терминам зависеть от типов со следующим правилом:

${\frac {\Gamma \;\vdash \;t:\sigma }{\Gamma \;\vdash \;\Lambda \alpha .t:\Pi \alpha .\sigma }}\;{\text{ if }}\alpha {\text{ does not occur free in }}\Gamma$

Термины, начинающиеся с $\Lambda$ называются полиморфными , так как их можно применять к разным типам для получения разных функций, аналогично полиморфным функциям в ML-подобных языках . Например, полиморфное тождество

весело   х   ->   х

OCaml имеет тип

'  а   ->   '  а

это означает, что он может принимать аргумент любого типа 'aи вернуть элемент этого типа. Этот тип соответствует по λ2 типу $\Pi \alpha .\alpha \to \alpha$ .

(λ ω ) Система F ω [ править ]

В системе F ${\underline {\omega }}$ вводится конструкция для типов поставок, которые зависят от других типов . Это называется конструктором типа и позволяет создать «функцию с типом в качестве значения ». ^[3] Примером такого конструктора типа является тип бинарных деревьев с листьями, помеченными данными заданного типа. $A$ : ${\mathsf {TREE}}:=\lambda A:*.\Pi B.(A\to B)\to (B\to B\to B)\to B$ , где " $A:*$ "неофициально" означает " $A$ является типом». Это функция, которая принимает параметр типа. $A$ в качестве аргумента и возвращает тип ${\mathsf {TREE}}$ значений типа $A$ . В конкретном программировании эта особенность соответствует возможности определять конструкторы типов внутри языка, а не рассматривать их как примитивы. Предыдущий конструктор типа примерно соответствует следующему определению дерева с помеченными листьями в OCaml:

введите   '  дерево     =   |    Лист     '  а   |    Узел     '  дерева     *   '  дерева

Этот конструктор типа можно применять к другим типам для получения новых типов. Например, чтобы получить тип дерева целых чисел:

введите   int_tree   =   целое   дерево

Система Ф ${\underline {\omega }}$ обычно не используется сам по себе, но полезен для выделения независимой функции конструкторов типов. ^[4]

(λP) Лямбда-П [ править ]

В системе λP , также называемой ΛΠ и тесно связанной с LF Logical Framework , существуют так называемые зависимые типы . Это типы, которым разрешено зависеть от термов . Важнейшим правилом внедрения системы является

${\frac {\Gamma ,x:A\;\vdash \;B:*}{\Gamma \;\vdash \;(\Pi x:A.B):*}}$

где $*$ представляет допустимые типы. Новый конструктор типов $\Pi$ через изоморфизм Карри-Говарда соответствует квантору универсальности, а система λP в целом соответствует логике первого порядка с импликацией как единственной связкой. Примером таких зависимых типов в конкретном программировании является тип векторов определенной длины: длина — это термин, от которого зависит тип.

(Λω) Система Fω [ править ]

Система Fω сочетает в себе $\Lambda$ конструктор системы F и конструкторы типов из системы F ${\underline {\omega }}$ . Таким образом, система Fω предоставляет как термины, зависящие от типов , так и типы, зависящие от типов .

(λC) Исчисление конструкций [ править ]

В исчислении конструкций обозначается как λC в кубе или как λPω, ^[1]^: 130эти четыре характеристики сосуществуют, так что и типы, и термины могут зависеть от типов и терминов. Четкая граница, существующая в λ→ между терминами и типами, несколько упразднена, поскольку все типы, кроме универсального, $\square$ сами являются терминами типа.

Формальное определение [ править ]

Что касается всех систем, основанных на просто типизированном лямбда-исчислении, все системы в кубе задаются в два этапа: сначала необработанные термины вместе с понятием β-редукции , а затем правила типизации, которые позволяют типизировать эти термины.

Множество сортов определяется как $S:=\{*,\square \}$ , сорта обозначаются буквой $s$ . Также есть набор $V$ переменных, представленных буквами $x,y,\dots$ . Необработанные члены восьми систем куба задаются следующим синтаксисом:

$A:=x\mid s\mid A~A\mid \lambda x:A.A\mid \Pi x:A.A$

и $A\to B$ обозначающий $\Pi x:A.B$ когда $x$ не возникает свободно в $B$ .

Среды, как обычно в типизированных системах, задаются формулой $\Gamma :=\emptyset \mid \Gamma ,x:A$

Понятие β-редукции является общим для всех систем куба. Это написано $\to _{\beta }$ и задано правилами

{\frac {}{(\lambda x:A.B)~C\to _{\beta }B[C/x]}}

{\frac {B\to _{\beta }B'}{\lambda x:A.B\to _{\beta }\lambda x:A.B'}}

{\frac {A\to _{\beta }A'}{\lambda x:A.B\to _{\beta }\lambda x:A'.B}}

{\frac {B\to _{\beta }B'}{\Pi x:A.B\to _{\beta }\Pi x:A.B'}}

{\frac {A\to _{\beta }A'}{\Pi x:A.B\to _{\beta }\Pi x:A'.B}}

Его рефлексивное, транзитивное замыкание записывается

=_{\beta }

.

Следующие правила типизации также являются общими для всех систем в кубе:

{\frac {}{\vdash *:\square }}\quad {\text{(Axiom)}}

{\frac {\Gamma \vdash A:s\quad x{\text{ does not occur in }}\Gamma }{\Gamma ,x:A\vdash x:A}}\quad {\text{(Start)}}

{\frac {\Gamma \vdash A:B\quad \Gamma \vdash C:s}{\Gamma ,x:C\vdash A:B}}\quad {\text{(Weakening)}}

{\frac {\Gamma \vdash C:\Pi x:A.B\quad \Gamma \vdash a:A}{\Gamma \vdash Ca:B[a/x]}}\quad {\text{(Application)}}

{\frac {\Gamma \vdash A:B\quad B=_{\beta }B'\quad \Gamma \vdash B':s}{\Gamma \vdash A:B'}}\quad {\text{(Conversion)}}

Разница между системами заключается в парах сортов

{\textstyle (s_{1},s_{2})}

которые разрешены в следующих двух правилах ввода:

{\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash B:s_{2}}{\Gamma \vdash \Pi x:A.B:s_{2}}}\quad {\text{(Product)}}

{\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash b:B\quad \Gamma ,x:A\vdash B:s_{2}}{\Gamma \vdash \lambda x:A.b:\Pi x:A.B}}\quad {\text{(Abstraction)}}

Соответствие между системами и парами ${\textstyle (s_{1},s_{2})}$ в правилах разрешено следующее:

$(s_{1},s_{2})$	$(,)$	$(*,\square )$	$(\square ,*)$	$(\square ,\square )$
λ→
λP
л2
ло о
λP2
λP ω
вот
λС

Каждому направлению куба соответствует одна пара (исключая пару ${\textstyle (*,*)}$ общие для всех систем), и в свою очередь каждая пара соответствует одной возможности зависимости между терминами и типами:

${\textstyle (*,*)}$ позволяет условиям зависеть от условий.
${\textstyle (*,\square )}$ позволяет типам зависеть от терминов.
${\textstyle (\square ,*)}$ позволяет терминам зависеть от типов.
${\textstyle (\square ,\square )}$ позволяет типам зависеть от типов.

Сравнение систем [ править ]

λ→ [ править ]

Типичный вывод, который можно получить:

\alpha :*\vdash \lambda x:\alpha .x:\Pi x:\alpha .\alpha

или с помощью ярлыка со стрелкой

\alpha :*\vdash \lambda x:\alpha .x:\alpha \to \alpha

очень напоминающий тождество (типа

{\textstyle \alpha }

) обычного λ→. Обратите внимание, что все используемые типы должны присутствовать в контексте, поскольку единственный вывод, который можно выполнить в пустом контексте, — это

{\textstyle \vdash *:\square }

.

Вычислительная мощность довольно слабая, соответствует расширенным полиномам (многочленам вместе с условным оператором). ^[5]

λ2 [ править ]

В λ2 такие члены можно получить как

\vdash (\lambda \beta :*.\lambda x:\bot .x\beta ):\Pi \beta :*.\bot \to \beta

с

{\textstyle \bot =\Pi \alpha :*.\alpha }

. Если кто-то читает

{\textstyle \Pi }

как универсальная квантификация через изоморфизм Карри-Ховарда, это можно рассматривать как доказательство принципа взрыва. В общем, λ2 добавляет возможность иметь непредикативные типы, такие как

{\textstyle \bot }

, то есть термины, количественно оценивающие все типы, включая самих себя.
Полиморфизм также позволяет строить функции, которые невозможно построить в λ→. Точнее, функции, определяемые в λ2, — это те функции, которые доказуемо полны в арифметике Пеано второго порядка . ^[6] В частности, все примитивно-рекурсивные функции определимы.

λP [ править ]

В λP возможность иметь типы в зависимости от термов означает, что можно выражать логические предикаты. Например, можно вывести следующее:

\alpha :*,a_{0}:\alpha ,p:\alpha \to *,q:*\vdash \lambda z:(\Pi x:\alpha .px\to q).\lambda y:(\Pi x:\alpha .px).(za_{0})(ya_{0}):(\Pi x:\alpha .px\to q)\to (\Pi x:\alpha .px)\to q

что соответствует, посредством изоморфизма Карри-Говарда, доказательству

(\forall x:A,Px\to Q)\to (\forall x:A,Px)\to Q

.
Однако с вычислительной точки зрения наличие зависимых типов не увеличивает вычислительную мощность, а только дает возможность выразить более точные свойства типа. ^[7]

Правило преобразования крайне необходимо при работе с зависимыми типами, поскольку оно позволяет выполнять вычисления над терминами типа. Например, если у вас есть $\Gamma \vdash A:P((\lambda x.x)y)$ и $\Gamma \vdash B:\Pi x:P(y).C$ , вам необходимо применить правило преобразования, чтобы получить $\Gamma \vdash A:P(y)$ иметь возможность печатать $\Gamma \vdash BA:C$ .

ло [ править ]

В λω следующий оператор

AND:=\lambda \alpha :*.\lambda \beta :*.\Pi \gamma :*.(\alpha \to \beta \to \gamma )\to \gamma

определимо, то есть

\vdash AND:*\to *\to *

. Вывод

\alpha :*,\beta :*\vdash \Pi \gamma :*.(\alpha \to \beta \to \gamma )\to \gamma :*

можно получить уже в λ2, однако полиморфный

{\textstyle AND}

может быть определено только в том случае, если правило

{\textstyle (\square ,*)}

тоже присутствует.

С вычислительной точки зрения λω чрезвычайно силен и считается основой языков программирования. ^[8]

λC [ править ]

Исчисление конструкций обладает как выразительностью предикатов λP, так и вычислительной мощностью λω, поэтому λC также называется λPω, ^[1]^: 130 так что он очень мощный, как с логической, так и с вычислительной стороны.

Связь с другими системами [ править ]

Система Automath аналогична λ2 с логической точки зрения. ML -подобные языки с точки зрения типизации лежат где-то между λ→ и λ2, поскольку они допускают ограниченный вид полиморфных типов, то есть типов в пренексной нормальной форме. Однако, поскольку они содержат некоторые операторы рекурсии, их вычислительная мощность больше, чем у λ2. ^[7] Система Coq основана на расширении λC с помощью линейной иерархии вселенных, а не только одной нетипизированной системы. ${\textstyle \square }$ и умение строить индуктивные типы.

Системы чистых типов можно рассматривать как обобщение куба с произвольным набором сортов, аксиомами, правилами произведения и абстракции. И наоборот, системы лямбда-куба можно выразить как системы чистого типа с двумя видами: $\{*,\square \}$ , единственная аксиома ${\textstyle \{*,\square \}}$ и набор правил ${\textstyle R}$ такой, что $\{(*,*,*)\}\subseteq R\subseteq \{(*,*,*),(*,\square ,\square ),(\square ,*,*),(\square ,\square ,\square )\}$ . ^[1]

Благодаря изоморфизму Карри-Говарда существует взаимно однозначное соответствие между системами в лямбда-кубе и логическими системами: ^[1] а именно:

Система куба	Логическая система
λ→	(Нулевой порядок) Исчисление высказываний
л2	Исчисление высказываний второго порядка
ло о	Слабое исчисление высказываний высшего порядка
вот	Исчисление высказываний высшего порядка
λP	(Первый порядок) Логика предикатов
λP2	Исчисление предикатов второго порядка
λP ω	Слабое исчисление предикатов высшего порядка
λС	Расчет конструкций

Вся логика импликативна (т.е. единственные связки ${\textstyle \to }$ и ${\textstyle \forall }$ ), однако можно определить и другие связки, например $\wedge$ или $\neg$ импредикативным образом в логиках второго и более высокого порядка. В слабой логике высшего порядка существуют переменные для предикатов более высокого порядка, но их количественная оценка невозможна.

Общие свойства [ править ]

Все системы в кубе пользуются

свойство Чёрча -Россера : если $M\to _{\beta }N$ и $M\to _{\beta }N'$ тогда существует $N''$ такой, что $N\to _{\beta }^{*}N''$ и $N'\to _{\beta }^{*}N''$ ;
свойство предметного сокращения : если $\Gamma \vdash M:T$ и $M\to _{\beta }M'$ затем $\Gamma \vdash M':T$ ;
уникальность типов: если $\Gamma \vdash A:B$ и $\Gamma \vdash A:B'$ затем $B=_{\beta }B'$ .

Все это можно доказать на общих системах чистых типов. ^[9]

Любой терм, хорошо типизированный в системе куба, является сильно нормализующим. ^[1]хотя это свойство не является общим для всех систем чистых типов. Ни одна система в кубе не является полной по Тьюрингу. ^[7]

Подтипы [ править ]

Однако подтипы не представлены в кубе, хотя такие системы, как $F_{<:}^{\omega }$ , известная как ограниченная квантификация высшего порядка , которая сочетает в себе подтипирование и полиморфизм, представляет практический интерес и может быть далее обобщена на операторы ограниченного типа . Дальнейшие расширения $F_{<:}^{\omega }$ разрешить определение чисто функциональных объектов ; эти системы обычно разрабатывались после публикации статьи о лямбда-кубе. ^[10]

Идея куба принадлежит математику Хенку Барендрегту (1991). Структура систем чистых типов обобщает лямбда-куб в том смысле, что все углы куба, а также многие другие системы могут быть представлены как экземпляры этой общей структуры. ^[11]Этот фреймворк появился на пару лет раньше лямбда-куба. В своей статье 1991 года Барендрегт также определяет углы куба в этой системе.

См. также [ править ]

В своем Разрешении руководить исследованиями ^[12] Оливье Риду дает вырезанный шаблон лямбда-куба, а также двойственное представление куба в виде октаэдра, где 8 вершин заменены гранями, а также двойственное представление в виде додекаэдра, где 12 ребер заменены гранями. лица.

Примечания [ править ]

^ Перейти обратно: ^а ^б ^с ^д ^Это ^ж Барендрегт, Хенк (1991). «Введение в системы обобщенных типов». Журнал функционального программирования . 1 (2): 125–154. дои : 10.1017/s0956796800020025 . hdl : 2066/17240 . ISSN 0956-7968 . S2CID 44757552 .
^ Недерпельт, Роб; Геверс, Герман (2014). Теория типов и формальное доказательство . Издательство Кембриджского университета. п. 69. ИСБН 9781107036505 .
^ Nederpelt & Geuvers 2014 , с. 85
^ Nederpelt & Geuvers 2014 , с. 100
^ Швихтенберг, Гельмут (1975). «Определимые функции в λ-исчислении с типами». Архив математической логики и фундаментальных исследований (на немецком языке). 17 (3–4): 113–114. дои : 10.1007/bf02276799 . ISSN 0933-5846 . S2CID 11598130 .
^ Жирар, Жан-Ив; Лафон, Ив; Тейлор, Пол (1989). Доказательства и типы . Кембриджские трактаты по теоретической информатике. Том. 7. Издательство Кембриджского университета. ISBN 9780521371810 .
^ Перейти обратно: ^а ^б ^с Риду, Оливье (1998). Лямбда-Пролог от А до Я... или почти (PDF) . [сн] OCLC 494473554 .
^ Пирс, Бенджамин; Дитцен, Скотт; Михайлов, Спиро (1989). Программирование в типизированных лямбда-исчислениях высшего порядка . Факультет компьютерных наук Университета Карнеги-Меллон. OCLC 20442222 . КМУ-КС-89-111 ЭРГО-89-075.
^ Соренсен, Мортен Хейне; Ужичин, Павел (2006). «Системы чистого типа и λ-куб». Лекции по изоморфизму Карри-Говарда . Эльзевир. стр. 343–359. дои : 10.1016/s0049-237x(06)80015-7 . ISBN 9780444520777 .
^ Пирс, Бенджамин (2002). Типы и языки программирования . МТИ Пресс. стр. 467–490. ISBN 978-0262162098 . ОСЛК 300712077 .
^ Пирс 2002 , с. 466
^ Риду 1998 , с. 70

Дальнейшее чтение [ править ]

Пейтон Джонс, Саймон; Мейер, Эрик (1997). «Хенк: типизированный язык среднего уровня» (PDF) . Майкрософт . Henk основан непосредственно на лямбда-кубе, выразительном семействе типизированных лямбда-исчислений.

Внешние ссылки [ править ]

Лямбда-куб Барендрегта в контексте систем чистых типов Роджера Бишопа Джонса

[:0-1] Перейти обратно: ^а ^б ^с ^д ^Это ^ж Барендрегт, Хенк (1991). «Введение в системы обобщенных типов». Журнал функционального программирования . 1 (2): 125–154. дои : 10.1017/s0956796800020025 . hdl : 2066/17240 . ISSN 0956-7968 . S2CID 44757552 .

[2] Недерпельт, Роб; Геверс, Герман (2014). Теория типов и формальное доказательство . Издательство Кембриджского университета. п. 69. ИСБН 9781107036505 .

[3] Nederpelt & Geuvers 2014 , с. 85

[4] Nederpelt & Geuvers 2014 , с. 100

[5] Швихтенберг, Гельмут (1975). «Определимые функции в λ-исчислении с типами». Архив математической логики и фундаментальных исследований (на немецком языке). 17 (3–4): 113–114. дои : 10.1007/bf02276799 . ISSN 0933-5846 . S2CID 11598130 .

[6] Жирар, Жан-Ив; Лафон, Ив; Тейлор, Пол (1989). Доказательства и типы . Кембриджские трактаты по теоретической информатике. Том. 7. Издательство Кембриджского университета. ISBN 9780521371810 .

[:1-7] Перейти обратно: ^а ^б ^с Риду, Оливье (1998). Лямбда-Пролог от А до Я... или почти (PDF) . [сн] OCLC 494473554 .

[8] Пирс, Бенджамин; Дитцен, Скотт; Михайлов, Спиро (1989). Программирование в типизированных лямбда-исчислениях высшего порядка . Факультет компьютерных наук Университета Карнеги-Меллон. OCLC 20442222 . КМУ-КС-89-111 ЭРГО-89-075.

[9] Соренсен, Мортен Хейне; Ужичин, Павел (2006). «Системы чистого типа и λ-куб». Лекции по изоморфизму Карри-Говарда . Эльзевир. стр. 343–359. дои : 10.1016/s0049-237x(06)80015-7 . ISBN 9780444520777 .

[10] Пирс, Бенджамин (2002). Типы и языки программирования . МТИ Пресс. стр. 467–490. ISBN 978-0262162098 . ОСЛК 300712077 .

[11] Пирс 2002 , с. 466

[12] Риду 1998 , с. 70

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]