Systém F

Systém F ( polymorfní počet lambda , systém $\lambda 2$ , typovaný počet lambda druhého řádu ) je typovaný systém počtu lambda , který se liší od jednoduše typovaného systému přítomností univerzálního kvantifikačního mechanismu nad typy. Tento systém vyvinul v roce 1972 Jean-Yves Girard [1] v kontextu teorie důkazů v logice. Nezávisle na něm podobný systém navrhl v roce 1974 John Reynolds [2] . Systém F vám umožňuje formalizovat koncept parametrického polymorfismu v programovacích jazycích a slouží jako teoretický základ pro takové programovací jazyky, jako jsouHaskell a ML .

Systém F umožňuje konstrukci termínů v závislosti na typech. Technicky je toho dosaženo mechanismem abstrahování termínu podle typu, což vede k novému termínu. Tradičně se pro takovou abstrakci používá velký symbol lambda . Například, vezmeme-li výraz typu a abstrahujeme proměnnou typu , získáme term . Tento termín je funkcí od typů k termínům. Aplikací této funkce na různé typy získáme termíny se stejnou strukturou, ale různými typy: $\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

- termín typu ;

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

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

je termín typu .

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

Je vidět, že termín má polymorfní chování, to znamená, že definuje společné rozhraní pro různé datové typy. V systému F je tomuto termínu přiřazen typ . Univerzální kvantifikátor v typu zdůrazňuje možnost nahrazení typové proměnné jakýmkoli platným typem . $\Lambda \alpha .~\lambda x^{\alpha }.~x$ $\forall \alpha .~\alpha \to \alpha$ $\alpha$

Formální popis

Syntaxe typu

Typy systému F jsou konstruovány ze sady typových proměnných pomocí operátorů a . Podle tradice se pro typové proměnné používají řecká písmena. Pravidla pro formování typů jsou následující: $\na$ $\pro všechny$

( Type variable ) Pokud je proměnná typu, pak je typ; $\alpha$ $\alpha$
( Arrow type ) Jestliže a jsou typy, pak je typ; $A$ $B$ $(A\do B)$
( Obecný typ ) Jestliže je typová proměnná a je typem, pak je typ. $\alpha$ $B$ $(\forall \alpha .~B)$

Vnější závorky jsou často vynechány, operátor je považován za asociativní vpravo a akce operátoru pokračuje doprava, pokud je to možné. Například je standardní zkratka pro . $\šipka doprava$ $\pro všechny$ $\forall \alpha .~\forall \beta .~\alpha \to \beta \to \alpha$ $(\forall \alpha .~(\forall \beta .~(\alpha \to (\beta \to \alpha ))))$

Syntaxe termínů

Termíny systému F jsou konstruovány ze sady termínových proměnných ( , atd .) podle následujících pravidel $X$ $y$ $z$

( Proměnná ) Jestliže je proměnná, pak je termín; $X$ $X$
( Abstrakce ) Jestliže je proměnná, je typ a je termín, pak je termín; $X$ $A$ $M$ $(\lambda x^{A}.~M)$
( Aplikace ) Jestliže a jsou termíny, pak je termín; $M$ $N$ $(M~N)$
( Univerzální abstrakce ) Jestliže je typová proměnná a je termín, pak je termín; $\alpha$ $M$ $(\Lambda \alpha .~M)$
( Univerzální použití ) Jestliže je termín a je typ, pak je termín. $M$ $A$ $(M~A)$

Vnější závorky jsou často vynechány, oba druhy použití jsou považovány za asociativní vlevo a akce abstrakce se považuje za pokračování doprava, pokud je to možné.

Existují dvě verze jednoduchého systému. Pokud, jako ve výše uvedených pravidlech, jsou termínové proměnné v lambda abstrakci označeny typy, pak je systém označován jako Church-typed . Pokud je pravidlo abstrakce nahrazeno

( Abstrakce podle Curryho ) Jestliže je proměnná a je termín, pak je termín, $X$ $M$ $(\lambda x.~M)$

a zahoďte poslední dvě pravidla, pak se systém nazývá Curry-typed . Ve skutečnosti jsou podmínky Curry-typizovaného systému stejné jako ty v netypizovaném lambda kalkulu.

Pravidla snížení

Kromě standardního -redukčního pravidla pro lambda kalkul $\beta$

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

Kostelní systém F zavádí další pravidlo,

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

umožňující vypočítat aplikaci termínu na typ pomocí mechanismu substituce typu namísto typové proměnné.

Kontexty psaní a tvrzení typu

