Typ indukcyjny - Inductive type

W teorii typów system ma typy indukcyjne, jeśli ma możliwości tworzenia nowego typu ze stałych i funkcji, które tworzą warunki tego typu. Funkcja ta pełni rolę podobną do struktur danych w języku programowania i umożliwia teorii typów dodawanie pojęć, takich jak liczby , relacje i drzewa . Jak sama nazwa wskazuje, typy indukcyjne mogą odnosić się do siebie, ale zwykle tylko w sposób, który pozwala na rekurencję strukturalną .

Standardowym przykładem jest kodowanie liczb naturalnych przy użyciu kodowania Peano .

 Inductive nat : Type :=
   | 0 : nat
   | S : nat -> nat.

Tutaj liczba naturalna jest tworzona albo ze stałej „0”, albo przez zastosowanie funkcji „S” do innej liczby naturalnej. „S” to funkcja następcy, która reprezentuje dodanie 1 do liczby. Zatem „0” to zero, „S 0” to jeden, „S (S 0)” to dwa, „S (S (S 0))” to trzy i tak dalej.

Od czasu ich wprowadzenia typy indukcyjne zostały rozszerzone, aby kodować coraz więcej struktur, a jednocześnie nadal są predykatywne i wspierają rekurencję strukturalną.

Eliminacja

Typy indukcyjne zwykle mają funkcję udowadniania ich właściwości. Tak więc „nat” może pochodzić z:

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

Jest to oczekiwana funkcja rekurencji strukturalnej dla typu „nat”.

Realizacje

Typy W i M

Typy W są typami dobrze ugruntowanymi w intuicjonistycznej teorii typów (ITT). Uogólniają liczby naturalne, listy, drzewa binarne i inne typy danych „w kształcie drzewa”. Niech U będzie wszechświatem typów . Mając typ A : U i rodzinę zależną B : A → U , można utworzyć typ W . Typ A można traktować jako „etykiety” dla (potencjalnie nieskończenie wielu) konstruktorów definiowanego typu indukcyjnego, podczas gdy B wskazuje (potencjalnie nieskończoną) arność każdego konstruktora. Typy W (odp. M-typy) mogą być również rozumiane jako drzewa uzasadnione (odp. nieuzasadnione) z węzłami oznaczonymi elementami a : A i gdzie węzeł oznaczony przez a ma B ( a )-wiele poddrzewa. Każdy typ W jest izomorficzny z początkową algebrą tak zwanego funktora wielomianowego . ${\ Displaystyle {\ mathsf {W}} _ {a: A} B (a)}$

Niech 0 , 1 , 2 , itd. będą typami skończonymi z mieszkańcami 1 ₁ : 1 , 1 ₂ , 2 ₂ : 2 itd. Liczby naturalne można zdefiniować jako typ W

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

gdzie f : 2 → U jest zdefiniowane przez f (1 ₂ ) = 0 (reprezentujące konstruktor dla zera, który nie przyjmuje argumentów), a f (2 ₂ ) = 1 (reprezentujący funkcję następnika, który przyjmuje jeden argument).

Można zdefiniować listy nad typem A : U jako gdzie ${\ Displaystyle \ Operatorname {Lista} (A): = {\ mathsf {W}} _ {(x: \ mathbf {1} + A)} f (x)}$

{\ Displaystyle {\ zacząć {wyrównany} f (\ nazwa operatora {inl} (1_ {\ mathbf {1} })) i = \ mathbf {0} \ \ f (\ nazwa operatora {inr} (a)) i = \ mathbf {1} \end{wyrównany}}}

a 1 ₁ jest jedynym mieszkańcem 1 . Wartość of odpowiada konstruktorowi pustej listy, podczas gdy wartość odpowiada konstruktorowi, który dołącza a na początku innej listy.

{\ Displaystyle f (\ nazwa operatora {inl} (1_ {\ mathbf {1} }))}

f(\operator {inr} (a))

