Лямбда-куб

Ля́мбда-куб (λ-куб) — наочна класифікація восьми типізованих лямбда-числень з явним приписуванням типів (систем, типізованих за Черчем). Куб організований відповідно до можливих залежностей між типами і термами цього числення і формує природну структуру для числення конструкцій. Ідею λ-куба запропонував 1991 року нідерландський логік і математик Генк Барендрегт. Подальші узагальнення лямбда-куба можна отримати, розглядаючи чисту систему типів.

λ-куб. Стрілка уздовж кожного ребра вказує на напрямок включення; простіша система є окремим випадком складнішої.

Структура λ-куба

У системах λ-куба змінні відносять до одного з двох сортів: $\ast$ або $\Box$. Всі допустимі вирази теж поділяються за сортами. Твердження про належність виразу до сорту надбудовується над твердженням типізації, тобто висловлювання $A:B:C$ читається так: елемент $A$ має тип $B$ і належить до сорту $C$. Сорт $\ast$ використовується для звичайних змінних і термів λ-числення, сорт $\Box$ — для змінних і виразів типу. Тому в системах λ-куба типи сорту $\ast$ і елементи сорту $\Box$ розглядаються як перетинні. Наприклад, тип терма $(\lambda x:\alpha .\,x):(\alpha \to \alpha ):\ast$ можна записати як елемент «вищого» сорту $(\alpha \to \alpha ):\ast :\Box$. Типи сорту $\Box$ іноді називають родами.

Під залежністю розуміють можливість визначати і використовувати функції, які відбивають елементи одного сорту в інший (або той самий). Елементи сорту $s_{1}$ залежать від елементів сорту $s_{2}$, якщо:

• для допустимого виразу $F[x]:\tau :s_{1}$, який, можливо, містить змінну $x:\sigma :s_{2}$, можна визначити лямбда-абстракцію $(\lambda x:\sigma .\,F[x]):(\sigma \to \tau ):s_{1}$;
• для функції $G:(\sigma \to \tau ):s_{1}$ має бути допустимим її застосування до елемента $Y:\sigma :s_{2}$, при цьому результат має бути елементом типу $\tau$ сорту $s_{1}$, тобто $(G\,Y):\tau :s_{1}$.

Базовою вершиною куба є система $\lambda ^{\rightarrow }$, що відповідає просто типізованому лямбда-численню. Терми (елементи сорту $\ast$) залежать від термів; типи (елементи сорту $\Box$) в залежностях участі не беруть. Три осі, що виходять з базової вершини, породжують такі системи:

• терми, які залежать від типів: система $\lambda 2$ (лямбда-числення з поліморфними типами, система F);
• типи, які залежать від типів: система $\lambda {\underline {\omega }}$ (лямбда-числення з операторами над типами);
• типи, які залежать від термів: система $\lambda P$ (лямбда-числення з залежними типами).

Решта систем є різними комбінаціями перелічених залежностей. Найбагатша система $\lambda P\omega$ (поліморфне лямбда-числення вищого порядку з залежними типами) фактично є численням конструкцій.

Властивості систем λ-куба

Всі системи лямбда-куба мають властивість сильної нормалізації будь-який допустимий терм (і тип) за скінченне число β-редукцій зводиться до єдиної нормальної форми.

Підтримка в мовах програмування

Різні функційні мови підтримують різні підмножини поданих у лямбда-кубі систем типів.

• Haskell, ML — λ2 (система F)
• В обмеженій формі Haskell (у реалізації GHC, починаючи з останніх версій) підтримує $\lambda {\underline {\omega }}$ за допомогою «type families».
• Coq, Agda — $\lambda P\omega$ (числення конструкцій)

Посилання

• Henk Barendregt, Lambda Calculi with Types(англ.) Handbook of Logic in Computer Science, Volume II, Oxford University Press.
• Simon Peyton Jones and Erik Meijer, 1997.. Henk: A Typed Intermediate Language [Архівовано 19 квітня 2012 у Wayback Machine.](англ.)
• Lennart Augustsson, 2007. Simpler, Easier! [Архівовано 20 травня 2021 у Wayback Machine.](англ.) Опис реалізації систем лямбда-куба мовою Haskell.
• Лямбда-куб на SpbHUG(рос.) з перекладом Дениса Москвіна розділу про лямбда-куб із книги Henk Barendregt, Lambda Calculi with Types