Co to jest indukcja indukcyjna?

11

Co to jest indukcja indukcyjna ?

Zasoby, które znalazłem to:

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.

盛安安
źródło
W czwartym cytacie jest kod Agda.
Gilles „SO- przestań być zły”
Jasne, ale bardzo trudno byłoby odczytać tak ogromną ilość kodu. I (tak mi się wydaje) bardzo łatwe, po prostu widząc 1 lub 2 przykłady.
盛安安

Odpowiedzi:

13

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:AType jednocześnie w specjalny sposób:

  1. A jest zdefiniowany jako typ indukcyjny.
  2. B jest określona przez rekursję wA .
  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
  • :(x:AB(x))A

Rodzina typów B jest zdefiniowana przez

  • B(a)=bool
  • B((x,f))=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 bool . Można zatem utworzyć dwa nowe elementy
(a,false)
i
(a,true)
w . Teraz mamy B ( ( a , f aAB((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ż typ A i jednocześnie rodzinę typów B:AType :

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

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 tpye A :

  • a:A
  • :(x:AB(x))A

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

  • Tru:B(a)
  • Fal:B(a)
  • jeśli x:A i y:B(x) to Zer:B((x,y))
  • jeśli x:A i y:B(x) i z:B((x,y)) to Suc(z):B((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((x,y)) jest (izomorficzny) liczb naturalnych.

Andrej Bauer
źródło
dlaczego, do diabła, ktoś zdefiniowałby takie typy danych D:
盛安安
7
Aby nauczyć, czym jest typ indukcyjno-indukcyjny. Mógłbym podać prawdziwy przykład, mianowicie wszechświat typu, ale byłoby to mylące.
Andrej Bauer,
3
@AndrejBauer Dla mnie to bardziej przypomina rekursję indukcyjną. Indukcja-indukcja ma miejsce, gdy rodzina typów jest zdefiniowana jako typ indukcyjny .
gallais
2
Ups, masz absolutną rację. Naprawię to.
Andrej Bauer,
Czy domeną ma być typ Sigma zamiast typu Pi?
Dan Christensen