Sistemul F

Sistemul F ( calcul lambda polimorf , sistem $\lambda 2$ , calcul lambda tipizat de ordinul doi ) este un sistem de calcul lambda tipizat care diferă de un sistem tipizat simplu prin prezența unui mecanism universal de cuantificare asupra tipurilor. Acest sistem a fost dezvoltat în 1972 de Jean-Yves Girard [1] în contextul teoriei demonstrației în logică. Independent de el, un sistem similar a fost propus în 1974 de John Reynolds [2] . Sistemul F vă permite să formalizați conceptul de polimorfism parametric în limbaje de programare și servește drept bază teoretică pentru astfel de limbaje de programare precum Haskell și ML .

Sistemul F permite construirea termenilor în funcție de tipuri. Din punct de vedere tehnic, acest lucru se realizează prin mecanismul abstracției unui termen după tip, care are ca rezultat un nou termen. În mod tradițional, pentru o astfel de abstractizare, se folosește simbolul lambda mare . De exemplu, luând un termen de tip și făcând abstracție peste o variabilă de tip , obținem termen . Acest termen este o funcție de la tipuri la termeni. Aplicând această funcție la diferite tipuri, vom obține termeni cu structură identică, dar tipuri diferite: $\lambda$ $\lambda x^{\alpha }.~x$ $\alpha \to \alpha$ $\alfa$ $\Lambda \alpha .~\lambda x^{\alpha }.~x$

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

- termenul tipului ;

{\texttt {Bool}}\la {\texttt {Bool}}

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

este un termen de tip .

{\texttt {Nat}}\la {\texttt {Nat}}

Se poate observa că termenul are comportament polimorf, adică definește o interfață comună pentru diferite tipuri de date. În sistemul F, acestui termen i se atribuie tipul . Cuantificatorul universal dintr-un tip subliniază posibilitatea de a înlocui orice tip valid pentru o variabilă de tip. $\Lambda \alpha .~\lambda x^{\alpha }.~x$ $\forall \alpha .~\alpha \to \alpha$ $\alfa$

Descriere formală

Introduceți sintaxa

Tipurile de sistem F sunt construite dintr-un set de variabile de tip folosind operatorii și . Prin tradiție, literele grecești sunt folosite pentru variabilele de tip. Regulile pentru formarea tipurilor sunt următoarele: $\la$ $\pentru toți$

( Variabila de tip ) Dacă este o variabilă de tip, atunci este un tip; $\alfa$ $\alfa$
( Tip săgeată ) Dacă și sunt tipuri, atunci este un tip; $A$ $B$ $(A\la B)$
( Tipul generic ) Dacă este o variabilă de tip și este un tip, atunci este un tip. $\alfa$ $B$ $(\forall \alpha .~B)$

Parantezele exterioare sunt adesea omise, operatorul este considerat drept asociativ, iar acțiunea operatorului continuă pe cât posibil spre dreapta. De exemplu, este abrevierea standard pentru . $\sageata dreapta$ $\pentru toți$ $\forall \alpha .~\forall \beta .~\alpha \to \beta \to \alpha$ $(\forall \alpha .~(\forall \beta .~(\alpha \to (\beta \to \alpha ))))$

Sintaxa termenilor

Termenii sistemului F sunt construiți dintr-un set de variabile de termen ( , , etc.) conform următoarelor reguli $X$ $y$ $z$

( Variabilă ) Dacă este o variabilă, atunci este un termen; $X$ $X$
( Abstracție ) Dacă este o variabilă, este un tip și este un termen, atunci este un termen; $X$ $A$ $M$ $(\lambda x^{A}.~M)$
( Aplicație ) Dacă și sunt termeni, atunci este un termen; $M$ $N$ $(M ~ N)$
( Abstracția universală ) Dacă este o variabilă de tip și este un termen, atunci este un termen; $\alfa$ $M$ $(\Lambda \alpha .~M)$
( Aplicație universală ) Dacă este un termen și este un tip, atunci este un termen. $M$ $A$ $(M~A)$

Parantezele exterioare sunt adesea omise, ambele tipuri de aplicații sunt considerate a fi asociate la stânga, iar acțiunea abstracțiilor este considerată a continua spre dreapta pe cât posibil.

Există două versiuni ale sistemului simplu tastat. Dacă, ca în regulile de mai sus, termenii variabile din abstracția lambda sunt adnotați cu tipuri, atunci se spune că sistemul este tip Church . Dacă regula de abstractizare este înlocuită cu

( Abstracția după Curry ) Dacă este o variabilă și este un termen, atunci este un termen, $X$ $M$ $(\lambda x.~M)$

și aruncați ultimele două reguli, apoi sistemul se numește Curry-typed . De fapt, termenii sistemului de tip Curry sunt aceiași cu cei din calculul lambda netipizat.

Reguli de reducere

În plus față de regula standard de reducere pentru calculul lambda $\beta$

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

Sistemul în stil bisericesc F introduce o regulă suplimentară,

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

