Järjestelmä F

Järjestelmä F ( polymorfinen lambda-laskenta , järjestelmä $\lambda 2$ , toisen asteen tyyppinen lambda-laskenta ) on tyypitetty lambda -laskentajärjestelmä, joka eroaa yksinkertaisesti tyypitetystä järjestelmästä yleisen tyyppien kvantifiointimekanismin läsnäololla . Tämän järjestelmän kehitti vuonna 1972 Jean-Yves Girard [1] logiikan todistusteorian yhteydessä. Hänestä riippumatta samanlaista järjestelmää ehdotti vuonna 1974 John Reynolds [2] . F-järjestelmän avulla voit formalisoida parametrisen polymorfismin käsitteen ohjelmointikielissä ja se toimii teoreettisena perustana sellaisille ohjelmointikielille kuin Haskell ja ML .

Järjestelmä F mahdollistaa termien muodostamisen tyypeistä riippuen. Teknisesti tämä saavutetaan mekanismilla, jossa termi abstraktoidaan tyypin mukaan, mikä johtaa uuteen termiin. Perinteisesti tällaisessa abstraktiossa käytetään suurta lambda-symbolia . Esimerkiksi ottamalla termi tyyppi ja abstraktimalla muuttujan tyypin , saamme termi . Tämä termi on funktio tyypeistä termeihin. Kun tätä funktiota sovelletaan eri tyyppeihin, saamme termejä, joilla on sama rakenne, mutta eri tyyppejä: $\lambda$ $\lambda x^{\alpha }.~x$ $\alpha \to \alpha$ $\alpha$ $\Lambda \alpha .~\lambda x^{\alpha }.~x$

(\Lambda \alpha .~\lambda x^{\alpha }.~x)~{\texttt {Bool}}\ \to _{\beta }\ \lambda x^{\texttt {Bool}} .~x

- tyypin termi ;

{\texttt {Bool}}\to {\texttt {Bool}}

(\Lambda \alpha .~\lambda x^{\alpha }.~x)~{\texttt {Nat))\ \to _{\beta }\ \lambda x^{\texttt {Nat)) .~x

on tyypin termi .

{\texttt {Nat}}\to {\texttt {Nat}}

Voidaan nähdä, että termillä on polymorfinen käyttäytyminen, eli se määrittelee yhteisen rajapinnan eri tietotyypeille. Järjestelmässä F tälle termille annetaan tyyppi . Tyypin yleinen kvantori korostaa mahdollisuutta korvata tyyppimuuttuja mikä tahansa kelvollinen tyyppi . $\Lambda \alpha .~\lambda x^{\alpha }.~x$ $\forall \alpha .~\alpha \to \alpha$ $\alpha$

Muodollinen kuvaus

Kirjoita syntaksi

Järjestelmän F tyypit muodostetaan tyyppimuuttujien joukosta käyttämällä ja -operaattoreita . Perinteisesti kreikkalaisia kirjaimia käytetään tyyppimuuttujina. Tyyppien muodostamista koskevat säännöt ovat seuraavat: $\to$ $\kaikille$

( Tyyppimuuttuja ) If on tyyppimuuttuja, niin on tyyppi; $\alpha$ $\alpha$
( Nuolityyppi ) Jos ja ovat tyyppejä, sitten on tyyppi; $A$ $B$ $(A\–B)$
( Yleinen tyyppi ) If on tyyppimuuttuja ja on tyyppi, niin on tyyppi. $\alpha$ $B$ $(\forall \alpha .~B)$

Ulommat sulut jätetään usein pois, operaattoria pidetään oikea-assosiatiivisena ja operaattorin toiminta jatkuu mahdollisimman pitkälle oikealle. Esimerkiksi on vakiolyhenne sanalle . $\nuoli oikealle$ $\kaikille$ $\forall \alpha .~\forall \beta .~\alpha \to \beta \to \alpha$ $(\forall \alpha .~(\forall \beta .~(\alpha \to (\beta \to \alpha ))))$

Termien syntaksi

Järjestelmän F termit muodostetaan termimuuttujien joukosta ( , , jne.) seuraavien sääntöjen mukaisesti $x$ $y$ $z$

( Muuttuja ) Jos on muuttuja, niin on termi; $x$ $x$
( Abstraktio ) If on muuttuja, on tyyppi ja on termi, niin on termi; $x$ $A$ $M$ $(\lambda x^{A}.~M)$
( Sovellus ) Jos ja ovat termejä, niin on termi; $M$ $N$ ${\näyttötyyli (M~N)}$
( Universal Abstraction ) If on tyyppimuuttuja ja on termi, niin on termi; $\alpha$ $M$ $(\Lambda \alpha .~M)$
( Universal Application ) If on termi ja on tyyppi, niin on termi. $M$ $A$ ${\näyttötyyli (M~A)}$

