Logique Equationnelle

Dans ce chapitre, nous présentons la logique dite équationnelle, utilisée pour faire la preuve de théorèmes et nous établissons le lien entre les théorèmes d'une spécification et les propriétés des opérations dans les modèles de la spécification.

En logique mathématique, une spécification algébrique peut être considéré comme décrivant une théorie dont les théorèmes dits “déductifs” sont déduits des axiomes.

Exemple

add(succ(succ(zero)),succ(zero)) = succ(succ(succ(zero)))

Ceci est une théorème de la théorie décrite par la spécification pour les entiers.

Les règles de déduction sont les règles de remplacement d'égaux à égaux (bien comme en mathématiques) et constituent la logique équationnelle (ainsi nommée parce que les théorèmes sont des équations).

Les règles de la logique équationnelle sont :

  1. réflexivité : t = t
  2. symétrie : t = t' ⇒ t' = t
  3. transitivité : t=t', t'=t ⇒ t = t
  4. substitution : t=t' ⇒ t[x\u] = t'[x\u]
  5. congruence : t1=t1' & t2=t2' & … & tn=tn' ⇒ f(t1,t2,…tn) = f(t1',t2',…tn') où
    • t1,t1',t2,t2'…tn sont des termes
    • x est une variable
    • f est un nom d'opération (d'arité n)

Exemple

Le théorème précédent peut être déduit à partir d'axiomes de la façon suivante :

1 add(m, zero) = m axiome
2 add(succ(succ(zero)),zero) = succ(succ(zero)) substitution (dans 1)
3 succ(add(succ(succ(zero)),zero)) = succ(succ(succ(zero))) congruence de succ appliqué en 2
4 add(m,succ(n)) = succ(add(m,n)) axiome
5 add(succ(succ(zero)),succ(zero)) = succ(add(succ(succ(zero)),zero) substitution de succ(succ(zero)) pour m, zero pour n dans (4)
add(succ(succ(zero)),succ(zero)) = succ(succ(succ(zero))) transitivité : de (5) et (3)

Le lien entre théorèmes déductifs d'une spécification et leur interprétations dans les modèles de la spécification est donné par le Théorème de Gödel-Birkhoff, que voici :

Théorème

Tout théorème déductif d'une spécification est valide dans tout modèle de la spécification. Inversement, toute équation valide dans tout modèle d'une spécification est un théorème déductif de la spécification.

Remarque

Certaines équations sont valides dans un modèle bien que l'on ne puisse pas les déduire en utilisant la seule logique équationnelle. De tel théorèmes sont dits inductifs car beaucoup d'entre eux peuvent être démontrés par induction.

théorème inductif

toute équation t = t' est un théorème inductif si tout équation en substituant les variables de t et t' par des termes clos est un théorème déductif.

remarque : tout théorème déductif est un théorème inductif

Exemple

sup(succ(m),m) = vrai est un théorème inductif qui n'est pas déductif. Pour démontrer ce théorème, il faut utiliser le principe d'induction comme il a été vu au chapitre de la sémantique dénotationnelle pour démontrer une propriété d'un langage. Contrairement aux théorèmes déductifs, les théorèmes inductifs ne sont pas valides dans tous les modèles. Ils sont valides dans les modèles initiaux.

 
m1ilc/semantics_c.txt · Dernière modification: 2010/05/24 11:18 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