permițând calcularea aplicării unui termen la un tip prin mecanismul substituției de tip în locul unei variabile de tip.

Contexte de tastare și afirmație de tip

Contextul, ca și în calculul lambda tip simplu , este un set de instrucțiuni despre atribuirea de tipuri diferitelor variabile, separate prin virgulă

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

Puteți adăuga o variabilă „proaspătă” pentru acest context în context: dacă este un context valid care nu conține variabila și este un tip, atunci este și un context valid. $\Gamma$ $X$ $B$ $\Gamma ,x\!:\!B$

Forma generală a unei instrucțiuni de tastare este:

\Gamma \vdash M\!:\!A

Acesta se citește după cum urmează: în context, un termen are tipul . $\Gamma$ $M$ $A$

Reguli de tastare în biserică

În sistemul F tip biserică, atribuirea tipurilor la termeni se face conform următoarelor reguli:

( Regulă inițială ) Dacă o variabilă este prezentă cu un tip într-un context , atunci are un tip în acel context . Sub forma unei reguli de inferență $X$ $A$ $\Gamma$ $X$ $A$

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

( Regula de introducere $\sageata dreapta$ ) Dacă într-un context extins prin declarația care are tip , termenul are tip , atunci în contextul menționat (fără ), abstracția lambda are tip . Sub forma unei reguli de inferență $A$ $A$ $M$ $B$ $A$ $\lambda a^{A}.~M$ $A la B$

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

( Regula de eliminare $\sageata dreapta$ ) Dacă într-un anumit context un termen are un tip și un termen are un tip , atunci aplicația are un tip . Sub forma unei reguli de inferență $M$ $A la B$ $N$ $A$ $M~N$ $B$

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

( Regulă de introducere $\pentru toți$ ) Dacă într - un anumit context un termen are un tip , atunci în acel context termenul are un tip . Sub forma unei reguli de inferență $M$ $A$ $\Lambda \alpha .~M$ $\forall \alpha .~A$

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

Această regulă necesită o avertizare: o variabilă de tip nu trebuie să apară în aserțiunile de tastare în context . $\alfa$ $\Gamma$

( Regula de eliminare $\pentru toți$ ) Dacă într-un anumit context un termen are tip și este un tip, atunci în acest context termenul are tip . Sub forma unei reguli de inferență $M$ $\forall \alpha .~A$ $B$ $M~B$ $A[\alpha :=B]$

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

Regulile de tastare ale lui Curry

În sistemul de tip Curry F, atribuirea tipurilor la termeni se face conform următoarelor reguli:

( Regulă inițială ) Dacă o variabilă este prezentă cu un tip într-un context , atunci are un tip în acel context . Sub forma unei reguli de inferență $X$ $A$ $\Gamma$ $X$ $A$

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

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

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

( Regula de introducere $\pentru toți$ ) Dacă într-un anumit context un termen are un tip , atunci în acest context acestui termen i se poate atribui și un tip . Sub forma unei reguli de inferență $M$ $A$ $M$ $\forall \alpha .~A$

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

Această regulă necesită o avertizare: o variabilă de tip nu trebuie să apară în aserțiunile de tastare în context . $\alfa$ $\Gamma$

( Regula de eliminare $\pentru toți$ ) Dacă, într-un anumit context, un termen are tip și este un tip, atunci în acest context acestui termen i se poate atribui și tipul . Sub forma unei reguli de inferență $M$ $\forall \alpha .~A$ $B$ $M$ $A[\alpha :=B]$

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

Exemplu. Conform regulii initiale:

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

Să aplicăm regula de eliminare , luând drept tip $\pentru toți$ $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 )

Acum, conform regulii de înlăturare , avem posibilitatea de a aplica termenul în sine $\sageata dreapta$ $X$

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

iar în final, conform regulii de introducere $\sageata dreapta$

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

Acesta este un exemplu de termen tastat în Sistemul F, dar nu într- un sistem simplu tastat .

Reprezentarea tipurilor de date

Sistemul F este suficient de expresiv pentru a implementa direct multe dintre tipurile de date utilizate în limbajele de programare. Vom lucra în versiunea Church a sistemului F.

Tip gol. Tip de

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

este nelocuită în sistemul F, adică nu există termeni cu acest tip în el.

Un singur tip. tip Y

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

sistemul F are un singur locuitor de formă normală, termen

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

tip boolean. În sistemul F este dat după cum urmează:

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

Acest tip are exact doi locuitori, identificați cu două constante booleene

{\mathtt {adevărat)}\ \equiv \ \Lambda \alpha .~\lambda x^{\alpha }.~\lambda y^{\alpha }.~x

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

Construcția operatorului condiționat

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

Această funcție satisface cerințele naturale

{\mathtt {ifThenElse}}\,A\,{\mathtt {adevărat}}\,M\,N=M

și

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

pentru un tip arbitrar și arbitrar și . Este ușor de verificat acest lucru prin extinderea definițiilor și efectuând -reduceri. $A$ $M\!:\!A$ $N\!:\!A$ $\beta$

