Jednoduše zadaný lambda kalkul

Jednoduše typovaný lambda kalkul ( simple typed lambda calculus , lambda kalkulus s jednoduchými typy , system $\lambda ^{\rightarrow }$ ) je systém typovaného lambda kalkulu , ve kterém je lambda abstrakci přiřazen speciální typ "šipka". Tento systém navrhl Alonzo Church v roce 1940 [1] . Pro formalismus kombinatorické logiky blízko lambda kalkulu uvažoval o podobném systému Haskell Curry v roce 1934 [2] .

Formální popis

Syntaxe typů a termínů

V základní verzi systému jsou typy konstruovány ze sady proměnných pomocí jediného konstruktoru binárních infixů . Podle tradice se pro typové proměnné používají řecká písmena a operátor je považován za asociativní vpravo, to znamená, že jde o zkratku pro . Písmena z druhé poloviny řecké abecedy ( , , atd.) se často používají k označení libovolných typů, nejen typových proměnných. $\lambda ^{\rightarrow }$ $\šipka doprava$ $\šipka doprava$ $\alpha \rightarrow \beta \to \gamma$ $\alpha \rightarrow (\beta \to \gamma )$ $\sigma$ $\tau$

Existují dvě verze jednoduchého systému. Pokud jsou jako termíny použity stejné termíny jako v netypovém lambda kalkulu , pak se systém nazývá implicitně typovaný nebo psaný Currym . Pokud jsou proměnné v lambda abstrakci označeny typy, pak se systém nazývá explicitně typovaný nebo Church typed . Jako příklad uvádíme identickou funkci ve stylu Curry: a Church-style: . $\lambda x.~x$ $\lambda x\!:\!\alpha .~x$

Pravidla snížení

Pravidla pro redukci se neliší od pravidel pro netypizovaný počet lambda . -redukce je definována prostřednictvím substituce $\beta$

(\lambda x\!:\!\sigma .~M)~N\ \to _{{\beta }}\ M[x:=N]

$\eta$ -snížení je definováno následovně

\lambda x\!:\!\sigma .~M~x\ \to _({\eta }}\ M

-redukce vyžaduje, aby proměnná nebyla v termínu volná . $\eta$ $X$ $M$

Kontexty psaní a výrazy typu

Kontext je sada příkazů pro psaní proměnných oddělených čárkami, např.

f\!:\!(\beta \to \gamma ),g\!:\!(\alpha \to \beta ),x\!:\!\alpha

Kontexty se obvykle označují velkými řeckými písmeny: . Pro tento kontext můžete do kontextu přidat proměnnou „fresh“: pokud je platný kontext, který neobsahuje proměnnou , pak je to také platný kontext. $\Gamma ,\Delta$ $\Gamma$ $X$ $\Gamma ,x\!:\!\alfa$

Obecná forma typizačního příkazu je:

\Gamma \vdash M\!:\!\sigma

To zní následovně: v kontextu má výraz typ . $\Gamma$ $M$ $\sigma$

Pravidla psaní (podle Churche)

V jednoduše zadaném lambda kalkulu se přiřazování typů termínům provádí podle níže uvedených pravidel.

Axiom. Pokud je proměnné přiřazen typ v kontextu , pak má v tomto kontextu typ . Ve formě odvozovacího pravidla: $X$ $\sigma$ $X$ $\sigma$

{{x\!:\!\sigma \in \Gamma } \over {\Gamma \vdash x\!:\!\sigma ))

Úvodní pravidlo . $\šipka doprava$ Pokud v nějakém kontextu, rozšířeném o příkaz, který má typ , má výraz typ , pak ve zmíněném kontextu (bez ) má lambda abstrakce typ . Ve formě odvozovacího pravidla: $X$ $\sigma$ $M$ $\tau$ $X$ $\lambda x\!:\!\sigma .~M$ $\sigma \to \tau$

{{\Gamma ,x\!:\!\sigma \vdash M\!:\!\tau } \over {\Gamma \vdash (\lambda x\!:\!\sigma .~M)\!:\ !(\sigma \to \tau )}}

odstranit pravidlo . $\šipka doprava$ Pokud je v nějakém kontextu termín typu a termín je typu , pak je aplikace typu . Ve formě odvozovacího pravidla: $M$ $\sigma \to \tau$ $N$ $\sigma$ $M~N$ $\tau$

{{\Gamma \vdash M\!:\!(\sigma \to \tau )\quad \Gamma \vdash N\!:\!\sigma } \over {\Gamma \vdash (M~N)\!: \!\tau}}

První pravidlo umožňuje přiřadit typ volným proměnným jejich zadáním v kontextu. Druhé pravidlo vám umožňuje zadat abstrakci lambda pomocí typu šipky, čímž se z kontextu odstraní proměnná vázaná touto abstrakcí. Třetí pravidlo umožňuje napsat žádost (přihlášku) za předpokladu, že levý žadatel má vhodný typ šipky.

Příklady tvrzení o psaní v církevním stylu:

x\!:\!\alpha \vdash x\!:\!\alpha

(axiom)

\vdash (\lambda x\!:\!\alpha .~x)\!:\!(\alpha \to \alpha )

(úvod )

\šipka doprava

f\!:\!(\beta \to \gamma \to \delta ),y\!:\!\beta \vdash (f~y)\!:\!(\gamma \to \delta )

(odstranění )

\šipka doprava

Vlastnosti

Jednoduše typovaný systém má vlastnost typové bezpečnosti: pod -redukcí zůstává typ lambda termínu nezměněn a samotné psaní neruší průběh výpočtů. $\beta$
V roce 1967 William Tait dokázal [3] , že -redukce pro jednoduše typizovaný systém má silnou normalizační vlastnost: jakýkoli přípustný člen může být redukován na jedinečnou normální formu po konečném počtu -redukcí. V důsledku toho se ukazuje, že ekvivalence pojmů je v tomto systému rozhoditelná. $\beta$ $\beta$ $\beta \eta$
Curry-Howardův izomorfismus spojuje jednoduše typizovaný lambda kalkul s takzvanou „minimální logikou“ (fragment intuicionistické výrokové logiky , který zahrnuje pouze implikaci ): zalidněné typy jsou přesně tautologiemi této logiky a termíny odpovídají důkazům zapsaným v formou přirozené dedukce.

Poznámky

↑ A. Kostel. Formulace jednoduché teorie typů // J. Symbolická logika. - 1940. - S. 56-68 .
↑ HB Curry. Funkčnost v kombinační logice // Proc Natl Acad Sci USA. - 1934. - S. 584-590 .
↑ W. W. Tait. Intenzionální interpretace funkcionálů konečného typu I // J. Symbolická logika. - 1967. - T. 32 (2) .

Literatura

Pierce, Benjamin C. Typy a programovací jazyky. - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Překlad do ruštiny: Pierce B. Typy v programovacích jazycích. - Dobrosvet , 2012. - 680 s. — ISBN 978-5-7913-0082-9 .
Barendregt, Henk. Lambda Calculi s typy // Handbook of Logic in Computer Science. - Oxford University Press, 1992. - Svazek II . - S. 117-309 .