Лямбда-куб

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

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

• Ось x ( ): типы, которые могут связывать термины, соответствующие зависимым типам . ${\displaystyle \rightarrow }$
• Ось Y ( ): термины, которые могут связывать типы, соответствующие полиморфизму . ${\displaystyle \uparrow }$
• Ось z ( ): типы, которые могут связывать типы, соответствующие операторам (связывания) типов . ${\displaystyle \nearrow }$

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

Примеры систем

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

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

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

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

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

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

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

весело  х  ->  х

OCaml имеет тип

' а  ->  ' а

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

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

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

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

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

тип  int_tree  =  int  дерево

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

(λP) Лямбда-P

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

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

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

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

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

(λC) Исчисление конструкций

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

Формальное определение

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

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

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

и обозначая, когда не встречается свободно в . ${\displaystyle A\to B}$ ${\displaystyle \Pi x:A.B}$ ${\displaystyle x}$ ${\displaystyle B}$

Окружения, как это обычно бывает в типизированных системах, задаются следующим образом: ${\displaystyle \Gamma :=\emptyset \mid \Gamma ,x:A}$

Понятие β-редукции является общим для всех систем в кубе. Оно записывается и задается правилами Его рефлексивное, транзитивное замыкание записывается . ${\displaystyle \to _{\beta }}$ $${\displaystyle {\frac {}{(\lambda x:A.B)~C\to _{\beta }B[C/x]}}}$$ $${\displaystyle {\frac {B\to _{\beta }B'}{\lambda x:A.B\to _{\beta }\lambda x:A.B'}}}$$ $${\displaystyle {\frac {A\to _{\beta }A'}{\lambda x:A.B\to _{\beta }\lambda x:A'.B}}}$$ $${\displaystyle {\frac {B\to _{\beta }B'}{\Pi x:A.B\to _{\beta }\Pi x:A.B'}}}$$ $${\displaystyle {\frac {A\to _{\beta }A'}{\Pi x:A.B\to _{\beta }\Pi x:A'.B}}}$$ ${\displaystyle =_{\beta }}$

Следующие правила типизации также являются общими для всех систем в кубе: $${\displaystyle {\frac {}{\vdash *:\square }}\quad {\text{(Axiom)}}}$$ $${\displaystyle {\frac {\Gamma \vdash A:s}{\Gamma ,x:A\vdash x:A}}x\not \in \Gamma \quad {\text{(Start)}}}$$ $${\displaystyle {\frac {\Gamma \vdash A:B\quad \Gamma \vdash C:s}{\Gamma ,x:C\vdash A:B}}x\not \in \Gamma \quad {\text{(Weakening)}}}$$ $${\displaystyle {\frac {\Gamma \vdash C:\Pi x:A.B\quad \Gamma \vdash D:A}{\Gamma \vdash CD:B[D/x]}}\quad {\text{(Application)}}}$$ $${\displaystyle {\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})}$ $${\displaystyle {\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)}}}$$ ${\displaystyle {\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash C:B\quad \Gamma ,x:A\vdash B:s_{2}}{\Gamma \vdash \lambda x:A.C:\Pi x:A.B}}\quad {\text{(Abstraction)}}}$

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

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

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

Сравнение систем

λ→

Типичный вывод, который может быть получен, это или с сокращением стрелки, очень похожий на тождество (типа ) обычного λ→. Обратите внимание, что все используемые типы должны появляться в контексте, поскольку единственный вывод, который может быть сделан в пустом контексте, это . $${\displaystyle \alpha :*\vdash \lambda x:\alpha .x:\Pi x:\alpha .\alpha }$$ $${\displaystyle \alpha :*\vdash \lambda x:\alpha .x:\alpha \to \alpha }$$ ${\textstyle \alpha }$ ${\textstyle \vdash *:\square }$

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

λ2

В λ2 такие термины могут быть получены как с . Если читать как универсальную квантификацию, через изоморфизм Карри-Ховарда, это можно рассматривать как доказательство принципа взрыва. В общем, λ2 добавляет возможность иметь непредикативные типы, такие как , то есть термины, квантифицирующие по всем типам, включая себя. Полиморфизм также позволяет строить функции, которые не были конструктивны в λ→. Точнее, функции, определяемые в λ2, являются теми, которые доказуемо тотальны в арифметике Пеано второго порядка . ^[6] В частности, все примитивные рекурсивные функции определимы. $${\displaystyle \vdash (\lambda \beta :*.\lambda x:\bot .x\beta ):\Pi \beta :*.\bot \to \beta }$$ ${\textstyle \bot =\Pi \alpha :*.\alpha }$ ${\textstyle \Pi }$ ${\textstyle \bot }$

λP

