Egyszerűen beírt lambda kalkulus

Az egyszerűen begépelt lambda-kalkulus ( egyszerű típusos lambda-kalkulus , lambda-kalkulus egyszerű típusokkal , rendszerrel $\lambda ^{\jobbra }$ ) a típusos lambda-kalkulus rendszere , amelyben egy speciális "nyíl" típus van hozzárendelve egy lambda-absztrakcióhoz. Ezt a rendszert Alonzo Church javasolta 1940-ben [1] . A kombinatorikus logika lambda-számításhoz közeli formalizmusához Haskell Curry 1934- ben egy hasonló rendszert vett figyelembe [2] .

Formai leírás

Típusok és kifejezések szintaxisa

A rendszer alapváltozatában a típusokat változók halmazából állítják össze egyetlen bináris infix konstruktor segítségével . A hagyomány szerint a típusváltozókra görög betűket használnak, az operátort pedig jobb-asszociatívnak tekintik, vagyis a rövidítése . A görög ábécé második feléből származó betűket ( , , stb.) gyakran tetszőleges típusok jelölésére használják, nem csak típusváltozókat. $\lambda ^{\jobbra }$ $\jobb nyíl$ $\jobb nyíl$ $\alpha \rightarrow \beta \to \gamma$ $\alpha \jobbra nyíl (\beta \to \gamma )$ $\sigma$ $\tau$

Az egyszerűen gépelt rendszernek két változata létezik. Ha ugyanazokat a kifejezéseket használjuk kifejezésként, mint a típus nélküli lambda-kalkulusban , akkor a rendszert implicit módon gépeltnek vagy Curry -típusúnak nevezzük . Ha a lambda-absztrakció változói típusokkal vannak ellátva, akkor a rendszert explicit typed -nek vagy Church typed -nek nevezzük . Példaként álljon itt egy azonos Curry-stílusú függvény: , és Church-stílusú: . $\lambda x.~x$ $\lambda x\!:\!\alpha .~x$

Csökkentési szabályok

A redukció szabályai nem különböznek a tipizálatlan lambda kalkulus szabályaitól . -a redukciót helyettesítéssel határozzuk meg $\beta$

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

$\eta$ -csökkentést a következőképpen határozzuk meg

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

A -redukció megköveteli, hogy a változó ne legyen szabad a kifejezésben . $\eta$ $x$ $M$

Kontextusok beírása és állítások típusa

A kontextus vesszővel elválasztott változók beírási utasításainak halmaza, például

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

A szövegkörnyezeteket általában nagy görög betűkkel jelöljük: . Ehhez a kontextushoz hozzáadhat egy „fresh” változót: ha egy érvényes kontextus, amely nem tartalmazza a változót , akkor az is érvényes kontextus. $\Gamma ,\Delta$ $\Gamma$ $x$ $\Gamma ,x\!:\!\alpha$

A gépelési utasítás általános formája a következő:

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

Ez így hangzik: a szövegkörnyezetben egy kifejezés típusa . $\Gamma$ $M$ $\sigma$

Gépelési szabályok (egyház szerint)

Az egyszerűen gépelt lambda kalkulusban a típusok kifejezésekhez való hozzárendelése az alábbi szabályok szerint történik.

Alapigazság. Ha egy változóhoz egy kontextusban típus van hozzárendelve , akkor abban a kontextusban van típusa . Következtetési szabály formájában: $x$ $\sigma$ $x$ $\sigma$

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

Bevezetési szabály . $\jobb nyíl$ Ha valamilyen kontextusban a típust tartalmazó utasítással kibővítve a kifejezésnek típusa van , akkor az említett kontextusban (anélkül ) a lambda absztrakciónak típusa van . Következtetési szabály formájában: $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 )}}

szabály törlése . $\jobb nyíl$ Ha valamilyen kontextusban egy kifejezés típusú és egy kifejezés típusos , akkor az alkalmazás típusos . Következtetési szabály formájában: $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}}

Az első szabály lehetővé teszi, hogy a kontextusban megadva típust rendeljen a szabad változókhoz. A második szabály lehetővé teszi, hogy a lambda absztrakciót nyíltípussal írja be, eltávolítva a kontextusból az ezen absztrakció által kötött változót. A harmadik szabály lehetővé teszi a pályázat (kérelem) beírását, feltéve, hogy a bal oldali pályázó rendelkezik megfelelő nyíltípussal.

Példák az egyházi típusú gépelési állításokra:

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

(alapigazság)

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

(bevezetés )

\jobb nyíl

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

(eltávolítás )

\jobb nyíl

Tulajdonságok

Az egyszerűen tipizált rendszernek megvan a típusbiztonsági tulajdonsága: -redukciók alatt a lambda tag típusa változatlan marad, és maga a tipizálás sem zavarja a számítások menetét. $\beta$
1967-ben William Tait bebizonyította [3] , hogy a -redukció egy egyszerűen tipizált rendszerre erős normalizációs tulajdonsággal rendelkezik: minden megengedett tag egy egyedi normál formára redukálható véges számú -redukció után. Ennek következtében a kifejezések -egyenértékűsége ebben a rendszerben eldönthetőnek bizonyul. $\beta$ $\beta$ $\beta \eta$
A Curry-Howard izomorfizmus az egyszerűen tipizált lambda-számítást az úgynevezett "minimális logikához" kapcsolja (az intuicionista propozicionális logika egy töredéke, amely csak implikációt tartalmaz ): a feltöltött típusok pontosan ennek a logikának a tautológiái, és a kifejezések megfelelnek a nyelvben írt bizonyításoknak. természetes levonás formája.

Jegyzetek

↑ A. templom. A típusok egyszerű elméletének megfogalmazása // J. Szimbolikus logika. - 1940. - S. 56-68 .
↑ HB Curry. Funkcionalitás a kombinatív logikában // Proc Natl Acad Sci USA. - 1934. - S. 584-590 .
↑ W. W. Tait. Az I. véges típusú függvények intenzionális értelmezései // J. Szimbolikus logika. - 1967. - T. 32 (2) .

Irodalom

Pierce, Benjamin C. Típusok és programozási nyelvek. - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Orosz nyelvű fordítás: Pierce B. Típusok programozási nyelvekben. - Dobrosvet , 2012. - 680 p. — ISBN 978-5-7913-0082-9 .
Barendregt, Henk. Lambda kalkulusok típusokkal // Logikai kézikönyv a számítástechnikában. - Oxford University Press, 1992. - II. kötet . - S. 117-309 .