Nous avons vu que plusieurs Σ-algèbres pouvaient être associées à une signature Σ. Parmi ces Σ-algèbre certaines ne correspondent pas au type que l'on souhaite spécifier.
Par exemple, dans l'interprétation Num4 de Nat, 3 est plus grand que son successeur, ce qui est correcte dans cette algèbre, mais incorrecte dans ce que nous voulions spécifier, le type des entier naturels.
Les axiomes permettent de préciser quelles sont les algèbres qui conviennent.
Ajoutons à [Nat Bool]
les axiomes suivants:
Considérons l'axiome sup(succ(m), zero) = vrai
. Si on remplace m par le terme succ(succ(succ(zero) ) )
dans l'algèbre Num4, l'interprétation du nombre gauche est
supNum4(succNum4(3),zero) ={0>0} = faux
alors que l'interprétation du membre droit est vrai
. Autrement dit, l'algèbre Num4 ne valide pas cet axiome. Par contre, l'algèbre Num valide [toutes les équations] tous les axiomes.
Nous somme intéressés par les algèbres qui valident tous les axiomes [toutes les équations].
soit Σ une signature et E un ensemble d'axiomes de cette signature. Une Σ-algèbre qui valide toutes les équations (axiomatiques) est appelée modèle de la spécification définie par Σ et E.
Par exemple, Num est un modèle pour notre spécification pour les entiers naturels, Num4 ne l'est pas : Num4 ne valide pas toutes les axiomes.
Intuitivement, nous choisirons la sémantique d'une spécification parmi l'ensemble des modèles. Selon les modèles retenus, la sémantique est différente. Ainsi, plusieurs sémantiques peuvent être définies.
Une sémantique possible est l'ensembe de tous les modèles. Cette sémantique ne paraît pas donner une idée précise de la structure caractéristique du type spécifié mais seulement de démontrer des théorèmes à partir des axiomes en utilisant la logique équationnelle. Pour cette raison, cette sémantique est dite “lâche”.
Dans la suite, nous définissons une sémantique plus précise – la sémantique initiale– en considérant uniquement les modèles dont les ensembles supports satisfont certaines propriétés.
Parmi les modèles, certains ont un ensemble support trop grand au sens où un élément n'est l'interprétation d'aucun terme clos. Un tel élément est appelé rossignol (ou “junk” en anglais).
Inversement, certains modèles ont un ensemble support trop petit au sens où un élément est l'interprétation de deux (ou plusieurs) termes clos t1 et t2, alors que t1=t2 ne peut être déduit des axiomes. Un tel élément est appelé confusion.
Dans une spécification Bool
par exemple, BoolB0 = {vrai, faux, peut-être} a un rossignol (peut-être) qui n'est l'interprétation d'aucun terme clos. BoolB1={faux} ne distingue pas “vrai” et “faux” donnant la valeur “faux” à v et f, il les confond, les confuse : une confusion (et v=f n'est pas un théorème).
N.B. On fait ici référence à la notion de théorème déductif que l'on peut démontrer à partir des axiomes en utilisant les règles de la logique équationnelle.
Intuitivement, les modèles les plus intéressants sont ceux sans rossignols ni confusions.
un modèle est dit initial s'il est sans rossignol ni confusion.
Le modèle initial existe toujours, quelque soit la spécification. On peut toujours le construire à partir de l'algèbre des termes clos. |
---|
L'effet de rajouter des axiomes à une spécification est de partitionner (on dit aussi quotiener) l'ensemble des termes clos en classes d'équivalence.
Les axiomes identifient certains termes syntaxiquement distinctes et sémantiquement égaux. incomplet…
Une sémantique pour une spécification algébrique est une famille de modèles ce cette spécification. On distingue :
modèle*
veut dire sémantique lâchemodèle!
veut dire sémantique initiale