Ля́мбда-куб (λ-куб) — наочна класифікація восьми типізованих лямбда-числень з явним приписуванням типів (систем, типізованих за Черчем). Куб організований відповідно до можливих залежностей між типами і термами цього числення і формує природну структуру для числення конструкцій. Ідею λ-куба запропонував 1991 року нідерландський логік і математик Генк Барендрегт. Подальші узагальнення лямбда-куба можна отримати, розглядаючи чисту систему типів.
![image](https://www.wikidata.uk-ua.nina.az/image/aHR0cHM6Ly93d3cud2lraWRhdGEudWstdWEubmluYS5hei9pbWFnZS9hSFIwY0hNNkx5OTFjR3h2WVdRdWQybHJhVzFsWkdsaExtOXlaeTkzYVd0cGNHVmthV0V2WTI5dGJXOXVjeTh4THpFNUwweGhiV0prWVY5amRXSmxMbkJ1Wnc9PS5wbmc=.png)
Структура λ-куба
У системах λ-куба змінні відносять до одного з двох сортів: або
. Всі допустимі вирази теж поділяються за сортами. Твердження про належність виразу до сорту надбудовується над твердженням типізації, тобто висловлювання
читається так: елемент
має тип
і належить до сорту
. Сорт
використовується для звичайних змінних і термів λ-числення, сорт
— для змінних і виразів типу. Тому в системах λ-куба типи сорту
і елементи сорту
розглядаються як перетинні. Наприклад, тип терма
можна записати як елемент «вищого» сорту
. Типи сорту
іноді називають .
Під залежністю розуміють можливість визначати і використовувати функції, які відбивають елементи одного сорту в інший (або той самий). Елементи сорту залежать від елементів сорту
, якщо:
- для допустимого виразу
, який, можливо, містить змінну
, можна визначити лямбда-абстракцію
;
- для функції
має бути допустимим її застосування до елемента
, при цьому результат має бути елементом типу
сорту
, тобто
.
Базовою вершиною куба є система , що відповідає . Терми (елементи сорту
) залежать від термів; типи (елементи сорту
) в залежностях участі не беруть. Три осі, що виходять з базової вершини, породжують такі системи:
- терми, які залежать від типів: система
(лямбда-числення з поліморфними типами, система F);
- типи, які залежать від типів: система
(лямбда-числення з операторами над типами);
- типи, які залежать від термів: система
(лямбда-числення з залежними типами).
Решта систем є різними комбінаціями перелічених залежностей. Найбагатша система (поліморфне лямбда-числення вищого порядку з залежними типами) фактично є численням конструкцій.
Властивості систем λ-куба
Всі системи лямбда-куба мають властивість [en] будь-який допустимий терм (і тип) за скінченне число (β-редукцій) зводиться до єдиної нормальної форми.
Підтримка в мовах програмування
Різні функційні мови підтримують різні підмножини поданих у лямбда-кубі систем типів.
Посилання
- 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
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
Lya mbda kub l kub naochna klasifikaciya vosmi tipizovanih lyambda chislen z yavnim pripisuvannyam tipiv sistem tipizovanih za Cherchem Kub organizovanij vidpovidno do mozhlivih zalezhnostej mizh tipami i termami cogo chislennya i formuye prirodnu strukturu dlya chislennya konstrukcij Ideyu l kuba zaproponuvav 1991 roku niderlandskij logik i matematik Genk Barendregt Podalshi uzagalnennya lyambda kuba mozhna otrimati rozglyadayuchi chistu sistemu tipiv l kub Strilka uzdovzh kozhnogo rebra vkazuye na napryamok vklyuchennya prostisha sistema ye okremim vipadkom skladnishoyi Struktura l kubaU sistemah l kuba zminni vidnosyat do odnogo z dvoh sortiv displaystyle ast abo displaystyle Box Vsi dopustimi virazi tezh podilyayutsya za sortami Tverdzhennya pro nalezhnist virazu do sortu nadbudovuyetsya nad tverdzhennyam tipizaciyi tobto vislovlyuvannya A B C displaystyle A B C chitayetsya tak element A displaystyle A maye tip B displaystyle B i nalezhit do sortu C displaystyle C Sort displaystyle ast vikoristovuyetsya dlya zvichajnih zminnih i termiv l chislennya sort displaystyle Box dlya zminnih i viraziv tipu Tomu v sistemah l kuba tipi sortu displaystyle ast i elementi sortu displaystyle Box rozglyadayutsya yak peretinni Napriklad tip terma lx a x a a displaystyle lambda x alpha x alpha to alpha ast mozhna zapisati yak element vishogo sortu a a displaystyle alpha to alpha ast Box Tipi sortu displaystyle Box inodi nazivayut Pid zalezhnistyu rozumiyut mozhlivist viznachati i vikoristovuvati funkciyi yaki vidbivayut elementi odnogo sortu v inshij abo toj samij Elementi sortu s1 displaystyle s 1 zalezhat vid elementiv sortu s2 displaystyle s 2 yaksho dlya dopustimogo virazu F x t s1 displaystyle F x tau s 1 yakij mozhlivo mistit zminnu x s s2 displaystyle x sigma s 2 mozhna viznachiti lyambda abstrakciyu lx s F x s t s1 displaystyle lambda x sigma F x sigma to tau s 1 dlya funkciyi G s t s1 displaystyle G sigma to tau s 1 maye buti dopustimim yiyi zastosuvannya do elementa Y s s2 displaystyle Y sigma s 2 pri comu rezultat maye buti elementom tipu t displaystyle tau sortu s1 displaystyle s 1 tobto GY t s1 displaystyle G Y tau s 1 Bazovoyu vershinoyu kuba ye sistema l displaystyle lambda rightarrow sho vidpovidaye Termi elementi sortu displaystyle ast zalezhat vid termiv tipi elementi sortu displaystyle Box v zalezhnostyah uchasti ne berut Tri osi sho vihodyat z bazovoyi vershini porodzhuyut taki sistemi termi yaki zalezhat vid tipiv sistema l2 displaystyle lambda 2 lyambda chislennya z polimorfnimi tipami sistema F tipi yaki zalezhat vid tipiv sistema lw displaystyle lambda underline omega lyambda chislennya z operatorami nad tipami tipi yaki zalezhat vid termiv sistema lP displaystyle lambda P lyambda chislennya z zalezhnimi tipami Reshta sistem ye riznimi kombinaciyami perelichenih zalezhnostej Najbagatsha sistema lPw displaystyle lambda P omega polimorfne lyambda chislennya vishogo poryadku z zalezhnimi tipami faktichno ye chislennyam konstrukcij Vlastivosti sistem l kubaVsi sistemi lyambda kuba mayut vlastivist en bud yakij dopustimij term i tip za skinchenne chislo b redukcij zvoditsya do yedinoyi normalnoyi formi Pidtrimka v movah programuvannyaRizni funkcijni movi pidtrimuyut rizni pidmnozhini podanih u lyambda kubi sistem tipiv Haskell ML l2 sistema F V obmezhenij formi Haskell u realizaciyi GHC pochinayuchi z ostannih versij pidtrimuye lw displaystyle lambda underline omega za dopomogoyu type families Coq Agda lPw displaystyle lambda P omega chislennya konstrukcij PosilannyaHenk Barendregt Lambda Calculi with Types angl Handbook of Logic in Computer Science Volume II Oxford University Press Simon Peyton Jones and Erik Meijer 1997 Henk A Typed Intermediate Language 19 kvitnya 2012 u Wayback Machine angl Lennart Augustsson 2007 Simpler Easier 20 travnya 2021 u Wayback Machine angl Opis realizaciyi sistem lyambda kuba movoyu Haskell ros z perekladom Denisa Moskvina rozdilu pro lyambda kub iz knigi Henk Barendregt Lambda Calculi with Types