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

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.

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 \to \mathsf{Type}$

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

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 : A$
• $\ell : \big(\sum_{x : A} B(x)\big) \to A$

A família de tipos é definida por$B$

• $B(a) = \mathtt{bool}$
• $B(\ell(x, f)) = \mathtt{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)$$\mathtt{bool}$ $$\ell(a, \mathtt{false})$$ $$\ell(a, \mathtt{true})$$ $A$$B(\ell(a, \mathtt{false})) = B(\ell(a, \mathtt{true})) = \mathtt{nat}$$n : \mathtt{nat}$ $$\ell(\ell(a, \mathtt{false}), n) : A$$ $$\ell(\ell(a, \mathtt{true}), n) : A$$ $$B(\ell(\ell(a, \mathtt{true}), n)) = \mathtt{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 : \mathtt{nat}$ $$\ell(\ell(\ell(a, \mathtt{true}), n), m) : A$$ $$\ell(\ell(\ell(a, \mathtt{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 \to \mathsf{Type}$

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

É 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(\mathsf{c}(\ldots)) = \cdots$$ $\mathsf{c}(\ldots)$$A$$B$$B$

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

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

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

• $\mathsf{Tru} : B(a)$
• $\mathsf{Fal} : B(a)$
• se e então$x : A$$y : B(x)$$\mathsf{Zer} : B(\ell(x,y))$
• se e e então .$x : A$$y : B(x)$$z : B(\ell(x,y))$$\mathsf{Suc}(z) : B(\ell(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 .$B$$B(a)$$B(\ell(x,y))$