O que é indução-indução ?
Os recursos que encontrei são:
- o livro HoTT , no final do capítulo 5.7.
- Artigo do nLab
- um artigo chamado definições indutivo-indutivas
- este post do blog também menciona tipos indutivos-indutivos
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.
Respostas:
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:A B:A→Type
Sem o terceiro requisito, poderíamos primeiro definir e, em seguida, separadamente .A B
Aqui está um exemplo de bebê. Defina indutivamente para ter os seguintes construtores:A
A família de tipos é definida porB
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, desdeA a:A. B(a) bool ℓ(a,false) ℓ(a,true) A B(ℓ(a,false))=B(ℓ(a,true))=nat n: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 :A B:A→Type
É 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(…) A B B
Vamos reformular nosso exemplo anterior como indução-indução. Primeiro, temos o tpye dado indutivamente :A
A família de tipos é definida pelos seguintes construtores:B
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 .B B(a) B(ℓ(x,y))
fonte