Cub lambda

Lambda-cube ( λ-cube ) este o clasificare vizuală a opt calculi lambda tipați cu atribuire explicită de tip (sisteme tip biserică ) . Cubul este organizat în funcție de posibilele dependențe dintre tipurile și termenii acestui calcul și formează o structură naturală pentru calculul de construcție . Ideea cubului λ a fost propusă în 1991 de către logicianul și matematicianul olandez Henk Barendregt . Alte generalizări ale cubului lambda pot fi obținute luând în considerare sistemul de tip pur .

Structura cubului λ

În sistemele λ-cub, variabilele sunt atribuite unuia din două feluri: sau . Toate expresiile valide sunt de asemenea sortate. Afirmația că o expresie aparține unui sort este construită deasupra aserției de tastare, adică instrucțiunea se citește după cum urmează: elementul are un tip și aparține sortării . Sortarea este folosită pentru variabile obișnuite și termeni ai calculului λ, sortarea este folosită pentru variabile și expresii de tip. Prin urmare, în sistemele λ-cub, tipurile de sortare și elementele de sortare sunt tratate ca intersectând. De exemplu, tipul unui termen poate fi scris ca un element de sortare „mai mare” . Tipurile de cultivare sunt uneori numite genuri . $\ast$ $\Cutie$ $A:B:C$ $A$ $B$ $C$ $\ast$ $\Cutie$ $\ast$ $\Cutie$ $(\lambda x:\alpha .\,x):(\alpha \to \alpha):\ast$ $(\alpha \to \alpha):\ast:\Box$ $\Cutie$

Dependența este înțeleasă ca abilitatea de a defini și utiliza funcții care mapează elemente de un fel cu altul (sau același). Elementele unui sort sunt dependente de elementele unui sort dacă: $s_{1}$ $s_{2}$

pentru o expresie validă , care poate conţine o variabilă , putem defini o abstractizare lambda ; $F[x]:\tau:s_{1)$ $x:\sigma:s_{2)$ $(\lambda x:\sigma .\,F[x]):(\sigma \to \tau):s_{1)$
funcția trebuie lăsată să se aplice unui element , iar rezultatul trebuie să fie un element de tip sort , adică . $G:(\sigma \to \tau):s_{1}$ $Y:\sigma:s_{2}$ $\tau$ $s_{1}$ $(G\,Y):\tau:s_{1)$

Vârful de bază al cubului este sistemul corespunzător calculului lambda tip simplu . Termenii (elementele de sortare ) depind de termeni; tipurile (elementele de sortare ) nu participă la dependențe. Cele trei axe care ies din vârful bazei dau naștere la următoarele sisteme: $\lambda ^{\rightarrow }$ $\ast$ $\Cutie$

termeni în funcție de tipuri: sistem (calcul lambda cu tipuri polimorfe, sistem F ); $\lambda 2$
tipuri dependente de tipuri: sistem (calcul lambda cu operatori peste tipuri); $\lambda \underline {\omega }$
tipuri dependente de termen: sistem (calcul lambda cu tipuri dependente ). $\lambda P$

Sistemele rămase sunt diferite combinații ale dependențelor enumerate. Cel mai bogat sistem (calcul lambda polimorf de ordin superior cu tipuri dependente) este de fapt un calcul de construcție . $\lambda P\omega$

Proprietățile sistemelor λ-cub

Toate sistemele cub lambda au proprietatea de normalizare puternică : orice termen (și tip) admisibil poate fi redus la o singură formă normală după un număr finit de β-reduceri .

Suport în limbaje de programare

Diferite limbaje funcționale acceptă un subset diferit al sistemelor de tip reprezentate în cubul lambda.

Haskell , ML - λ2 ( sistem F )
Într-o formă limitată, Haskell (în implementarea GHC de la versiunile recente) acceptă utilizarea „familiilor de tip”. $\lambda \underline {\omega }$
Coq , Agda - ( calcul de construcție ) $\lambda P\omega$

Link -uri

Henk Barendregt, Lambda Calculi with Types (engleză) , Handbook of Logic in Computer Science, Volumul II, Oxford University Press.
Simon Peyton Jones și Erik Meijer, 1997. Henk: A Typed Intermediate Language
Lennart Augustsson, 2007. Mai simplu, mai ușor! (Engleză) Descrierea implementării sistemelor lambda-cube în Haskell.
Lambda Cube pe SpbHUG (rusă) cu traducerea de către Denis Moskvin a secțiunii despre cubul lambda din cartea Henk Barendregt, Lambda Calculi with Types