O que é indução-indução?

11

O que é indução-indução ?

Os recursos que encontrei são:

As duas primeiras referências são muito breves para mim e as duas últimas são muito técnicas. Alguém pode explicar isso em termos leigos? Seria melhor se houver código Agda.

盛安安
fonte
Há código Agda na sua quarta citação.
Gilles 'SO- stop be evil'
Claro, mas seria super difícil ler essa enorme quantidade de código. E (eu acho) super fácil apenas vendo 1 ou 2 exemplos.
盛安安

Respostas:

13

Suplementar 03/10/2016: Misturei indução-indução e indução-recursão (não a primeira vez que fiz isso!). Minhas desculpas pela bagunça. Eu atualizei a resposta para cobrir os dois.

Acho que as explicações no artigo de Forsberg & Setzer iluminam uma axiomatização finita de definições indutivo-indutivas .

Indução-recursão

Uma definição indutivo-recursiva é aquela em que definimos um tipo e uma família de tipos simultaneamente de uma maneira especial:AB:AType

  1. A é definido como um tipo indutivo.
  2. B é definido por recursividade em .A
  3. Fundamentalmente, a definição de pode usar .AB

Sem o terceiro requisito, poderíamos primeiro definir e, em seguida, separadamente .AB

Aqui está um exemplo de bebê. Defina indutivamente para ter os seguintes construtores:A

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

A família de tipos é definida porB

  • B(a)=bool
  • B((x,f))=nat .

Então, o que está em ? Primeiro de tudo, temos um elemento Por causa disso, existe um tipo que é definido como . Portanto, podemos formar dois novos elementos e em . Agora temos , para que também possamos formar para cada os elementos e Podemos continuar assim . A próxima etapa será que, desde A

a:A.
B(a)bool
(a,false)
(a,true)
AB((a,false))=B((a,true))=natn:nat
((a,false),n):A
((a,true),n):A
B(((a,true),n))=nat
existe para cada o elemento e o elemento Podemos continuar. Um pouco de pensamento revela que é mais ou menos duas cópias de listas de números naturais, compartilhando uma lista vazia comum. Vou deixar isso como um exercício para descobrir o porquê.m:nat
(((a,true),n),m):A
(((a,false),n),m):A
A

Indução-indução

Uma definição indutiva-indutiva também define um tipo e, simultaneamente, uma família de tipos :AB:AType

  1. A é definido indutivamente
  2. B é definido indutivamente e pode se referir aA
  3. Fundamentalmente, pode referir-se a .AB

É importante entender a diferença entre indução-recursão e indução-indução. Na indução-recursão definimos , fornecendo equações da forma onde é um construtor para . Numa definição indutiva-indutivo definimos , fornecendo construtores para formar os elementos de .B

B(c())=
c()ABB

Vamos reformular nosso exemplo anterior como indução-indução. Primeiro, temos o tpye dado indutivamente :A

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

A família de tipos é definida pelos seguintes construtores:B

  • Tru:B(a)
  • Fal:B(a)
  • se e entãox:Ay:B(x)Zer:B((x,y))
  • se e e então .x:Ay:B(x)z:B((x,y))Suc(z):B((x,y))

Como você pode ver, definimos regras para gerar os elementos de que equivale a dizer que é (isomófico para) os booleanos, e é (isomórfico para) os números naturais .BB(a)B((x,y))

Andrej Bauer
fonte
por que diabos alguém iria definir tais tipos de dados D:
盛安安
7
Para ensinar o que é um tipo indutivo-indutivo. Eu poderia dar um exemplo real, ou seja, um universo de tipos, mas isso seria confuso.
Andrej Bauer
3
@AndrejBauer Parece-me mais uma recursão de indução. Indução-indução é quando a família de tipos é definida como um tipo indutivo .
Gallais
2
Opa, você está absolutamente certo. Eu resolvo isso.
Andrej Bauer
O domínio de deveria ser do tipo Sigma, em vez de Pi?
Dan Christensen