Лямбда-куб

Лямбда-куб. Направление каждой стрелки соответствует направлению включения.

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

• ось 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 для «типизированного лямбда-исчисления второго порядка») есть другой тип абстракции, написанный с помощью $\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-подобных языках . Например, полиморфное тождество

fun x -> x

OCaml тип имеет

'a -> 'a

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

(λ ω ) Система F ω

В системе F ${\underline {\omega }}$ вводится конструкция для типов поставок, которые зависят от других типов . Это называется конструктором типа и позволяет создать «функцию с типом в качестве значения ». Примером такого конструктора типа является тип бинарных деревьев с листьями, помеченными данными заданного типа. $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:

type 'a tree = | Leaf of 'a | Node of 'a tree * 'a tree

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

type int_tree = int tree

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

(λ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ω, эти четыре характеристики сосуществуют, так что и типы, и термины могут зависеть от типов и терминов. Четкая граница, существующая в λ→ между терминами и типами, несколько упразднена, поскольку все типы, кроме универсального, $\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 }$.

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

λ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, — это те функции, которые доказуемо полны в арифметике Пеано второго порядка . В частности, все примитивно-рекурсивные функции определимы.

λ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$.
Однако с вычислительной точки зрения наличие зависимых типов не увеличивает вычислительную мощность, а только дает возможность выразить более точные свойства типа.

Правило преобразования крайне необходимо при работе с зависимыми типами, поскольку оно позволяет выполнять вычисления над терминами типа. Например, если у вас есть $\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$.

ло

В lō следующий оператор

$$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 ,*)}$ тоже присутствует.

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

λC

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

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

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

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

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

Система куба	Логическая система
λ→	(Нулевой порядок) Исчисление высказываний
л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'$.

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

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

Подтипы

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

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

См. также

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

Дальнейшее чтение

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

Внешние ссылки

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