В λP возможность иметь типы, зависящие от терминов, означает, что можно выразить логические предикаты. Например, следующее выводится: что соответствует, через изоморфизм Карри-Ховарда, доказательству . Однако с вычислительной точки зрения наличие зависимых типов не увеличивает вычислительную мощность, а только возможность выразить более точные свойства типов. ^[7] $${\displaystyle {\begin{array}{l}\alpha :*,a_{0}:\alpha ,p:\alpha \to *,q:*\vdash \\\quad \lambda z:(\Pi x:\alpha .px\to q).\\\quad \lambda y:(\Pi x:\alpha .px).\\\quad (za_{0})(ya_{0}):(\Pi x:\alpha .px\to q)\to (\Pi x:\alpha .px)\to q\end{array}}}$$ ${\displaystyle (\forall x:A,Px\to Q)\to (\forall x:A,Px)\to Q}$

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

λω

В λω можно определить следующий оператор , то есть . Вывод может быть получен уже в λ2, однако полиморфизм может быть определен только в том случае, если также присутствует правило . $${\displaystyle AND:=\lambda \alpha :*.\lambda \beta :*.\Pi \gamma :*.(\alpha \to \beta \to \gamma )\to \gamma }$$ ${\displaystyle \vdash AND:*\to *\to *}$ $${\displaystyle \alpha :*,\beta :*\vdash \Pi \gamma :*.(\alpha \to \beta \to \gamma )\to \gamma :*}$$ ${\textstyle AND}$ ${\textstyle (\square ,*)}$

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

λС

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

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

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

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

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

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

Общие свойства

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

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

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

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

Подтипирование

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

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

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

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

Примечания

1. Барендрегт, Хенк (1991). «Введение в системы обобщенных типов». Журнал функционального программирования . 1 (2): 125–154. doi :10.1017/s0956796800020025. hdl : 2066/17240 . ISSN  0956-7968. S2CID  44757552.
2. Недерпелт, Роб; Гейверс, Герман (2014). Теория типов и формальное доказательство. Cambridge University Press. стр. 69. ISBN 9781107036505.
3. Nederpelt & Geuvers 2014, с. 85
4. Nederpelt & Geuvers 2014, стр. 100
5. Швихтенберг, Гельмут (1975). «Definierbare Funktionen imλ-Kalkül mit Typen». Archiv für Mathematische Logik und Grundlagenforschung (на немецком языке). 17 (3–4): 113–114. дои : 10.1007/bf02276799. ISSN  0933-5846. S2CID  11598130.
6. Жирар, Жан-Ив; Лафон, Ив; Тейлор, Пол (1989). Доказательства и типы . Cambridge Tracts in Theoretical Computer Science. Том 7. Cambridge University Press. ISBN 9780521371810.
7. Риду, Оливье (1998). Лямбда-пролог A à Z ... или presque (PDF) . [сн] OCLC  494473554.
8. Ангиули, Карло; Гратцер, Дэниел (2024). «2.1.3 Кто проверяет типы правил типизации? и 2.2 К синтаксису теории зависимых типов». Принципы теории зависимых типов (PDF) . Университет Индианы и Орхусский университет . Получено 7 сентября 2024 г. .
9. Favier, Naïm (17 августа 2023 г.). «В правиле вывода преобразования лямбда-куба, почему необходимо Γ ⊢ B′:s?». Computer Science Stack Exchange . Получено 7 сентября 2024 г.
10. Пирс, Бенджамин; Дитцен, Скотт; Михайлов, Спиро (1989). Программирование в типизированных лямбда-исчислениях высшего порядка . Кафедра компьютерных наук, Университет Карнеги-Меллона. OCLC  20442222. CMU-CS-89-111 ERGO-89-075.
11. Sørensen, Morten Heine; Urzyczyin, Pawel (2006). "Pure type systems and the λ-cube". Lectures on the Curry-Howard Isomorphism . Elsevier. pp. 343–359. doi :10.1016/s0049-237x(06)80015-7. ISBN 9780444520777.
12. Пирс, Бенджамин (2002). Типы и языки программирования . MIT Press. С. 467–490. ISBN 978-0262162098. OCLC  300712077.
13. Пирс 2002, стр. 466
14. Риду 1998, стр. 70

1. Предположение в правиле преобразования является удобным; вместо этого можно было бы доказать метатеорему, что . ^{[8] [9]} ${\displaystyle \Gamma \vdash B':s}$ ${\displaystyle \Gamma \vdash A:B\land B=_{\beta }B'\Rightarrow \Gamma \vdash B':s}$

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

• Пейтон Джонс, Саймон; Мейер, Эрик (1997). "Henk: A Typed Intermediate Language" (PDF) . Microsoft . Henk основан непосредственно на лямбда-кубе, выразительном семействе типизированных лямбда-исчислений.

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

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