Kontext, stejně jako v jednoduše zadaném lambda kalkulu , je soubor příkazů o přiřazování typů různým proměnným, oddělených čárkou

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

Pro tento kontext můžete do kontextu přidat proměnnou „fresh“: pokud je platný kontext, který neobsahuje proměnnou , a je to typ, pak je to také platný kontext. $\Gamma$ $X$ $B$ $\Gamma ,x\!:\!B$

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

\Gamma \vdash M\!:\!A

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

Pravidla církevního psaní

V Churchově typizovaném systému F se přiřazování typů termínům provádí podle následujících pravidel:

( Počáteční pravidlo ) Pokud je proměnná přítomna s typem v kontextu , pak má typ v tomto kontextu . Ve formě inferenčního pravidla $X$ $A$ $\Gamma$ $X$ $A$

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

( Úvodní pravidlo $\šipka doprava$ ) Jestliže v nějakém kontextu rozšířeném o příkaz, který má typ , má výraz typ , pak v uvedeném kontextu (bez ) má abstrakce lambda typ . Ve formě inferenčního pravidla $A$ $A$ $M$ $B$ $A$ $\lambda a^{A}.~M$ $A až B$

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

( pravidlo odstranění $\šipka doprava$ ) Pokud má v nějakém kontextu termín typ a termín má typ , pak má typ aplikace . Ve formě inferenčního pravidla $M$ $A až B$ $N$ $A$ $M~N$ $B$

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

( Úvodní pravidlo $\pro všechny$ ) Jestliže v nějakém kontextu má termín typ , pak v tomto kontextu má termín typ . Ve formě inferenčního pravidla $M$ $A$ $\Lambda \alpha .~M$ $\forall \alpha .~A$

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

Toto pravidlo vyžaduje upozornění: typová proměnná se nesmí vyskytovat v výrazech pro zadávání kontextu . $\alpha$ $\Gamma$

( pravidlo odstranění $\pro všechny$ ) Pokud má v nějakém kontextu výraz typ , a je typem, pak v tomto kontextu má výraz typ . Ve formě inferenčního pravidla $M$ $\forall \alpha .~A$ $B$ $M~B$ $A[\alpha :=B]$

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

Curryho pravidla psaní

V systému F typu Curry se přiřazování typů termínům provádí podle následujících pravidel:

( Počáteční pravidlo ) Pokud je proměnná přítomna s typem v kontextu , pak má typ v tomto kontextu . Ve formě inferenčního pravidla $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\to B) }

( pravidlo odstranění $\šipka doprava$ ) Pokud má v nějakém kontextu termín typ a termín má typ , pak má typ aplikace . Ve formě inferenčního pravidla $M$ $A až B$ $N$ $A$ $M~N$ $B$

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

( Úvodní pravidlo $\pro všechny$ ) Pokud má termín v nějakém kontextu typ , pak v tomto kontextu lze tomuto termínu také přiřadit typ . Ve formě inferenčního pravidla $M$ $A$ $M$ $\forall \alpha .~A$

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

Toto pravidlo vyžaduje upozornění: typová proměnná se nesmí vyskytovat v výrazech pro zadávání kontextu . $\alpha$ $\Gamma$

( pravidlo odstranění $\pro všechny$ ) Pokud má v nějakém kontextu výraz typ , a je typem, pak v tomto kontextu lze tomuto výrazu přiřadit také typ . Ve formě inferenčního pravidla $M$ $\forall \alpha .~A$ $B$ $M$ $A[\alpha :=B]$

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

Příklad. Podle původního pravidla:

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

Použijme pravidlo odebrání , přičemž jako typ $\pro všechny$ $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 )

Nyní, v souladu s pravidlem odebrání , máme možnost použít termín na sebe sama $\šipka doprava$ $X$

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

a konečně podle pravidla úvodu $\šipka doprava$

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

Toto je příklad výrazu zadávaného v systému F, ale ne v jednoduše zadávaném systému .

Reprezentace datových typů

Systém F je dostatečně expresivní, aby přímo implementoval mnoho datových typů používaných v programovacích jazycích. Budeme pracovat v Churchově verzi systému F.

Prázdný typ. Typ

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

je v systému F neobydlený, to znamená, že v něm nejsou žádné termíny s tímto typem.

Jediný typ. Typ Y

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

systém F má jednoho normálního obyvatele, člen

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

booleovský typ. V systému F je dáno následovně:

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

Tento typ má přesně dva obyvatele identifikované dvěma booleovskými konstantami

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

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

