¿Qué es diferente entre Set y Type en Coq? [cerrado]

13

Los tipos de AFAIU pueden ser Setcuyos elementos son programas o propositioncuyos elementos son pruebas. Entonces, en base a este entendimiento:

Inductive prod (X Y: Type) : Set := 
| pair: X -> Y -> prod X Y.

El siguiente código debe compilarse, pero no se debe al siguiente error. Si cambio Setcon Typeu otro Typecon Setél se compila bien. ¿Alguien puede ayudarme a entender lo que significa el siguiente error? Estoy tratando de enseñarme Coq usando el libro de Fundamentos de Software.

Error:

Error: Large non-propositional inductive types must be in Type.
Abhishek Kumar
fuente
2
Los probadores de teoremas siempre han sido un área gris para CS.SE, pero supongo que este es un buen candidato para que los mods migren a StackOverflow.
jmite
Esta pregunta tiene algunas respuestas aquí .
Anton Trunov
@jmite Dado que esta pregunta es sobre el cálculo de las construcciones con Coq simplemente sirviendo como sintaxis concreta, creo que está en el tema aquí.
Gilles 'SO- deja de ser malvado'

Respuestas:

12

Coq tiene 3 tipos "grandes":

  • Propestá destinado a proposiciones. Es impredicativo, lo que significa que puede crear instancias de funciones polimórficas con tipos polimórficos. También tiene irrelevancia de prueba, lo que significa que si entonces . Esto permite que los términos que solo se usan para la prueba se borren en cualquier código generado por Coq.p1,p2:Pp1=p2
  • Setestá destinado a la computación. Es predicativo y no tiene irrelevancia de prueba, lo que le permite hacer cosas buenas como no suponer . Las partes permanecen durante la extracción del código.1=2Set
  • Type es un supertipo de ambos, lo que le permite escribir código una vez que funciona con cualquiera

Estoy bastante seguro de que su error se debe a que está definiendo un Setcuyos parámetros pueden ser Type, lo que significa que pueden ser Prop, lo que no está permitido. Si cambia a esto:

Inductive prod (X Y: Set) : Set := 
| pair: X -> Y -> prod X Y. 

Tu código debería funcionar.

jmite
fuente
3
Coq no tiene prueba de irrelevancia a Propmenos que lo agregue como axioma.
Geoff