Ulkosulut jätetään usein pois, molempien sovellusten katsotaan olevan vasen-assosiatiivisia ja abstraktien toiminnan katsotaan jatkuvan mahdollisimman pitkälle oikealle.

Yksinkertaisesti kirjoitetusta järjestelmästä on kaksi versiota. Jos, kuten yllä olevissa säännöissä, lambda-abstraktion termimuuttujat on merkitty tyypeillä, järjestelmän sanotaan olevan kirkon tyyppinen . Jos abstraktiosäännön tilalle tulee

( Abstraktio Curryn mukaan ) If on muuttuja ja on termi, niin on termi, $x$ $M$ $(\lambda x.~M)$

ja hylkää kaksi viimeistä sääntöä, niin järjestelmää kutsutaan Curry-tyyppiseksi . Itse asiassa Curry-tyyppisen järjestelmän ehdot ovat samat kuin tyypittämättömässä lambda-laskennassa.

Vähennyssäännöt

Lambda -kiven standardin vähennyssäännön lisäksi $\beeta$

(\lambda a^{A}.~M)~N\ \to _{\beta }\ M[a:=N]

Kirkkotyyppinen järjestelmä F tuo lisäsäännön,

(\Lambda \alpha .~M)~A\ \to _{\beta }\ M[\alpha :=A]

mahdollistaa termin soveltamisen tyyppiin laskemisen tyyppikorvausmekanismin avulla tyyppimuuttujan sijaan.

Kontekstien kirjoittaminen ja väitteen kirjoittaminen

Konteksti, kuten yksinkertaisesti kirjoitetussa lambda-laskennassa , on joukko lauseita eri muuttujien tyyppien määrittämisestä, erotettuna pilkulla

\Gamma =x_{1}\!:\!A_{1},x_{2}\!:\!A_{1},\ldots ,x_{n}\!:\!A_{n}

Voit lisätä kontekstiin muuttujan "fresh" tälle kontekstille: jos on kelvollinen konteksti, joka ei sisällä muuttujaa , ja on tyyppi, se on myös kelvollinen konteksti. $\Gamma$ $x$ $B$ $\Gamma ,x\!:\!B$

Kirjoituslausekkeen yleinen muoto on:

\Gamma \vdash M\!:\!A

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

Kirkon kirjoitussäännöt

Kirkon tyyppisessä järjestelmässä F tyyppien määrittäminen termeille tapahtuu seuraavien sääntöjen mukaisesti:

( Alkusääntö ) Jos muuttuja esiintyy tyypin kanssa kontekstissa , sillä on tyyppi kyseisessä kontekstissa . Päätelmäsäännön muodossa $x$ $A$ $\Gamma$ $x$ $A$

{\displaystyle {x\!:\!A\in \Gamma } \over {\Gamma \vdash x\!:\!A))

( Johdannon sääntö $\nuoli oikealle$ ) Jos jossain kontekstissa, jota laajennetaan lauseella, jolla on tyyppi , termillä on tyyppi , niin mainitussa yhteydessä (ilman ) lambda-abstraktiolla on tyyppi . Päätelmäsäännön muodossa $a$ $A$ $M$ $B$ $a$ $\lambda a^{A}.~M$ $A:sta B:hen$

{\Gamma ,a\!:\!A\vdash M\!:\!B} \over {\Gamma \vdash (\lambda a^{A}.~M)\!:\!(A \to B)}

( Poistosääntö $\nuoli oikealle$ ) Jos jossain kontekstissa termillä on tyyppi ja termillä on tyyppi , sovelluksella on tyyppi . Päätelmäsäännön muodossa $M$ $A:sta B:hen$ $N$ $A$ $M~N$ $B$

{\Gamma \vdash M\!:\!(A\to B)\quad \Gamma \vdash N\!:\!A} \over {\Gamma \vdash (M~N)\!:\ !B}

( Johdannon sääntö $\kaikille$ ) Jos jossain kontekstissa termillä on tyyppi , niin siinä yhteydessä termillä on tyyppi . Päätelmäsäännön muodossa $M$ $A$ $\Lambda \alpha .~M$ $\forall \alpha .~A$

{\displaystyle {\Gamma \vdash M\!:\!A} \over {\Gamma \vdash (\Lambda \alpha .~M)\!:\!(\forall \alpha .~A)))

