Лямбда-куб

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

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

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

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

Під залежністю розуміють можливість визначати і використовувати функції, які відбивають елементи одного сорту в інший (або той самий). Елементи сорту $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$, тобто $(GY):\tau :s_1$.

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

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

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

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

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

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

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

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

Посилання

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