¿Qué es un constructor en Coq?

Question

Tengo problemas para entender los principios de qué es un constructor y cómo funciona.

Por ejemplo, en Coq, se nos ha enseñado a definir los números naturales como este:

Inductive nat : Type := 
    | O : nat 
    | S : nat -> nat. 

y me han dicho que S es un constructor, pero ¿qué significa eso exactamente?

Y si lo:

Check (S (S (S (S O)))). 

consigo que es 4 y de tipo nat.

¿Cómo funciona esto, y cómo Coq sabe que (S (S (S (S O)))) representa 4?

Supongo que la respuesta a esto es una magia de fondo extremadamente inteligente en Coq.

Answer 1

Inductive naturals : Type := 
    | Z : naturals 
    | N : naturals -> naturals. 

dice lo siguiente:

1. Z es un término de tipo naturals

2. cuando e es un término de tipo naturals, N e es un término de tipo naturals.

3. Aplicar Z o N son las únicas dos maneras de crear un natural. Cuando se le da un natural arbitrario, usted sabe que fue hecho de uno o del otro.

4. dos términos e1 y e2 de tipo naturals son iguales si y sólo si ambos son Z o si son respectivamente N t1 y N t2 con t1 igual a t2.

Puede ver cómo estas reglas se generalizarían a definiciones de tipo inductivo arbitrarias. Sin embargo, resulta que cuando la definición de tipo es para constructores de la forma Z y N, estas propiedades corresponden más o menos exactamente a Peano's axioms para números naturales. Esta es la razón por la que un tipo denominado nat está predefinido en Coq con constructores de estas formas que se utilizarán para representar números naturales. Este tipo recibe un tratamiento especial porque se cansa muy rápido para manipular la forma cruda, pero los tratamientos especiales solo están disponibles para su comodidad.

Answer 2

En teoría de tipos, un constructor (tipo) es solo una forma de construir nuevos tipos a partir de los existentes (http://en.wikipedia.org/wiki/Type_constructor).

En su definición inductiva de nat, S es un constructor porque (si mira la firma) toma un nat y produce otro nat.

Por ejemplo, un constructor de tipo para un par de NAT será:

Inductive pair : Type := P: nat->nat->pair. 

Check P (S (O)) (S(S(O))).