Konstruktor elementów ogólnego typu W ma typ ${\ Displaystyle {\ mathsf {W}} _ {x: A} B (x)}$

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

Możemy również napisać tę zasadę w stylu dowodu dedukcji naturalnej ,

{\ Displaystyle {\ Frac {a: A \ qquad f: B (a) \ do {\ mathsf {W}} _ {x: A} B (x)} {{\ mathsf {sup}} (a, f ):{\mathsf {W}}_{x:A}B(x)}}.}

Zasada eliminacji dla typów W działa podobnie do indukcji strukturalnej na drzewach. Jeśli kiedykolwiek własność (w interpretacji zdań-jako-typów ) zachodzi dla wszystkich poddrzew danego drzewa, to obowiązuje ona również dla tego drzewa, to obowiązuje dla wszystkich drzew. ${\ Displaystyle C: {\ mathsf {W}} _ {x: A} B (x) \ do U}$

{\ Displaystyle {\ Frac {w: {\ mathsf {W}} _ {a: A} B (a) \ qquad a: A \; f: B (a) \ do {\ 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)}}}

W teoriach typu ekstensjonalnego, typy W (odp. typy M) można zdefiniować aż do izomorfizmu jako początkowe algebry (odp. końcowe kogebry) dla funktorów wielomianowych . W tym przypadku właściwość inicjalizacji (res. finality) odpowiada bezpośrednio odpowiedniej zasadzie indukcji. W teoriach typu intensjonalnego z aksjomatem jednowartościowości ta zgodność jest zgodna z homotopią (równością zdań).

Typy M są podwójne do typów W, reprezentują dane koindukcyjne (potencjalnie nieskończone), takie jak strumienie . Typy M mogą pochodzić od typów W.

Wzajemnie indukcyjne definicje

Technika ta pozwala na pewne definicje wielu typów, które są od siebie zależne. Na przykład zdefiniowanie dwóch predykatów parzystości na liczbach naturalnych przy użyciu dwóch wzajemnie indukcyjnych typów w Coq :

Inductive even : nat -> Prop :=
  | zero_is_even : even O
  | S_of_odd_is_even : (forall n:nat, odd n -> even (S n))
with odd : nat -> Prop :=
  | S_of_even_is_odd : (forall n:nat, even n -> odd (S n)).

Indukcyjno-rekurencja

Indukcja-rekurencja rozpoczęła się jako badanie granic ITT. Po odkryciu limity zostały przekształcone w reguły, które umożliwiły zdefiniowanie nowych typów indukcyjnych. Te typy mogą zależeć od funkcji, a funkcja od typu, o ile oba zostały zdefiniowane jednocześnie.

Typy wszechświatów można zdefiniować za pomocą indukcji-rekurencji.

Indukcja-indukcja

Indukcja-indukcja umożliwia jednoczesną definicję typu i rodziny typów. A więc typ $A$ i rodzina typów . $B:A\do wpisywania$

Wyższe typy indukcyjne

Jest to aktualny obszar badań w teorii typów homotopii (HoTT). HoTT różni się od ITT typem tożsamości (równość). Wyższe typy indukcyjne nie tylko definiują nowy typ ze stałymi i funkcjami, które tworzą elementy typu, ale także nowe wystąpienia typu tożsamości, które je wiążą.

Prostym przykładem jest typ $okręgu$ , który jest zdefiniowany za pomocą dwóch konstruktorów, punktu bazowego;

podstawa : koło

i pętla;

pętla : baza = baza .

Istnienie nowego konstruktora typu tożsamościowego czyni $koło$ wyższym typem indukcyjnym.

Zobacz też

Koindukcja dopuszcza (efektywnie) nieskończone struktury w teorii typów.

Bibliografia

Program Fundacji Uniwalentnych (2013). Teoria typów homotopii: jednowartościowe podstawy matematyki . Instytut Studiów Zaawansowanych.

Languages

In other projects