Lazi

règle de calcul (simplifiante,finale,composition)

Contexte

En Lazi une règle de calcul est une règle de déduction désuisant une égalité x *=* y où x est le seul paramètre de la règle. C'est donc un moyen systématique de trouver une chose égale à une autre.

Remarquons qu'un calcul (au sens commun) se ramène toujours à des égalités. Par exemple si on calcul les états successifs d'une machine symbolique, cela revient à déterminer les égalités f(mn)=mn+1 où mk est l'état de la machine à l'étape k et f est la fonction calculant l'état suivant.

On définira une notion naturelle de composition car on peut voir une règle de calcul comme une fonction sur les formules associant y à x. On verra que la composition de deux règles de calcul est une règle de calcul (éventutellement de domaine vide).

La notion de règle simplifiante signifie que le calcul finit par aboutir à des éléments simples quand cela est possible.

Définitions

Règle de calcul

Soit M une mathématique et d une règle de déduction de M. On dit que d est une règle de calcul ssi elle déduit une vérité de forme x *=* y où x est l'unique paramètre de d et où y est syntaxiquement différent de x.

Composition de deux règles de calcul

Soit R et S deux règle de calcul.
Soit T le type défini par :

  • x est dans le domaine de T si x est dans le domaine de R et si la formule calculée par R sur x est dans le domaine de S
  • soit x dans le domaine de T, soit y tq R déduit x *=* y, soit z tq S déduit y *=* z, alors T a pour objet x *=* z.

Règle de calcul simplifiante

On dit que la règle est simplifiante ssi on a la conjonction suivante :

  • Quand x est égal à un mot clé lazi.0 alors la composition de la règle sur elle-même récursivement aboutit à déduire l'égalité à ce mot.
  • Si x est une formule n'appartenant pas au domaine de la règle, alors ses sous-formules non plus.

Remarque : informellement la deuxième condition revient à ce que toute sous-formule soit aussi calculée et simplifiée.

Règle de calcul finale

On dit qu'une règle de calcul est finale ssi on a la conjonction suivante :

  • C'est une règle simplifiante.
  • La règle composée à elle même est un type de domaine vide.

Remarques :

  • La dernière condition revient à dire que l'on aboutit au résultat final en une fois.
  • Lors du calcul du résultat de la règle, les calculs élémentaires étant en nombre illimité, le calcul du domaine de cette règle peut être infini si le calcul de la formule en argument est infini.