Sémantique d'une Spécification

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:

  • add(n,zero) = n
  • add(m, succ(n) )= succ(add(m,n) )
  • sup(zero,sero) = faux
  • sup(zero,succ(n) ) = faux
  • sup(succ(n), zero) = vrai
  • sup(succ(m),succ(n) ) = succ(sup(m,n) )

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].

modèle

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.

Rossignols et confusions

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.

modèle initiale

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.

Construction du modèle initial à paritr 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. FIXME incomplet…

Conclusion

Une sémantique pour une spécification algébrique est une famille de modèles ce cette spécification. On distingue :

  • la sémantique lâche, qui comporte tous les modèles
  • la sémantique initiale, qui comporte les modèles initiaux (isomorphes entre eux). En CafeOBJ, le spécificateur peut indiquer laquelle de ces sémantiques il souhaite associer à sa spécification.
    • modèle* veut dire sémantique lâche
    • modèle! veut dire sémantique initiale

Spécification Algébrique ⇐ * ⇒ Logique Equationnelle

 
m1ilc/semantics_b.txt · Dernière modification: 2010/05/27 22:33 par suitable
 
Sauf mention contraire, le contenu de ce wiki est placé sous la licence suivante :CC Attribution-Noncommercial-Share Alike 3.0 Unported
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki