Calcul et remplacement

Contexte

Nous serons amenés à comparer les calcul d'une formule x avec x où une partie est remplacée par une autre (voir 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:Toute vérité se calcule en une égalité". Nous allons voir ici que lors d'un calcul une sous-partie ne peut subir que les traitements suivant:

duplication et déplacement (par la règle distribute)
comparaison à 1b ou 0b (argument de if)
calcul (argument de if ou position de fonction)

Ce qui fait que si on remplace une partie d'une formule par une formule de même calculabilité et, si elle est calculable alors elle est de même résultat de calcul, alors la calculabilité de la formule globale est inchangée.
Remarquons que la valeur syntaxique du résultat du calcul de la formule globale peut être changée: par exemple si dans equal (if 1b 0b 0b) on remplace if 1b 0b 0b par if 0b 0b 0b, le résultat final passe de equal (if 1b 0b 0b) à equal (if 0b 0b 0b).

Énoncé

Conditions

x, y,z et t sont des formules lazi.0.0 telles que

x =c z
on a la disjonction:
- x est une fonction constante par calcul
- y =c t

Conclusion

x +f y =c z +f t

Preuve

Nous allons prouver le théorème par récurrence. Soit x,y,z,t tels que dans les conditions.

Calculons x +f y et z +f t pour montrer que x +f y =c z +f t.

On utilise une forme du premier ordre du tiers exclu pour explorer deux cas: x est ou non calculable.

Si x n'est pas calculable alors z n'est pas calculable, donc x +f y et z +f t ne sont pas calculables et on a donc par définition x +f y =c z +f t.

Si x est calculable, soit xc le résultat du calcul de x et zc le résultat du calcul de z. Les calculs de x +f y et z +f t reviennent à calculer xc +f y et zc +f t.

Comme x =c z, nous avons deux cas:

xc = zc

Si le calcul de xc +f y ou xc +f t est terminé, comme la terminaison d'un calcul ne dépend pas de la valeur du dernier argument cela implique que les deux sont des calculs terminés et comme xc =c zc et y =c t, on a x +f y =c z +f t.

Si le calcul de xc +f y n'est pas terminé, alors c'est aussi le cas de zc +f t. Comme l'application d'une règle sur une formule est indépendante du dernier argument, la règle de calcul applicable à xc +f y ou xc +f t est la même.

Si la règle 1 "if 1b" s'applique : alors y et t sont éliminés, et donc le résultat est syntaxiquement identique, on a donc x +f y =c z +f t.

Si la règle 2 "if 0b" s'applique: on obtient y et t. Comme on a y =c t, on démontre facilement que x +f y =c z +f t.

Si la règle 4 "if x" s'applique: la règle continue à s'appliquer soit:

indéfiniment, et alors x +f y et z +f t ne sont pas calculables, on a donc x +f y =c z +f t.
jusqu'à ce que la règle "if 1b" ou "if 0b" puisse s'appliquer, et on a déjà traité ce cas
la condition du if est calculable mais n'aboutit ni à 0b ni à 1b, le calcul est terminé avec des valeurs de la forme xc2 +f x et xc2 +f y. Comme xc2 =c xc2 et x =c y, on a x +f y =c z +f t.

La règle 5 "calcul de la fonction" ne peut s'appliquer car xc est un calcul terminé.

Si la règle 3 "distribute" s'applique: soit a et b telles que xc = $F[distribute] +f a +f b, le résultat est de la forme (a +f y) +f (b +f y) et (a +f t) +f (b +f t).

Récurrence sur les sous-formules utilisées par un calcul
Si on peut appliquer la récurrence: il nous faut l'appliquer sur le 4-uple (a +f y, b +f y, a +f t, b +f t) et montrer que a +f y =c a +f t et b +f y =c b +f t.

Pour cela on applique à nouveau la récurrence sur a,y,a,t : on a a =c a, b =c b par définition de =c et y =c t par hypothèse de départ. Donc on obtient a +f y =c a +f t et b +f y =c b +f t.

xc et zc sont des applications

Soit xc1 +f xc2 et zc1 +f zc2 ces applications. Par définition de =c, nous avons xc1 =c zc1 et xc2 =c zc2

@todo