Tämä sääntö edellyttää varoituksen: tyyppimuuttujaa ei saa esiintyä kontekstikirjoitusväitteissä . $\alpha$ $\Gamma$

( Poistosääntö $\kaikille$ ) Jos jossain kontekstissa termillä on tyyppi ja se on tyyppi, niin tässä yhteydessä termillä on tyyppi . Päätelmäsäännön muodossa $M$ $\forall \alpha .~A$ $B$ $M~B$ $A[\alpha :=B]$

{\Gamma \vdash M\!:\!(\forall \alpha .~A)} \over {\Gamma \vdash (M~B)\!:\!(A[\alpha :=B] )}

Curryn kirjoitussäännöt

Curry-tyyppisessä järjestelmässä F tyyppien määrittäminen termeille tapahtuu seuraavien sääntöjen mukaisesti:

( Alkusääntö ) Jos muuttuja esiintyy tyypin kanssa kontekstissa , sillä on tyyppi kyseisessä kontekstissa . Päätelmäsäännön muodossa $x$ $A$ $\Gamma$ $x$ $A$

{\displaystyle {x\!:\!A\in \Gamma } \over {\Gamma \vdash x\!:\!A))

{\Gamma ,a\!:\!A\vdash M\!:\!B} \over {\Gamma \vdash (\lambda a.~M)\!:\!(A\-B) }

{\Gamma \vdash M\!:\!(A\to B)\quad \Gamma \vdash N\!:\!A} \over {\Gamma \vdash (M~N)\!:\ !B}

( Johdannon sääntö $\kaikille$ ) Jos termillä on jossain kontekstissa tyyppi , niin tässä yhteydessä tälle termille voidaan myös määrittää tyyppi . Päätelmäsäännön muodossa $M$ $A$ $M$ $\forall \alpha .~A$

{\displaystyle {\Gamma \vdash M\!:\!A} \over {\Gamma \vdash M\!:\!(\forall \alpha .~A)))

Tämä sääntö edellyttää varoituksen: tyyppimuuttujaa ei saa esiintyä kontekstikirjoitusväitteissä . $\alpha$ $\Gamma$

( Poistosääntö $\kaikille$ ) Jos jossain kontekstissa termillä on tyyppi ja se on tyyppi, niin tässä yhteydessä tälle termille voidaan myös määrittää tyyppi . Päätelmäsäännön muodossa $M$ $\forall \alpha .~A$ $B$ $M$ $A[\alpha :=B]$

{\displaystyle {\Gamma \vdash M\!:\!(\forall \alpha .~A)} \over {\Gamma \vdash M\!:\!(A[\alpha :=B])))

Esimerkki. Alkuperäisen säännön mukaan:

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

Sovelletaan poistosääntöä tyypiksi $\kaikille$ $B$ $\forall \alpha .~\alpha \to \alpha$

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

Nyt meillä on poistosäännön mukaan mahdollisuus soveltaa termiä itseensä $\nuoli oikealle$ $x$

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

ja lopuksi käyttöönottosäännön mukaan $\nuoli oikealle$

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

Tämä on esimerkki termistä, joka kirjoitetaan järjestelmässä F, mutta ei yksinkertaisesti kirjoitetussa järjestelmässä .

Tietotyyppien esitys

Järjestelmä F on riittävän ilmeikäs toteuttamaan suoraan monet ohjelmointikielissä käytetyt tietotyypit. Työskentelemme kirkon F-järjestelmän versiossa.

Tyhjä tyyppi. Tyyppi

\bot \ \equiv \ \forall \alpha .~\alpha

on asumaton järjestelmässä F, eli siinä ei ole tämän tyypin termejä.

Yksi tyyppi. Y tyyppi

\top \ \equiv \ \forall \alpha .~\alpha \to \alpha

järjestelmässä F on yksi normaalimuotoinen asukas, termi

{\mathtt {id}}\ \equiv \ \Lambda \alpha .~\lambda x^{\alpha }.~x

boolen tyyppi. Järjestelmässä F annetaan seuraavasti:

{\mathtt {Bool))\ \equiv \ \forall \alpha .~\alpha \to \alpha \to \alpha

Tällä tyypillä on täsmälleen kaksi asukasta, jotka tunnistetaan kahdella Boolen vakiolla

{\mathtt {true))\ \equiv \ \Lambda \alpha .~\lambda x^{\alpha }.~\lambda y^{\alpha }.~x

{\mathtt {false))\ \equiv \ \Lambda \alpha .~\lambda x^{\alpha }.~\lambda y^{\alpha }.~y

Ehdollinen operaattorirakenne

