A ordem das declarações em um tipo indutivo é importante?

9

Eu queria saber se a ordem das declarações de um tipo indutivo pode importar.

Por exemplo, no Coq, você pode definir Nat:

Inductive Nat :=
  | O : Nat
  | S : Nat -> Nat.

ou

Inductive Nat :=
  | S : Nat -> Nat
  | O : Nat.

Talvez isso mude a ordem dos parâmetros no eliminador gerado automaticamente, mas isso não é grande coisa.

O que eu quero saber é se é possível escrever uma declaração como

Inductive typewhereordermatters :=
  | cons1 : type1
  | cons2 : type2.

onde type2é um tipo dependente, dependendo cons1? (e, neste caso, escreva as declarações na outra ordem não teriam significado, porque type2se refeririam a cons1qual ainda não existe).

lo.logic type-theory coq dependent-type Guillaume Brunerie
fonte

Respostas:

10

  1. O pedido não importa. Não consigo pensar em um caso em que isso aconteceria. Como Andrej Bauer aponta em um comentário, se você alterar a ordem, o resultado é canonicamente isomórfico ao original .

  2. Um caso não pode depender de outro caso. Os elementos da soma representam uma escolha, portanto, não faz sentido que a escolha feita dependa de uma escolha que não seja feita.

Dave Clarke
fonte
2
Você pode ser mais específico sobre o seu primeiro ponto. O pedido não importa. Se você alterar a ordem, o resultado é canonicamente isomórfico ao original.
Andrej Bauer 14/05
2
@ Dave: Obrigado! Eu estava fazendo essa pergunta por causa da (altamente experimental teoria dos) tipos indutivos mais altos, onde esse fenômeno parece acontecer , e eu queria saber se esse também pode ser o caso dos tipos indutivos regulares.
Guillaume Brunerie
11
@ Guillaume: Não sei ao certo qual fenômeno você está apontando com o link. As diferentes cláusulas construtoras de uma definição de tipo de dados não podem depender uma da outra, seja um tipo de dados de ordem superior. Talvez você esteja pensando em registros dependentes (que são usados ​​no link e estão disponíveis na Agda e na Coq )?
Noam Zeilberger 14/05
11
@ Noam: No exemplo do tipo indutivo mais alto circle, o tipo do loopconstrutor depende do baseconstrutor.
Guillaume Brunerie
2
@ Guillaume: Entendo agora (eles estão introduzindo uma sintaxe experimental), não sei como eu perdi isso.
Noam Zeilberger
6

O pedido importa da maneira que você pede? Não.

Mas a ordem é completamente irrelevante para o funcionamento do assistente de prova? Novamente não. Em Matita, um assistente de prova muito semelhante ao Coq, a ordem em que construtores são escritos em uma definição indutiva faz questão de verificação de tipo, especificamente quando o tipo de verificação a expressão de correspondência.

Matita primeiro deve verificar se todos os construtores estão sendo comparados no corpo da partida. Isso é feito alternando entre os construtores na ordem em que são declarados. Em seguida, trata-se de verificar a expressão de correspondência adequada, o que acontece na ordem inversa, verificando primeiro o caso para o último construtor declarado. Esse tipo é realizado e usado para verificar os outros casos.

Isso geralmente aparece ao escrever uma expressão de correspondência grande. Você gostaria de preencher primeiro os casos fáceis, deixando os casos mais difíceis sob um curinga, periodicamente digite a verificação do que você escreveu para se certificar de que faz sentido. Às vezes, o Matita é incapaz de inferir o tipo da expressão de correspondência incompleta, mas o fará com muita satisfação se você preencher o caso do último construtor definido no tipo indutivo.

Presumo, embora não tenha certeza, que Coq faz algo semelhante.

Dominic Mulligan
fonte