Induktiv typ

I typteorin har ett system induktiva typer om det har möjligheter att skapa en ny typ från konstanter och funktioner som skapar termer av den typen. Funktionen har en roll som liknar datastrukturer i ett programmeringsspråk och tillåter en typteori att lägga till begrepp som siffror , relationer och träd . Som namnet antyder kan induktiva typer vara självrefererande, men vanligtvis bara på ett sätt som tillåter strukturell rekursion .

Standardexemplet är att koda de naturliga talen med Peanos kodning . Det kan definieras i Coq enligt följande:

     
    0  
         Induktiv  nat  :  Typ  :=  |  :  nat  |  S  :  nat  ->  nat  .

Här skapas ett naturligt tal antingen från konstanten "0" eller genom att tillämpa funktionen "S" på ett annat naturligt tal. "S" är efterföljarens funktion som representerar att lägga till 1 till ett tal. Således är "0" noll, "S 0" är ett, "S (S 0)" är två, "S (S (S 0))" är tre, och så vidare.

Sedan deras introduktion har induktiva typer utökats till att koda fler och fler strukturer, samtidigt som de fortfarande är predikativa och stödjer strukturell rekursion.

Eliminering

Induktiva typer kommer vanligtvis med en funktion för att bevisa egenskaper hos dem. Således kan "nat" komma med (i Coq-syntax):

          0               nat_elim  :  (  forall  P  :  nat  ->  Prop  ,  (  P  )  ->  (  forall  n  ,  P  n  ->  P  (  S  n  ))  ->  (  forall  n  ,  P  n  )).

Med ord: för varje proposition "P" över naturliga tal, givet ett bevis på "P 0" och ett bevis på "P n -> P (n+1)", får vi tillbaka ett bevis på "forall n, P n ". Detta är den välbekanta induktionsprincipen för naturliga tal.

Genomföranden

W- och M-typer

W-typer är välgrundade typer inom intuitionistisk typteori ( ITT). De generaliserar naturliga tal, listor, binära träd och andra "trädformade" datatyper. Låt dig vara ett universum av typer . Givet en typ A : U och en beroende familj B : A → U , kan man bilda en W-typ ${\mathsf {W}}_{a:A}B(a) )$ . Typen A kan ses som "etiketter" för de (potentiellt oändligt många) konstruktörerna av den induktiva typen som definieras, medan B indikerar den (potentiellt oändliga) ariteten för varje konstruktor. W-typer (resp. M-typer) kan också förstås som välgrundade (resp. icke välgrundade) träd med noder märkta av elementen a : A och där noden märkt med a har B ( a ) - många underträd. Varje W-typ är isomorf till den initiala algebra av en så kallad polynomfunktion .

0 Låt , 1 , 2 etc. vara finita typer med invånare 1 ₁ : 1 , 1 ₂ , 2 ₂ : 2 etc. Man kan definiera de naturliga talen som W-typen

\mathbb {N} :={\mathsf {W}}_{x:\mathbf {2} }f(x)

0 med f : 2 → U definieras av f (1 ₂ ) = (representerar konstruktorn för noll, som inte tar några argument), och f (2 ₂ ) = 1 (representerar efterföljarfunktionen, som tar ett argument).

Man kan definiera listor över en typ A : U som $\operatorname {List} (A):={\mathsf {W}} _{(x:\mathbf {1} +A)}f(x)$ där

{\begin{aligned}f(\operatörsnamn {inl} (1_{\mathbf {1} }))&=\ mathbf {0} \\f(\operatörsnamn {inr} (a))&=\mathbf {1} \end{aligned}}

och 1 ₁ är den enda invånaren i 1 . Värdet på

f(\operatörsnamn {inl} (1_{\mathbf {1} }))

motsvarar konstruktorn för den tomma listan, medan värdet på

f(\operatörsnamn {inr} (a))

motsvarar konstruktorn som lägger till a i början av en annan lista.

Konstruktorn för element av en generisk W-typ ${\mathsf {W}}_{x:A}B(x)$ har typen

{\mathsf {sup}}:\prod _{a:A}{\Big (}B(a)\to {\mathsf {W}}_{x:A}B(x){\Big )}\till {\mathsf {W}}_{x:A}B(x).

Vi kan också skriva denna regel i stil med ett naturligt avdragsbevis ,

{\frac {a:A\qquad f:B(a)\to {\mathsf {W}}_{x:A}B(x)}{{\mathsf {sup}}(a,f ):{\mathsf {W}}_{x:A}B(x)}}.

Elimineringsregeln för W-typer fungerar på samma sätt som strukturell induktion på träd. Om, närhelst en egenskap (under tolkningen av propositioner-som-typer ) $C:{\mathsf {W}}_{x:A}B(x)\ till U$ gäller för alla underträd i ett givet träd gäller det också för det trädet, då gäller det för alla träd.

{\frac {w:{\mathsf {W}}_{a :A}B(a)\qquad a:A,\;f:B(a)\to {\mathsf {W}}_{x:A}B(x),\;c:\prod _{b :B(a)}C(f(b))\;\vdash \;h(a,f,c):C({\mathsf {sup}}(a,f))}{{\mathsf {elim }}(w,h):C(w)}}

I extensional typteorier kan W-typer (resp. M-typer) definieras fram till isomorfism som initiala algebror (resp. slutliga koalgebror) för polynomfunktioner . I detta fall motsvarar egenskapen initialitet (res. finality) direkt den lämpliga induktionsprincipen. I intensional typteorier med univalensaxiomet håller denna korrespondens upp till homotopi (propositionell likhet).

M-typer är dubbla till W-typer, de representerar koduktiva (potentiellt oändliga) data som strömmar . M-typer kan härledas från W-typer.

Ömsesidigt induktiva definitioner

Denna teknik tillåter vissa definitioner av flera typer som är beroende av varandra. Till exempel, att definiera två paritetspredikat på naturliga tal med två ömsesidigt induktiva typer i Coq :

      
      
            
      
             Induktiv  jämn  :  nat  ->  Prop  :=  |  noll_är_jämn  :  jämn  O  |  S_of_odd_is_even  :  (  forall  n  :  nat  ,  udda  n  ->  jämn  (  S  n  ))  med  udda  :  nat  ->  Prop  :=  |  S_of_even_is_odd  :  (  forall  n  :  nat  ,  jämn  n  ->  udda  (  S  n  )).

Induktion-rekursion

Induktion-rekursion började som en studie av gränserna för ITT. När de väl hittats omvandlades gränserna till regler som gjorde det möjligt att definiera nya induktiva typer. Dessa typer kan bero på en funktion och funktionen på typen, så länge som båda definierades samtidigt.

Universumstyper kan definieras med induktionsrekursion.

Induktion-induktion

Induktionsinduktion tillåter definition av en typ och en familj av typer på samma gång. Så, en typ $A$ och en familj av typer $B:A\to Type$ .

Högre induktiva typer

Detta är ett aktuellt forskningsområde inom Homotopy Type Theory (HoTT). HoTT skiljer sig från ITT genom sin identitetstyp (jämlikhet). Högre induktiva typer definierar inte bara en ny typ med konstanter och funktioner som skapar element av typen, utan också nya instanser av den identitetstyp som relaterar dem.

Ett enkelt exempel är $cirkeltypen$ , som definieras med två konstruktorer, en baspunkt;

bas : cirkel

och en slinga;

loop : bas = bas .

Förekomsten av en ny konstruktor för identitetstypen gör $cirkel$ till en högre induktiv typ.

Se även

Koinduktion tillåter (effektivt) oändliga strukturer i typteorin.

Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics . Institutet för avancerade studier.

externa länkar