{\mathtt {ifThenElse}}\ \equiv \ \Lambda \alpha .~\lambda b^{\mathtt {Bool)).~\lambda x^{\alpha }.~\lambda y^{\alpha }.~b\,\alpha \,x\,y

Tämä toiminto täyttää luonnolliset vaatimukset

{\mathtt {ifThenElse}}\,A\,{\mathtt {true}}\,M\,N=M

{\mathtt {ifThenElse}}\,A\,{\mathtt {false}}\,M\,N=N

mielivaltaiselle tyypille ja mielivaltaiselle ja . Tämä on helppo varmistaa laajentamalla määritelmiä ja tekemällä -vähennyksiä. $A$ $M\!:\!A$ $N\!:\!A$ $\beeta$

Taideteoksen tyyppi. Satunnaisille tyypeille ja niiden karteesisen tuotteen tyypille $A$ $B$

A\times B~\equiv ~\forall \alpha .~(A\to B\to \alpha )\to \alpha

pariskunta asuu

\langle M;N\rangle ~\equiv ~\Lambda \alpha .~\lambda f^{(A\to B\to \alpha )}.~f~M~N

jokaiselle ja . Parin projektiot saadaan funktioilla $M\!:\!A$ $N\!:\!B$

{\mathtt {fst))\ \equiv \ \Lambda \alpha .~\Lambda \beta .~\lambda p^{\alpha \times \beta }.~p\,\alpha \,(\lambda x^{\alpha }.\,\lambda y^{\beta }.\,x)~:~\forall \alpha .~\forall \beta .\,\alpha \times \beta \to \alpha

{\mathtt {snd))\ \equiv \ \Lambda \alpha .~\Lambda \beta .~\lambda p^{\alpha \times \beta }.~p\,\beta \,(\lambda x^{\alpha }.\,\lambda y^{\beta }.\,y)~:~\forall \alpha .~\forall \beta .\,\alpha \times \beta \to \beta

Nämä toiminnot täyttävät ja luontaiset vaatimukset . ${\mathtt {fst}}\,A\,B\,\langle M;N\rangle =M$ ${\mathtt {snd}}\,A\,B\,\langle M;N\rangle =N$

Summatyyppi. Satunnaisille tyypeille ja niiden summan tyypille $A$ $B$

A+B~\equiv ~\forall \alpha .~(A\to \alpha )\to (B\to \alpha )\to \alpha

täytetään joko termillä tyyppi , tai termillä tyyppi , käytetystä rakentajasta riippuen $A$ $B$

{\mathtt {injL}}\,M~\equiv ~\Lambda \alpha .\,\lambda f^{A\to \alpha }.\,\lambda g^{B\to \alpha }. \,f\,M

{\mathtt {injR}}\,N~\equiv ~\Lambda \alpha .\,\lambda f^{A\to \alpha }.\,\lambda g^{B\to \alpha }. \,g\,N

Täällä ,. _ Toiminnolla, joka suorittaa tapausten jäsentämisen (kuvion täsmäytyksen), on muoto $M\!:\!A$ $N\!:\!B$

{\mathtt {match}}~\equiv ~\Lambda \alpha .\,\Lambda \beta .\,\Lambda \gamma .\,\lambda s^{\alpha +\beta }.\,\ lambda f^{\alpha \to \gamma }.\,\lambda g^{\beta \to \gamma }.\,s\,\gamma \,f\,g~:~\forall \alpha .~\ kaikille \beta .~\forall \gamma .~\alpha +\beta \to (\alpha \to \gamma )\to (\beta \to \gamma )\to \gamma

Tämä toiminto täyttää seuraavat luonnolliset vaatimukset

{\mathtt {match}}\,A\,B\,C\,({\mathtt {injL}}\,M)\,F\,G=F\,M

{\mathtt {match}}\,A\,B\,C\,({\mathtt {injR}}\,N)\,F\,G=G\,N

mielivaltaisille tyypeille ja ja mielivaltaisille termeille ja . $A$ $B$ $C$ $F\!:\!A\to C$ $G\!:\!B\to C$

Kirkon numerot. Luonnollisten lukujen tyyppi järjestelmässä F

{\mathtt {Nat))\ \equiv \ \forall \alpha .~\alpha \to (\alpha \to \alpha )\to \alpha

jossa on ääretön määrä erilaisia elementtejä, jotka on saatu kahdella konstruktorilla ja : ${\mathtt {zero}}\!:\!{\mathtt {Nat}}$ ${\mathtt {succ}}\!:\!{\mathtt {Nat}}\to {\mathtt {Nat}}$

