Lambdakub

Lambda-kub ( λ-kub ) är en visuell klassificering av åtta maskinskrivna lambda-kalkyler med explicit typtilldelning (Church-typed systems ) . Kuben är organiserad efter möjliga beroenden mellan typerna och termerna i denna kalkyl och bildar en naturlig struktur för konstruktionskalkylen . Idén med λ-kuben föreslogs 1991 av den holländska logikern och matematikern Henk Barendregt . Ytterligare generaliseringar av lambdakuben kan erhållas genom att betrakta systemet av ren typ .

Struktur för λ-kuben

I λ-kubsystem tilldelas variabler till en av två sorter: eller . Alla giltiga uttryck sorteras också. Påståendet att ett uttryck tillhör en sort byggs ovanpå skrivpåståendet, det vill säga påståendet lyder som följer: elementet har en typ och tillhör sorten . Sorteringen används för vanliga variabler och termer i λ-kalkylen, sorteringen används för variabler och typuttryck. Därför behandlas sorteringstyper och sorteringselement i λ-kubsystem som korsande. Typen av en term kan till exempel skrivas som ett element av en "högre" sort . Kultivartyper kallas ibland för släkten . $\ast$ $\Låda$ $A:B:C$ $A$ $B$ $C$ $\ast$ $\Låda$ $\ast$ $\Låda$ $(\lambda x:\alpha .\,x):(\alpha \to \alpha ):\ast$ $(\alpha \to \alpha ):\ast :\Box$ $\Låda$

Beroende förstås som förmågan att definiera och använda funktioner som mappar element av en sort till en annan (eller samma). Elementen i en sort är beroende av elementen i en sort om: $s_{1}$ $s_{2}$

för ett giltigt uttryck , som eventuellt innehåller en variabel , kan vi definiera en lambdaabstraktion ; ${\displaystyle F[x]:\tau :s_{1))$ $x:\sigma :s_{2}$ ${\displaystyle (\lambda x:\sigma .\,F[x]):(\sigma \to \tau ):s_{1))$
funktionen måste tillåtas tillämpas på ett element , och resultatet måste vara ett element av typ sort , det vill säga . $G:(\sigma \to \tau ):s_{1}$ $Y:\sigma :s_{2}$ $\tau$ $s_{1}$ ${\displaystyle (G\,Y):\tau :s_{1))$

Kubens baspunkt är det system som motsvarar den enkelt skrivna lambdakalkylen . Termer (element of sort ) beror på termer; typer (sorteringselement ) deltar inte i beroenden. De tre axlarna som kommer ut från baspunkten ger upphov till följande system: $\lambda ^{\högerpil }$ $\ast$ $\Låda$

termer beroende på typer: system (lambda-kalkyl med polymorfa typer, system F ); $\lambda 2$
typer beroende på typer: system (lambda-kalkyl med operatorer över typer); $\lambda \underline {\omega }$
termberoende typer: system (lambdakalkyl med beroende typer ). $\lambda P$

De återstående systemen är olika kombinationer av de angivna beroenden. Det rikaste systemet (polymorf lambdakalkyl av högre ordning med beroende typer) är faktiskt en konstruktionskalkyl . $\lambda P\omega$

Egenskaper för λ-kubsystem

Alla lambda-kubsystem har den starka normaliseringsegenskapen : vilken som helst tillåten term (och typ) kan reduceras till en enda normalform efter ett ändligt antal β-reduktioner .

Stöd i programmeringsspråk

Olika funktionella språk stöder en annan delmängd av typsystemen som representeras i lambdakuben.

Haskell , ML - λ2 ( system F )
I en begränsad form stöder Haskell (i GHC- implementeringen sedan de senaste versionerna) användning av "typfamiljer". $\lambda \underline {\omega }$
Coq , Agda - ( konstruktionskalkyl ) $\lambda P\omega$

Länkar

Henk Barendregt, Lambda Calculi with Types (engelska) , Handbook of Logic in Computer Science, Volym II, Oxford University Press.
Simon Peyton Jones och Erik Meijer, 1997. Henk: A Typed Intermediate Language
Lennart Augustsson, 2007. Enklare, lättare! (engelska) Beskrivning av implementeringen av lambda-kubsystem i Haskell.
Lambdakub på SpbHUG (ryska) med Denis Moskvins översättning av avsnittet om lambdakub från boken Henk Barendregt, Lambda Calculi med typer