Лямбда-куб

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

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

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

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

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

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

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

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

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

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

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

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

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

• Haskell, ML — λ2 (система F)
• В обмеженій формі Haskell (у реалізації GHC, починаючи з останніх версій) підтримує ${\displaystyle \lambda {\underline {\omega }}}$ за допомогою «type families».
• Coq, Agda — ${\displaystyle \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.
• (рос.) з перекладом Дениса Москвіна розділу про лямбда-куб із книги Henk Barendregt, Lambda Calculi with Types