Yksinkertaisesti kirjoitettu lambda-laskenta

Yksinkertaisesti kirjoitettu lambdalaskenta ( yksinkertainen kirjoitettu lambdalaskenta , lambdalaskenta yksinkertaisilla tyypeillä , järjestelmä $\lambda ^{\rightarrow }$ ) on kirjoitettu lambda -laskentajärjestelmä , jossa erityinen "nuoli"-tyyppi on määritetty lambda-abstraktiolle. Tätä järjestelmää ehdotti Alonzo Church vuonna 1940 [1] . Haskell Curry harkitsi samanlaista järjestelmää lambda -laskua lähellä olevan kombinatorisen logiikan formalismille vuonna 1934 [2] .

Muodollinen kuvaus

Tyyppien ja termien syntaksi

Järjestelmän perusversiossa tyypit muodostetaan muuttujajoukosta käyttämällä yhtä binääriliitekonstruktoria . Perinteisesti kreikkalaisia kirjaimia käytetään tyyppimuuttujille, ja operaattoria pidetään oikea-assosiatiivisena, eli se on lyhenne sanoista . Kreikan aakkosten toisen puoliskon kirjaimia ( , , jne.) käytetään usein merkitsemään mielivaltaisia tyyppejä, ei vain tyyppimuuttujia. $\lambda ^{\rightarrow }$ $\nuoli oikealle$ $\nuoli oikealle$ $\alpha \rightarrow \beta \to \gamma$ $\alpha \rightarrow (\beta \to \gamma )$ $\sigma$ $\tau$

Yksinkertaisesti kirjoitetusta järjestelmästä on kaksi versiota. Jos termeinä käytetään samoja termejä kuin tyypittämättömässä lambda-laskennassa , niin järjestelmää kutsutaan implisiittisesti kirjoitetuksi tai Curry -tyyppiseksi . Jos lambda-abstraktion muuttujat on merkitty tyypeillä, järjestelmää kutsutaan eksplisiittisesti kirjoitetuksi tai kirkkotyyppiseksi . Esimerkkinä tässä on identtinen Curry-tyylinen funktio: , ja Church-tyylinen: . $\lambda x.~x$ $\lambda x\!:\!\alpha .~x$

Vähennyssäännöt

Pelkistyssäännöt eivät eroa tyypittämättömän lambda -kiven säännöistä . -vähennys määritellään korvaamisen kautta $\beeta$

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

$\eta$ -vähennys määritellään seuraavasti

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

Reduktio edellyttää, että muuttuja ei ole vapaa termissä . $\eta$ $x$ $M$

Kontekstien ja väitteiden kirjoittaminen

Konteksti on joukko pilkuilla erotettuja muuttujien kirjoituskäskyjä, esimerkiksi

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

Kontekstit merkitään yleensä isoilla kreikkalaisilla kirjaimilla: . Voit lisätä kontekstiin muuttujan "fresh" tälle kontekstille: jos on kelvollinen konteksti, joka ei sisällä muuttujaa , se on myös kelvollinen konteksti. $\Gamma ,\Delta$ $\Gamma$ $x$ $\Gamma ,x\!:\!\alpha$

Kirjoituslausekkeen yleinen muoto on:

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

Tämä kuuluu seuraavasti: kontekstissa termillä on tyyppi . $\Gamma$ $M$ $\sigma$

Kirjoitussäännöt (kirkon mukaan)

Yksinkertaisesti kirjoitetussa lambda-laskennassa tyyppien määrittäminen termeihin tapahtuu alla olevien sääntöjen mukaisesti.

Axiom. Jos muuttujalle on määritetty tyyppi kontekstissa , sillä on tyyppi kyseisessä kontekstissa . Päätelmäsäännön muodossa: $x$ $\sigma$ $x$ $\sigma$

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

Johdanto sääntö . $\nuoli oikealle$ Jos jossain kontekstissa, laajennettynä lauseella, jossa on tyyppi , termillä on tyyppi , niin mainitussa yhteydessä (ilman ) lambda-abstraktiolla on tyyppi . Päätelmäsäännön muodossa: $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 )}}

poista sääntö . $\nuoli oikealle$ Jos jossain kontekstissa termi on tyyppiä ja termi on tyyppiä , sovellus on tyyppiä . Päätelmäsäännön muodossa: $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}}

Ensimmäisen säännön avulla voit määrittää tyypin vapaille muuttujille määrittämällä ne kontekstissa. Toisen säännön avulla voit kirjoittaa lambda-abstraktion nuolityypillä ja poistaa tämän abstraktion sitoman muuttujan kontekstista. Kolmas sääntö sallii hakemuksen (hakemuksen) kirjoittamisen edellyttäen, että vasemmalla hakijalla on sopiva nuolityyppi.

Esimerkkejä kirkon tyylisistä kirjoitusväitteistä:

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

(aksiooma)

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

(johdanto )

\nuoli oikealle

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

(poisto )

\nuoli oikealle

Ominaisuudet

Yksinkertaisesti tyypitetyllä järjestelmällä on tyyppiturvallisuuden ominaisuus: alle -vähennykset, lambda-termin tyyppi pysyy ennallaan, eikä itse tyypitys häiritse laskennan etenemistä. $\beeta$
Vuonna 1967 William Tait osoitti [3] , että yksinkertaisesti kirjoitetun järjestelmän -reduktiolla on vahva normalisointiominaisuus: mikä tahansa hyväksyttävä termi voidaan pelkistää ainutlaatuiseen normaalimuotoon äärellisen määrän -pelkistysten jälkeen. Tämän seurauksena termien -ekvivalenssi osoittautuu tässä järjestelmässä päätettävissä olevaksi. $\beeta$ $\beeta$ $\beta \eta$
Curry-Howard-isomorfismi yhdistää yksinkertaisesti kirjoitetun lambda-laskennan ns. "minimaaliseen logiikkaan" ( intuitionistisen lauselogiikan fragmentti, joka sisältää vain implikaatiot ): asutetut tyypit ovat täsmälleen tämän logiikan tautologioita, ja termit vastaavat kirjoitettuja todisteita. luonnollisen vähennyksen muodossa.

Muistiinpanot

↑ A. Kirkko. Yksinkertaisen tyyppiteorian muotoilu // J. Symbolinen logiikka. - 1940. - S. 56-68 .
↑ HB Curry. Toiminnallisuus kombinatorisessa logiikassa // Proc Natl Acad Sci USA. - 1934. - S. 584-590 .
↑ W. W. Tait. Äärillisen tyypin I funktionaalisten intensionaaliset tulkinnat // J. Symbolinen logiikka. - 1967. - T. 32 (2) .

Kirjallisuus

Pierce, Benjamin C. Tyypit ja ohjelmointikielet. - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Käännös venäjäksi: Pierce B. Tyypit ohjelmointikielillä. - Dobrosvet , 2012. - 680 s. — ISBN 978-5-7913-0082-9 .
Barendregt, Henk. Lambdacalculi tyypeillä // Tietojenkäsittelytieteen logiikkakäsikirja. - Oxford University Press, 1992. - Vol. II . - S. 117-309 .