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.
Odpowiedzi:
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 typA i rodzinę typów B:A→Type jednocześnie w specjalny sposób:
Bez trzecie wymaganie może najpierw określićA , a następnie oddzielnie B .
Oto przykład dziecka. ZdefiniujA indukcyjnie, aby mieć następujące konstruktory:
Rodzina typówB jest zdefiniowana przez
Co jest wA ? Przede wszystkim mamy elementu a:A. Z tego powodu, nie jest to typ B(a) , która jest zdefiniowana jako bool . Można zatem utworzyć dwa nowe elementy ℓ(a,false) i ℓ(a,true) w . Teraz mamy B ( ℓ ( a , f aA B(ℓ(a,false))=B(ℓ(a,true))=nat , więc możemy również utworzyć dla każdegon:nat elementy
ℓ(ℓ(a,false),n):A
i
ℓ(ℓ(a,true),n):A
Możemy dalej tak postępować. Następnym etapem będzie, że od
B(ℓ(ℓ(a,true),n))=nat
jest na każdym:nat element
ℓ(ℓ(ℓ(a,true),n),m):A
i element
ℓ(ℓ(ℓ(a,false),n),m):A
Możemy iść dalej. Trochę myślenia ujawnia, żeA 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ż typA i jednocześnie rodzinę typów B:A→Type :
Ważne jest zrozumienie różnicy między indukcją-rekurencją a indukcją-indukcją. W indukcyjnego rekursji zdefiniowaćB dostarczając równania postaci
B(c(…))=⋯
gdzie c(…) 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 tpyeA :
Rodzina typówB jest definiowana przez następujące konstruktory:
Jak widać, podaliśmy zasady generowania elementówB które sprowadzają się do stwierdzenia, że B(a) jest (izomorficzny) do booleanów, a B(ℓ(x,y)) jest (izomorficzny) liczb naturalnych.
źródło