Tipul operei de artă. Pentru tipurile arbitrare și tipul produsului cartezian al acestora $A$ $B$

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

locuit de un cuplu

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

pentru fiecare și . Proiecțiile unei perechi sunt date de funcții $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

Aceste funcții satisfac cerințele naturale ale și . ${\mathtt {fst}}\,A\,B\,\langle M;N\rangle =M$ ${\mathtt {snd}}\,A\,B\,\langle M;N\rangle =N$

Tipul sumei. Pentru tipurile arbitrare și tipul sumei lor $A$ $B$

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

populat fie de un termen de tip , fie de un termen de tip , în funcție de constructorul aplicat $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

Aici , . Funcția care realizează analizarea majusculelor (potrivirea modelului) are forma $M\!:\!A$ $N\!:\!B$

{\mathtt {potrivire}}~\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 .~\ forall \beta .~\forall \gamma .~\alpha +\beta \to (\alpha \to \gamma )\to (\beta \to \gamma )\to \gamma

Această funcție satisface următoarele cerințe naturale

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

și

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

pentru tipuri arbitrare și și termeni arbitrari și . $A$ $B$ $C$ $F\!:\!A\la C$ $G\!:\!B\la C$

Numerele bisericii. Tipul numerelor naturale în sistemul F

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

locuit de un număr infinit de elemente diferite, obținute prin doi constructori și : ${\mathtt {zero}}\!:\!{\mathtt {Nat}}$ ${\mathtt {succ}}\!:\!{\mathtt {Nat}}\la {\mathtt {Nat}}$

{\mathtt {zero)}\\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 \la \alpha }.\,s\,(n\,\alpha \,z\,s)

Un număr natural poate fi obținut prin aplicarea celui de-al doilea constructor - ori la primul sau, echivalent, reprezentat printr-un termen $n$ $n$

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

Proprietăți

Un sistem tip simplu are proprietatea siguranței de tip: sub -reduceri, tipul termenului lambda rămâne neschimbat, iar tastarea în sine nu interferează cu progresul calculelor. $\beta$

În disertația sa, Jean-Yves Girard a arătat [1] că sistemul F are proprietatea de normalizare puternică: orice termen admisibil poate fi redus la o formă normală unică după un număr finit de reduceri. $\beta$

Sistemul F este un sistem impredicativ , deoarece variabila de tip asociată cuantificatorului universal la definirea unui tip generic poate fi înlocuită cu obiectul care este definit în sine. De exemplu, un singur termen de tip poate fi aplicat propriului său tip, producând un termen de tip . După cum a arătat Joe Wells în 1994 [3] , problema inferenței de tip pentru versiunea lui Curry a Sistemului F este de nerezolvat. Prin urmare, în implementarea practică a limbajelor de programare, se folosesc de obicei versiuni limitate, predicative ale polimorfismului: polimorfism preex (polimorfism stil ML ), polimorfism de rang 2 etc. În cazul polimorfismului preex, domeniul de aplicare al variabilelor de tip este doar tipurile fără cuantificatori. În aceste sisteme, problema inferenței de tip este rezolvabilă, o astfel de inferență se bazează pe algoritmul Hindley-Milner . ${\texttt {id}}$ $\top \equiv \forall \alpha .~\alpha \to \alpha$ $\top \to \top$

Corespondența Curry-Howard leagă sistemul F de logica propozițională intuiționistă minimă de ordinul doi construite din variabile propoziționale prin implicație și cuantificare propozițională universală În acest caz, valorile (adevărat), (fals), conjunctive (negație), (conjuncție) și (disjuncție), precum și (cuantificator de existență) pot fi definite după cum urmează $\top$ $\bot$ $\lnu$ $\teren$ $\lor$ $\există$

\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\lor 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

Rețineți că corespondența Curry-Howard atribuie adevărat un singur tip, fals un tip gol, conjuncționează un produs de tipuri și disjunge o sumă a acestora.

Note

↑ 1 2 Girard, Jean-Yves. Interpretation fonctionnelle et elimination des coupures de l'arithmétique d'ordre supérieur : Ph.D. teza. - Universitatea Paris 7, 1972.
↑ John C. Reynolds. Spre o teorie a structurii tip . - 1974. Arhivat la 31 octombrie 2014.
↑ Wells JB Tipabilitatea și verificarea tipului în calculul lambda de ordinul doi sunt echivalente și indecidabile // Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS). - 1994. - S. 176-185 . Arhivat din original pe 22 februarie 2007.

Literatură

Pierce, Benjamin C. Tipuri și limbaje de programare. - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Traducere în rusă: Pierce B. Tipuri în limbaje de programare. - Dobrosvet , 2012. - 680 p. — ISBN 978-5-7913-0082-9 .
Barendregt, Henk. Lambda Calculi cu tipuri // Manual de logică în informatică. - Oxford University Press, 1992. - Vol. II . - S. 117-309 .
Jean-Yves Girard, Paul Taylor, Yves Lafont. Dovezi și tipuri . - Cambridge University Press , 1989. - ISBN 0 521 37181 3 .