{\mathtt {nolla))\ \equiv \ \Lambda \alpha .\,\lambda z^{\alpha }.\,\lambda s^{\alpha \to \alpha }.\,z

{\mathtt {succ}}\ \equiv \ \lambda n^{\mathtt {Nat)).\,\Lambda \alpha .\,\lambda z^{\alpha }.\,\lambda s^ {\alpha \to \alpha }.\,s\,(n\,\alpha \,z\,s)

Luonnollinen luku saadaan käyttämällä toista konstruktoria - kertaa ensimmäiseen tai vastaavasti termillä $n$ $n$

{\overline {n))\ \equiv \ \Lambda \alpha .\,\lambda z^{\alpha }.\,\lambda s^{\alpha \rightarrow \alpha }.\,\alleviivaus { s(s(s\ldots (s} _{n}\,z)\ldots ))

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$

Jean-Yves Girard osoitti väitöskirjassaan [1] , että järjestelmällä F on vahva normalisointiominaisuus: mikä tahansa hyväksyttävä termi voidaan pelkistää ainutlaatuiseen normaalimuotoon äärellisen määrän -pelkistysten jälkeen. $\beeta$

F-järjestelmä on impredikatiivinen järjestelmä, koska yleistä tyyppiä määriteltäessä yleiseen kvantoriin liittyvä tyyppimuuttuja voidaan korvata määriteltävällä objektilla itsellään. Esimerkiksi yksittäistä tyyppiä olevaa termiä voidaan soveltaa sen omaan tyyppiin, jolloin saadaan termi tyyppi . Kuten Joe Wells osoitti vuonna 1994 [3] , Curryn System F -version tyyppipäätelmän ongelma on ratkaisematon. Siksi ohjelmointikielten käytännön toteutuksessa käytetään yleensä polymorfismin rajoitettuja predikatiivisia versioita: prenex-polymorfismi ( ML - tyylinen polymorfismi ), 2-luokan polymorfismi jne. Prenex-polymorfismin tapauksessa tyyppimuuttujien laajuus on vain tyypit ilman kvantoreita. Näissä järjestelmissä tyyppipäätelmän ongelma on ratkaistavissa, tällainen päättely perustuu Hindley-Milner-algoritmiin . ${\texttt {id}}$ $\top \equiv \forall \alpha .~\alpha \to \alpha$ $\top \to \top$

Curry-Howard-vastaavuus linkittää järjestelmän F minimaaliseen toisen asteen intuitionistiseen lauselogiikkaan konstruoitu propositionaalisista muuttujista implikaatiolla ja universaalilla propositiokvantifioinnilla Tässä tapauksessa arvot (tosi), (epätosi), konnektiivit (negaatio), (konjunktio) ja (disjunktio) sekä (olemassaolokvantioija) voidaan määritellä seuraavasti $\top$ $\bot$ $\lei$ $\maa$ $\lor$ $\olemassa$

\top ~\equiv ~\forall \alpha .\,\alpha \to \alpha

\bot ~\equiv ~\forall \alpha .\,\alpha

\lnot A~\equiv ~A\to \bot

A\land B~\equiv ~\forall \alpha .\,(A\to B\to \alpha )\to \alpha

A\tai B~\equiv ~\forall \alpha .\,(A\to \alpha )\to (B\to \alpha )\to \alpha

\exists \alpha .\,M[\alpha ]~\equiv ~\forall \gamma .\,(\forall \alpha .\,M[\alpha ]\to \gamma )\to \gamma

Huomaa, että Curry-Howard-vastaavuus määrittää tosi yhden tyypin, false tyhjän tyypin, konjunktio tyyppien tulon ja disjunktio niiden summan.

Muistiinpanot

↑ 1 2 Girard, Jean-Yves. Tulkinta fonctionnelle et elimination des coupures de l'aritmetique d'ordre supérieur : Ph.D. opinnäytetyö. — Université Paris 7, 1972.
↑ John C. Reynolds. Kohti tyyppirakenteen teoriaa . - 1974. Arkistoitu 31. lokakuuta 2014.
↑ Wells JB Typability ja tyypin tarkistus toisen asteen lambda-laskennassa ovat samanarvoisia ja ratkaisemattomia // Proceedings of 9th Annual IEEE Symposium on Logic in Computer Science (LICS). - 1994. - S. 176-185 . Arkistoitu alkuperäisestä 22. helmikuuta 2007.

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 .
Jean-Yves Girard, Paul Taylor, Yves Lafont. Todisteet ja tyypit . - Cambridge University Press , 1989. - ISBN 0 521 37181 3 .