Konstrukce podmíněného operátoru

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

Tato funkce splňuje přirozené požadavky

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

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

pro libovolný typ a libovolný a . Je snadné to ověřit rozšířením definic a provedením -redukce. $A$ $M\!:\!A$ $N\!:\!A$ $\beta$

Typ uměleckého díla. Pro libovolné typy a typ jejich kartézského součinu $A$ $B$

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

obývá pár

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

pro každého a . Projekce dvojice jsou dány funkcemi $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

Tyto funkce splňují přirozené požadavky a . ${\mathtt {fst}}\,A\,B\,\langle M;N\rangle =M$ ${\mathtt {snd}}\,A\,B\,\langle M;N\rangle =N$

Typ částky. Pro libovolné typy a typ jejich součtu $A$ $B$

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

vyplněno buď termínem typu , nebo termínem typu , v závislosti na použitém konstruktoru $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

Zde , . Funkce, která provádí analýzu velkých a malých písmen (pattern matching) má tvar $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 .~\ forall \beta .~\forall \gamma .~\alpha +\beta \to (\alpha \to \gamma )\to (\beta \to \gamma )\to \gamma

Tato funkce splňuje následující přirozené požadavky

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

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

pro libovolné typy a libovolné termíny a . $A$ $B$ $C$ $F\!:\!A\to C$ $G\!:\!B\to C$

Kostelní čísla. Typ přirozených čísel v soustavě F

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

obývá nekonečné množství různých prvků, získaných prostřednictvím dvou konstruktérů a : ${\mathtt {nula}}\!:\!{\mathtt {Nat}}$ ${\mathtt {succ}}\!:\!{\mathtt {Nat}}\to {\mathtt {Nat}}$

{\mathtt {nula))\ \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)

Přirozené číslo lze získat aplikací druhého konstruktoru - krát na první, nebo ekvivalentně reprezentované výrazem $n$ $n$

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

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$

Jean-Yves Girard ve své dizertační práci ukázal [1] , že systém F má silnou normalizační vlastnost: jakýkoli přípustný člen může být po konečném počtu -redukcí redukován na jedinečnou normální formu. $\beta$

F systém je nepredikativní systém, protože typová proměnná spojená s univerzálním kvantifikátorem při definování generického typu může být nahrazena objektem, který je definován sám. Například termín jednoho typu lze použít na svůj vlastní typ, čímž vznikne termín typu . Jak ukázal Joe Wells v roce 1994 [3] , problém odvození typu pro Curryho verzi systému F je neřešitelný. Proto se při praktické implementaci programovacích jazyků obvykle používají omezené, predikativní verze polymorfismu: prenexový polymorfismus (polymorfismus ve stylu ML ), polymorfismus 2. úrovně atd. V případě prenexového polymorfismu jsou rozsahem typových proměnných pouze typy bez kvantifikátorů. V těchto systémech je problém typové inference řešitelný, taková inference je založena na Hindley-Milnerově algoritmu . ${\texttt {id}}$ $\top \equiv \forall \alpha .~\alpha \to \alpha$ $\top \to \top$

Curry-Howardova korespondence spojuje Systém F s minimální intuicionistickou výrokovou logikou druhého řádu konstruovány z výrokových proměnných implikací a univerzální výrokovou kvantifikací V tomto případě lze hodnoty (pravda), (nepravda), spojky (negace), (konjunkce) a (disjunkce) a také (kvantifikátor existence) definovat následovně $\horní$ $\bot$ $\lne$ $\přistát$ $\lor$ $\existuje$

\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

Všimněte si, že korespondence Curry-Howard přiřazuje true jeden typ, false prázdný typ, spojuje součin typů a odděluje jejich součet.

Poznámky

↑ 1 2 Girard, Jean-Yves. Interpretace fonctionnelle et elimination des coupures de l'aritmétique d'ordre supérieur : Ph.D. teze. — Université Paris 7, 1972.
↑ John C. Reynolds. Směrem k teorii typové struktury . - 1974. Archivováno 31. října 2014.
↑ Wells JB Typabilita a typová kontrola v lambda-kalkulu druhého řádu jsou ekvivalentní a nerozhodnutelné // Sborník z 9. výročního sympozia IEEE o logice v počítačové vědě (LICS). - 1994. - S. 176-185 . Archivováno z originálu 22. února 2007.

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 .
Jean-Yves Girard, Paul Taylor, Yves Lafont. Důkazy a typy . - Cambridge University Press , 1989. - ISBN 0 521 37181 3 .