Qu'est-ce qu'un constructeur dans Coq?

J'ai du mal à comprendre les principes de ce qu'est un constructeur et comment il fonctionne.Qu'est-ce qu'un constructeur dans Coq?

Par exemple, en Coq, nous avons appris à définir les nombres naturels comme celui-ci:

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

Et ont été dit que S est un constructeur, mais qu'est-ce que cela signifie exactement?

Si je fais alors:

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

Je reçois qu'il est 4 et de type nat.

Comment cela fonctionne-t-il, et comment Coq sait-il que (S (S (S (S O)))) représente 4?

Je suppose que la réponse à ceci est une magie d'arrière-plan extrêmement intelligente dans Coq.

Source

2011-02-23 Jerome

La jolie impression de '(S (S (S (SO))))' comme '4' est juste la commodité que vous ne devriez pas laisser vous distraire. Si vous êtes au point où vous voulez avoir une idée de ce qu'est un constructeur, définissez votre propre type 'naturals' avec les constructeurs' Z' (pour zéro) et 'N' (pour next). Alors rien de magique n'arrivera. –

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

dit les choses suivantes:

Z est un terme de type naturals
lorsque e est un terme de type naturals, N e est un terme de type naturals.
L'application de Z ou N est la seule façon de créer un élément naturel. Quand on lui donne un naturel arbitraire, vous savez qu'il a été fabriqué à partir de l'un ou de l'autre.
deux termes e1 et e2 de type naturals sont égaux si et seulement si elles sont à la fois Z ou si elles sont respectivement N t1 et N t2 avec t1 égal à t2.

Vous pouvez voir comment ces règles généraliseraient à des définitions de type inductif arbitraires. Cependant, il se trouve que lorsque la définition de type est pour les constructeurs de la forme de Z et N, ces propriétés correspondent plus ou moins exactement à Peano's axioms pour les nombres naturels. C'est pourquoi un type nommé nat est prédéfini en Coq avec des constructeurs de ces formes à utiliser pour représenter des nombres naturels. Ce type reçoit un traitement spécial car il se fatigue très rapidement pour manipuler la forme brute, mais les traitements spéciaux ne sont là que pour plus de commodité.

Source

2011-02-23 12:18:50

Au point 2, vouliez-vous dire que N e est un terme de type naturals? – mushroom

@mushroom Oui, je l'ai fait. –

-1

En théorie des types, un constructeur (type) est juste un moyen de construire de nouveaux types à partir de ceux existants (http://en.wikipedia.org/wiki/Type_constructor). Dans votre définition inductive de nat, S est un constructeur car (si vous regardez la signature) il prend un nat et produit un autre nat.

Par exemple, un constructeur de type pour une paire de nats sera:

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

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

Source

2011-02-23 18:18:48 GClaramunt

Cette réponse est un peu trompeuse: le fait que 'S' soit un constructeur n'est pas déterminé par son type. Par exemple 'plus 1' n'est pas un constructeur (même s'il a le même type que' S' et même eta-s'y réduit). 'S' est un constructeur parce que c'est l'un des moyens" canoniques "de construire un' nat'. Il est important que les constructeurs d'un type soient les seuls moyens de construire des objets de ce type. – Gilles

Oui, vaut la peine de préciser que je parlais dans le contexte d'une définition de type (inductive). Une fonction ordinaire n'est pas un constructeur de type même si elle partage la même signature de type. (si c'est de cela dont vous parlez) – GClaramunt

J'ai peut-être mélangé les noms, je pense qu'on les appelle constructeurs de valeur – GClaramunt

Qu'est-ce qu'un constructeur dans Coq?

Répondre

Questions connexes