Co to jest indukcja indukcyjna?

Co to jest indukcja indukcyjna ?

Zasoby, które znalazłem to:

• książka HoTT na końcu rozdziału 5.7.
• Artykuł nLab
• artykuł zatytułowany Definicje indukcyjno-indukcyjne
• ten post na blogu wspomina także o typach indukcyjno-indukcyjnych

Pierwsze dwa odniesienia są dla mnie za krótkie, a dwa ostatnie są zbyt techniczne. Czy ktoś może to wytłumaczyć laikiem? Byłoby lepiej, gdyby był kod Agda.

Uzupełnienie 2016-10-03: Zmieszałem indukcję z indukcją z rekurencją (nie pierwszy raz to zrobiłem!). Przepraszam za bałagan. Zaktualizowałem odpowiedź, aby objąć oba te elementy.

Wyjaśnienia znajduję w pracy Forsberga i Setzera. Skończona aksjatyzacja definicji indukcyjno-indukcyjnych jest pouczająca.

Rekursja indukcyjna

Definicja indukcyjno-rekurencyjna to taka, w której definiujemy jednocześnie typ $A$ i rodzinę typów $B : A \to \mathsf{Type}$ jednocześnie w specjalny sposób:

1. $A$ jest zdefiniowany jako typ indukcyjny.
2. $B$ jest określona przez rekursję w$A$ .
3. Co najważniejsze, definicja $A$ może wykorzystywać $B$ .

Bez trzecie wymaganie może najpierw określić $A$ , a następnie oddzielnie $B$ .

Oto przykład dziecka. Zdefiniuj $A$ indukcyjnie, aby mieć następujące konstruktory:

• $a : A$
• $\ell : \big(\sum_{x : A} B(x)\big) \to A$

Rodzina typów $B$ jest zdefiniowana przez

• $B(a) = \mathtt{bool}$
• $B(\ell(x, f)) = \mathtt{nat}$ .

Co jest w $A$ ? Przede wszystkim mamy elementu

$$a : A.$$ Z tego powodu, nie jest to typ $B(a)$ , która jest zdefiniowana jako $\mathtt{bool}$ . Można zatem utworzyć dwa nowe elementy $$\ell(a, \mathtt{false})$$ i $$\ell(a, \mathtt{true})$$ w . Teraz mamy B ( ℓ ( a , f a$A$$B(\ell(a, \mathtt{false})) = B(\ell(a, \mathtt{true})) = \mathtt{nat}$ , więc możemy również utworzyć dla każdego$n : \mathtt{nat}$ elementy $$\ell(\ell(a, \mathtt{false}), n) : A$$ i $$\ell(\ell(a, \mathtt{true}), n) : A$$ Możemy dalej tak postępować. Następnym etapem będzie, że od $$B(\ell(\ell(a, \mathtt{true}), n)) = \mathtt{nat}$$ jest na każdy$m : \mathtt{nat}$ element $$\ell(\ell(\ell(a, \mathtt{true}), n), m) : A$$ i element $$\ell(\ell(\ell(a, \mathtt{false}), n), m) : A$$ Możemy iść dalej. Trochę myślenia ujawnia, że$A$ to mniej więcej dwie kopie liczb naturalnych, dzielące wspólną pustą listę. Zostawię to jako ćwiczenie, aby dowiedzieć się, dlaczego.

Indukcja-indukcja

Definicja indukcyjno-indukcyjna definiuje również typ $A$ i jednocześnie rodzinę typów $B : A \to \mathsf{Type}$ :

1. $A$ jest zdefiniowane indukcyjnie
2. $B$ jest zdefiniowane indukcyjnie i może odnosić się do$A$
3. Co najważniejsze, może odnosić się do B .$A$$B$

Ważne jest zrozumienie różnicy między indukcją-rekurencją a indukcją-indukcją. W indukcyjnego rekursji zdefiniować $B$ dostarczając równania postaci

$$B(\mathsf{c}(\ldots)) = \cdots$$ gdzie $\mathsf{c}(\ldots)$ jest konstruktor $A$ . W definicji indukcyjnego indukcyjnego zdefiniować $B$ dostarczając konstruktorów do formowania elementów $B$ .

Przeformułujmy nasz poprzedni przykład jako indukcję-indukcję. Najpierw mamy indukcyjnie podane tpye $A$ :

• $a : A$
• $\ell : \big(\sum_{x : A} B(x)\big) \to A$

Rodzina typów $B$ jest definiowana przez następujące konstruktory:

• $\mathsf{Tru} : B(a)$
• $\mathsf{Fal} : B(a)$
• jeśli $x : A$ i $y : B(x)$ to $\mathsf{Zer} : B(\ell(x,y))$
• jeśli $x : A$ i $y : B(x)$ i $z : B(\ell(x,y))$ to $\mathsf{Suc}(z) : B(\ell(x,y))$ .

Jak widać, podaliśmy zasady generowania elementów $B$ które sprowadzają się do stwierdzenia, że $B(a)$ jest (izomorficzny) do booleanów, a $B(\ell(x,y))$ jest (izomorficzny) liczb naturalnych.