¿Importa el orden de las declaraciones en un tipo inductivo?

9

Me preguntaba si el orden de las declaraciones de tipo inductivo puede importar.

Por ejemplo, en Coq, puede definir Natya sea por:

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

o

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

Quizás esto cambie el orden de los parámetros en el eliminador generado automáticamente, pero eso no es gran cosa.

Lo que me pregunto es si es posible escribir una declaración como

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

donde type2es un tipo dependiente, dependiendo de cons1? (y en este caso, escribir las declaraciones en el otro orden no tendría ningún significado, porque type2se estaría refiriendo a lo cons1que aún no existe).

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

Respuestas:

10

  1. El orden no importa. No puedo pensar en un caso en el que lo haría. Como Andrej Bauer señala en un comentario, si cambia el orden, el resultado es canónicamente isomorfo al original .

  2. Un caso no puede depender de otro caso. Los elementos de la suma representan una elección, por lo que no tiene sentido que la elección tomada dependa de una elección que no se tome.

Dave Clarke
fuente
2
Puedes ser más específico sobre tu primer punto. El orden no importa. Si cambia el orden, el resultado es canónicamente isomorfo al original.
Andrej Bauer,
2
@Dave: ¡Gracias! Estaba haciendo esta pregunta debido a (la teoría altamente experimental de) los tipos inductivos superiores, donde este fenómeno parece suceder , y quería saber si esto también puede ser el caso con los tipos inductivos regulares.
Guillaume Brunerie
1
@Guillaume: no estoy seguro de qué fenómeno estás señalando con el enlace. Las diferentes cláusulas de constructor de una definición de tipo de datos no pueden depender unas de otras, independientemente de si se trata de un tipo de datos de orden superior. ¿Quizás esté pensando en registros dependientes (que se usan en el enlace y están disponibles en Agda y en Coq )?
Noam Zeilberger
1
@Noam: en el ejemplo del tipo inductivo superior circle, el tipo del loopconstructor depende del baseconstructor.
Guillaume Brunerie
2
@Guillaume: Ahora veo (están introduciendo una sintaxis experimental), no sé cómo me perdí eso.
Noam Zeilberger
6

¿Importa el orden en la forma en que lo pides? No.

¿Pero es la orden completamente irrelevante para el funcionamiento del asistente de pruebas? De nuevo no. En Matita, un asistente de prueba muy similar a Coq, el orden en que los constructores se escriben en una definición inductiva sí importa para la verificación de tipos, específicamente cuando se verifica una expresión de coincidencia.

Matita primero tiene que verificar que todos los constructores estén siendo enfrentados en el cuerpo del partido. Para ello, recorre los constructores en el orden en que se declaran. Luego, se trata de verificar la expresión de coincidencia adecuada, que ocurre en orden inverso, verificando primero el caso del último constructor declarado. Este tipo se lleva a cabo y se utiliza para verificar los otros casos.

Esto a menudo aparece cuando se escribe una expresión de coincidencia grande. Primero le gustaría completar los casos fáciles, dejando los casos más difíciles bajo un comodín, escriba periódicamente la verificación de lo que ha escrito para asegurarse de que tenga sentido. A veces, Matita es incapaz de inferir el tipo de expresión de coincidencia incompleta, pero lo hará con mucho gusto si completa el caso del último constructor definido en el tipo inductivo.

Supongo, aunque no estoy seguro, que Coq hace algo similar.

Dominic Mulligan
fuente