Lazi

Recherche d'une preuve

Propriétés des calculs

Lors d'un calcul une partie d'une formule (comme b dans a +f b) ne peut être que soit:

  • déplacée ou copiée
  • évaluée pour être testée par if
  • évaluée en tant que fonction

Le déplacement ou la copie ne différencie pas les différentes parties.

Une partie incalculable, pour chacun des 3 cas, ne peut être différenciée d'une autre partie incalculable, ce qui fait que l'on peut voir les parties incalculables comme équivalentes, ce que fait l'égalité par calcul.

Deux parties égales par calcul ne peuvent se différencier que par les sous-formules incalculables. Hors comme elles sont indistinguables l'une de l'autre du point de vue du calcul, cela implique que les deux parties égales par calcul sont indistinguables dans le calcul, les deux calculs sont donc identiques et les formules produites ne sont différentes que par les sous-formules incalculables. Elles sont donc égales par calcul.

Les remplacement et ajout de règles de calcul

L'idée est d'ajouter des variables à une formules et des règles de calcul pour calculer ces variables de sorte que le calcul avec variables soit équivalent au calcul où l'on remplace les variables par certaines valeurs. De cette manière, on montre que les calculs pour deux formules sont équivalents en passant par un troisième calcul (avec variables).

On peut le faire avec les sous-formules incalculable: on remplace toutes les sous-formules incalculables par une variable i et on ajoute la règle de calcul i → i

Les sous-théorèmes nécessaires

  • x =c y ssi en remplaçant les sous-formules incalculables par une variable inutilisée les deux formules deviennent égales.

La preuve

C'est une application évidente du théorème décrit ci-dessus