Lazi

essai 2

Arguments égaux par calcul

Contexte

Nous allons montrer ici que deux formules égales par calcul se comportent de manière identiques du point du vue du calcul. Si on voit ça du point de vue informatique, la notion "égal par calcul" est la notion d'équivalence calculatoire des fonction pure si on considère qu'une boucle infinie est équivalente à une autre.

Nous nous servirons de ce résultat pour le théorème "Recherche:Roadmap:5 Vérif types:4 Définir extensions:1 Mots clés:3 Traduction sans hypothèse:Règle du tiers exclu:Toute vérité se calcule en une égalité:Rebut:essai 2:Rebut:Toute vérité se calcule en une égalité".

Énoncé

Variables

a, b, c

Conditions

  • a, b et c sont des formules
  • b =c c

Conclusion

a +f b =c a +f c

Recherche d'une preuve

Caneva de la preuve

La deuxième condition de la définition de =c est évidente (faux), il nous reste à montrer la première: si a +f b est calculable alors a +f c est calculable, et inversement.

Pour cela nous allons montrer qu'une certaine similarité persiste entre a +f b et a +f c lors de leur calcul. Cette similarité fait que la chaîne de calcul est identique pour les deux, et donc si l'un est calculable l'autre aussi.

Il nous reste à voir d'où provient cette similarité.

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.

Essai 1

On remplace b et c par une variable x. On a 3 cas:

  1. le calcul n'a jamais à évaluer x
  2. une évaluation de x est nécessaire pour une confition d'un if
  3. une évaluation de x est nécessaire en tant que fonction

Cas 1 :

Peut importe si le calcul se termine ou non, le calcul de a +f b et a +f c restent similaires

Cas 2 :

Du fait que b =c c, le résultat est similaire du point de vue du test du if (à prouver), donc les calculs continuent sans différenciation.

Cas 3 :

Remarquons que l'évaluation de x peut nécessiter des arguments extérieur à x.

Preuve

Pour prouver a +f b =c a +f c, nous allons supposer que a +f b est calculable et prouver que le calcul de a +f c est similaire à celui de a +f b. Pour cela nous allons montrer une propriété par récurrence sur la longueur du calcul de a +f b.

Pour deux formules x et y soit "x =s y" définie par :

  • x = y ou
  • x et y sont des applications x1 +f x2 et y1 +f y2 avec x1 =c y1 et x2 =c y2

Remarque =s est comme =c moins la condition sur la calculabilité.

La propriété prouvée par récurrence est "=s" appliquée aux deux formules calculées.

Si le calcul est de longueur nul

Cela implique que a +f b est un calcul terminé.
D'après le théorème "La terminaison d'un calcul est indépendante du dernier argument" on déduit que a +f c est un calcul terminé.
Il nous reste à montrer que a +f b =s a +f c. Pour cela nous montrerons directement la deuxième condition de la disjonction définissant "=s". Comme =c est réflexive on a a =c a, par hypothèse on a b =c c. Donc on a a +f b =s a +f c.

=s et →c1

Soit x et y tels que x =s y. Soit z et t tels que x →c1 z et y →c1 t.
Si x = y alors z = t et donc z =s t.
Sinon, x et y sont des applications x1 +f x2 et y1 +f y2 avec x1 =c y1 et x2 =c y2.

Si la règle "calcul de la fonction" s'applique à x : soit z1 tel que x1 →c1 z1. On a z = z1 +f x2.