Lazi

Théorème des calculs et de l'égalité structurelle

Contexte

Pour prouver le théorème de conservation de la calculabilité par =c on a besoin de prouver une propriété sur =s.

Énoncé

Variables

x1,x2,y1,y2

Conditions

  • x1,x2,y1,y2 sont des formules
  • x1 =s y1
  • x2 =s y2

Conclusion

x1 +f x2 =s y1 +f y2

Preuve

Soit R la relation définie dans le théorème de l'ordonnancement des calculs. Du fait que l'ensemble des formules est dénombrable et que la condition de chaîne descendante est vraie, il existe un isomorphisme O de (ℕ,>) vers (l'ensemble des formules calculables,R).

Nous utiliserons cette fonction O pour prouver le théorème par récurrence.

Soit P la propriété sur ℕ définie par : P n =

Pour toute formules x1,x2,y1,y2 vérifiant :
- x1 =s y1
- x2 =s y2
- O x1 ≤ n
- O y1 ≤ n
- O x2 ≤ n ou le calcul de x1 +f x2 ne passe pas par x2
- O y2 ≤ n ou le calcul de y1 +f y2 ne passe pas par y2
alors
x1 +f x2 =s y1 +f y2

Montrons que P est vrai pour tout entier ≥0 par récurrence.

Prouvons P 0 :

Soit x1,x2,y1,y2 tels que dans les conditions de P 0.
D'après la définition de R, on voit que O 0 est un mot.
x1,x2,y1,y2 sont le même mot, aucune règle de calcul n'existe pour l'application de deux mots, donc x1 +f x2 et y1 +f y2 ont leur calcul terminé. Donc d'après la définition de =s, on a x1 +f x2 =s y1 +s y2.

Supposons P n et prouvons P (n+1) :

Soit x1,x2,y1,y2 tels que dans les conditions de P n. On a :
- Si x1 est incalculable, alors x1 +f x2 l'est aussi, ainsi que y1 (car x1 =s y1) et donc y1 +f y2. Donc x1 +f x2 =s y1 +s y2.
- Si x1 est calculable alors y1 l'est aussi (car x1 =s y1). Soit x1c et y1c tq x1 →ct x1c et y1 →ct y1c. On a :
- Si x1c +f x2 est de la forme $F[ if ] +f ax +f bx +f x2 :
Alors d'après le théorème de la décomposition par égalité structurelle, y1c est de la forme $F[ if ] +f ay +f by +f y2 avec ax =s ay, bx =s by. On a les cas suivants :
- si ax est incalculable : alors ay l'est aussi et x1c +f x2 ainsi que y1c +f y2 sont incalculables. Comme x1 +f x2 →c x1c +f x2, x1 +f x2 est incalculable, de même pour y1 +f y2. Donc x1 +f x2 =s y1 +s y2.
- si ax →c $F[ 1b ] : alors, par définition de =s, ay →c $F[ 1b ]. Donc x1c +f x2 →c1 bx et y1c +f y2 →c1 by. On a donc x1 +f x2 →c bx et y1 +f y2 →c by avec bx =s by. Donc x1 +f x2 =s y1 +s y2.
- si ax →c $F[ 0b ] : Par un raisonnement similaire à celui pour le cas "ax →c $F[ 1b ]" on aboutit à la même conclusion.
- si ax possède un calcul terminé axc différent de $F[ 1b ] et $F[ 0b ] : comme ax =s ay, ay est dans le même cas, soit ayc son calcul terminé. Donc x1 +f x2 →ct $F[ if ] +f axc +f bx +f x2 et y1 +f y2 →ct $F[ if ] +f ayc +f by +f y2. D'après le théorème de recomposition par égalité structurelle, on a $F[ if ] +f axc +f bx +f x2 =s $F[ if ] +f ayc +f by +f y2. On a donc x1 +f x2 =s y1 +s y2.
Nous voyons donc que dans tous les cas on a x1 +f x2 =s y1 +s y2.
- Si x1c +f x2 est de la forme $F[ distribute ] +f ax +f bx +f x2 :
Alors d'après le théorème de la décomposition par égalité structurelle, y1c est de la forme $F[ distribute ] +f ay +f by +f y2 avec ax =s ay, bx =s by. On a :
- $F[ distribute ] +f ax +f bx +f x2 →c1 (ax +f x2) +f (bx +f x2)
- $F[ distribute ] +f ay +f by +f y2 →c1 (ay +f y2) +f (by +f y2)
Nous allons prouver (ax +f x2) +f (bx +f x2) =s (ay +f y2) +f (by +f y2), pour en déduire x1 +f x2 =s y1 +s y2. Pour cela nous allons utiliser l'hypothèse de récurrence.
Come x1 +f x2 →c (ax +f x2) +f (bx +f x2), on a O ((ax +f x2) +f (bx +f x2)) ≤ n, de même on a O ((ay +f y2) +f (by +f y2)) ≤ n.
Par définition de l'ordre sur les formules, on a O (ax +f x2)≤ n (car R((ax +f x2) +f (bx +f x2)),(ax +f x2)). De même pour les y, on a O (ay +f y2)≤ n.
Si le calcul de (ax +f x2) +f (bx +f x2) passe par bx +f x2, alors on a O(bx +f x2) ≤ n. Sinon, alors on vérifie directement la condition de P.
Il en est de même pour la partie y.
Pour pouvoir appliquer P n, il nous reste à montrer que ax +f x2 =s ay +f y2 et bx +f x2 =s by +f y2. Pour cela nous allons recommencer le raisonnement ci-dessus mais cette fois ci sur ax,ay,x2,y2 :
Comme O(ax +f x2) ≤ n, on a O ax ≤ n. On a déjà ax =s ay, x2 =s y2 et bx =s by. Soit le calcul de ax +f x2 ne passe pas par x2, soit le calcul de ax +f x2 passe par x2 et alors O x2 ≤ n. Donc dans tous les cas les conditions de P n sont réalisées. Il en est de même de la partie y. Donc on peut appliquer P n ce qui nous donne ax +f x2 =s ay +f y2 et bx +f x2 =s by +f y2.
Nous pouvons donc appliquer P n, ce qui nous donne (ax +f x2) +f (bx +f x2) =s (ay +f y2) +f (by +f y2).
- Si le calcul de x1c +f x2 est terminé.
- Si le calcul de y1c +f y2 n'est pas terminé : alors y1c +f y2 est de la forme $F[ if ] +f ay +f by +f y2 ou $F[ distribute ] +f ay +f by +f y2. Par le théorème de la décomposition par égalité structurelle x1c +f x2 est sous une forme similère et donc les cas sont déjà traité ci-dessus. Remarque: le cas "distribute" n'est pas possible, mais ça n'a pas d'importance pour le raisonnement.
-Si le calcul de y1c +f y2 est terminé : l'application directe de la définition de =s nous donne x1 +f x2 =s y1 +s y2.
Donc dans tous les cas nous avons x1 +f x2 =s y1 +s y2. Donc P (n+1) est vrai.

Donc par récurrence, pour tout n∈ℕ, P n. Comme pour toute formules x1,x2,y1,y2 il existe n tq O x1 ≤ n, O x2 ≤ n , O y1 ≤ n et O y2 ≤ n, on en déduit l'énnoncé du théorème.

CQFD

Recherche d'une preuve

Essai 3

Contexte

L'essai 2 marche presque, mais il y a un problème pour le cas "distribute", quand les arguments ne sont pas calculés, car alors on n'a pas forcément un argument inférieur pour l'ordre de calcul, ce qui empêche d'utiliser la récurrence. De plus il faut changer la relation R sur l'ordre des formules pour inclure les sous-fonctions.

Comment palier au problème ?

En changeant l'énnoncé de P

Ancien P :

Soit P la propriété sur ℕ définie par : P n =
Pour toute formules x1,x2,y1,y2 vérifiant :
- O (x1 +f x2) ≤ n
- O (y1 +f y2) ≤ n
- x1 =s y1
- x2 =s y2
alors
x1 +f x2 =s y1 +f y2

Nouveau P :

Soit P la propriété sur ℕ définie par : P n =
Pour toute formules x1,x2,y1,y2 vérifiant :
- x1 =s y1
- x2 =s y2
- O x1 ≤ n
- O x2 ≤ n ou le calcul de x1 +f x2 ne passe pas par x2
- O y1 ≤ n
- O y2 ≤ n ou le calcul de y1 +f y2 ne passe pas par y2
alors
x1 +f x2 =s y1 +f y2

Preuve partielle

On preprend la preuve de l'essai 2 sur la partie "distribute".

- Si x1c +f x2 est de la forme $F[ distribute ] +f ax +f bx +f x2 :

Alors d'après le théorème de la décomposition par égalité structurelle, y1c est de la forme $F[ distribute ] +f ay +f by +f y2 avec ax =s ay, bx =s by. On a :
- $F[ distribute ] +f ax +f bx +f x2 →c1 (ax +f x2) +f (bx +f x2)
- $F[ distribute ] +f ay +f by +f y2 →c1 (ay +f y2) +f (by +f y2)
Nous allons montrer que (ax +f x2) +f (bx +f x2) =s (ay +f y2) +f (by +f y2) en appliquant P n :
Come x1 +f x2 →c (ax +f x2) +f (bx +f x2), on a O ((ax +f x2) +f (bx +f x2)) ≤ n, de même on a O ((ay +f y2) +f (by +f y2)) ≤ n.
Par définition de l'ordre sur les formules, on a O (ax +f x2)≤ n ainsi que pour ax, ay +f y2 et ay.
Si le calcul de (ax +f x2) +f (bx +f x2) passe par bx +f x2, alors on a O(bx +f x2) ≤ n. Sinon, alors on vérifie directement la condition de P.
Il en est de même pour la partie y.
Pour pouvoir appliquer P n, il nous reste à montrer que ax +f x2 =s ay +f y2 et bx +f x2 =s by +f y2. Pour cela nous allons recommencer le raisonnement ci-dessus mais cette fois ci sur ax,ay,x2,y2 :
Comme O(ax +f x2) ≤ n, on a O ax ≤ n. On a déjà ax =s ay, x2 =s y2 et bx =s by. Soit le calcul de ax +f x2 ne passe pas par x2, soit le calcul de ax +f x2 passe par x2 et alors O x2 ≤ n. Donc dans tous les cas les conditions de P n sont réalisées. Il en est de même de la partie y. Donc on peut appliquer P n ce qui nous donne ax +f x2 =s ay +f y2 et bx +f x2 =s by +f y2.
Nous pouvons donc appliquer P n, ce qui nous donne (ax +f x2) +f (bx +f x2) =s (ay +f y2) +f (by +f y2).

Essai 2

Contexte

Plutôt que d'utiliser =ss, qui est équivalente à =s quand les formules ont leur calcul terminé (voir les problèmes avec le théorème des calculs et de =ss), il semble plus simple de ne pas utiliser cette relation et plutôt de définir une relation d'ordre partielle sur les formules calculables (x est plus grande que y si x engendre y).

Recherche d'un ordre sur les formules pour la récurrence

Il faut que les sous-formules calculées lors du calcul de la formule globale soit inférieur à la formule globale.

Remarquons qu'une formule peut se contenir en sous-formule, mais si elle était calculée on aurait forcément une boucle infinie. De manière générale, si b est une sous-formule calculée (lors du calcul de a) de a, on ne peut avoir la réciproque car sinon le calcul de a (ou b) serait infini.

Canevas

On prouve que sur l'ensemble des formules calculables la relation →c est un ordre partiel. On fait une récurrence sur cet ordre.

Preuve

D'après le théorème de l'ordonnancement des calculs et du fait que l'ensemble des formules est dénombrable, il existe une fonction O de l'ensemble des formules calculables vers ℕ, tq pour deux formules calculables x et y, si le calcul de x passe par y alors O y < O x et tel que si O x <5 alors x est un mot (if, 1b, 0b, equal, distribute).

Soit P la propriété sur ℕ définie par : P n =

Pour toute formules x1,x2,y1,y2 vérifiant :
- O (x1 +f x2) ≤ n
- O (y1 +f y2) ≤ n
- x1 =s y1
- x2 =s y2
alors
x1 +f x2 =s y1 +f y2

Montrons que P est vrai pour tout entier ≥0 par récurrence.

Prouvons P 0 :

Soit x1,x2,y1,y2 tels que dans les conditions de P 1.
x1,x2,y1,y2 sont des mots, aucunne règle de calcul n'existe pour l'application de deux mots, donc x1 +f x2 et y1 +f y2 ont leur calcul terminé. Donc x1 +f x2 =s y1 +s y2.

Supposons P n et prouvons P (n+1) :

Soit x1,x2,y1,y2 tels que dans les conditions de P n. On a :
- Si x1 est incalculable, alors x1 +f x2 l'est aussi, ainsi que y1 et donc y1 +f y2. Donc x1 +f x2 =s y1 +s y2.
- Si x1 est calculable alors y1 l'est aussi. Soit x1c et y1c tq x1 →ct x1c et y1 →ct y1c. On a :
- Si x1c +f x2 est de la forme $F[ if ] +f ax +f bx +f x2 :
Alors d'après le théorème de la décomposition par égalité structurelle, y1c est de la forme $F[ if ] +f ay +f by +f y2 avec ax =s ay, bx =s by. On a les cas suivants :
- si ax est incalculable : alors ay l'est aussi et x1c +f x2 ainsi que y1c +f y2 sont incalculables. Comme x1 +f x2 →c x1c +f x2, x1 +f x2 est incalculable, de même pour y1 +f y2. Donc x1 +f x2 =s y1 +s y2.
- si ax →c $F[ 1b ] : alors, par définition de =s, ay →c $F[ 1b ]. Donc x1c +f x2 →c1 bx et y1c +f y2 →c1 by. On a donc x1 +f x2 →c bx et y1 +f y2 →c by avec bx =s by. Donc x1 +f x2 =s y1 +s y2.
- is ax →c $F[ 0b ] : Par un raisonnement similaire à celui pour le cas "ax →c $F[ 1b ]" on aboutit à la même conclusion.
- si ax possède un calcul terminé axc différent de $F[ 1b ] et $F[ 0b ] : comme ax =s ay, ay est dans le même cas, soit ayc son calcul terminé. Donc x1 +f x2 →ct $F[ if ] +f axc +f bx +f x2 et y1 +f y2 →ct $F[ if ] +f ayc +f by +f y2. D'après le théorème de recomposition par égalité structurelle, on a $F[ if ] +f axc +f bx +f x2 =s $F[ if ] +f ayc +f by +f y2. On a donc x1 +f x2 =s y1 +s y2.
Nous voyons donc que dans tous les cas on a x1 +f x2 =s y1 +s y2.
- Si x1c +f x2 est de la forme $F[ distribute ] +f ax +f bx +f x2 :
Alors d'après le théorème de la décomposition par égalité structurelle, y1c est de la forme $F[ distribute ] +f ay +f by +f y2 avec ax =s ay, bx =s by. On a :
- $F[ distribute ] +f ax +f bx +f x2 →c1 (ax +f x2) +f (bx +f x2)
- $F[ distribute ] +f ay +f by +f y2 →c1 (ay +f y2) +f (by +f y2)
Come x1 +f x2 →c (ax +f x2) +f (bx +f x2), on a O ((ax +f x2) +f (bx +f x2)) ≤ n, de même on a O ((ay +f y2) +f (by +f y2)) ≤ n.
Si le calcul de (ax +f x2) +f (bx +f x2) et (ay +f y2) +f (by +f y2) passe par toutes les valeurs ax,x2,bx,(ax +f x2),(bx +f x2) et pareil en y alors on pourrait appliquer P n deux fois pour arriver à prouver (ax +f x2) +f (bx +f x2) =s (ay +f y2) +f (by +f y2).

On a la disjonction suivante :
- le calcul de (ax +f x2) +f (bx +f x2) ne calcule pas l'argument. Alors on a O(ax +f x2) < n et O(bx +f x2) < n

- Sinon le seul cas restant est quand le calcul de x1c +f x2 est terminé. Si le calcul de y1c +f y2 n'était pas terminé, alors il serait de la forme $F[ if ] +f ay +f by +f y2 ou $F[ distribute ] +f ay +f by +f y2. Par le théorème de la décomposition par égalité structurelle x1c +f x2 serait sous une forme similère et donc les cas sont déjà traité ci-dessus. Remarque : le cas "distribute" n'est pas possible, mais nous n'avons pas besoin de distinguer les cas possibles des autres pour ce raisonnement.
Donc dans tous les cas nous avons x1 +f x2 =s y1 +s y2. Donc P (n+1) est vrai.

Essai 1

Canevas

On définit une relation x =ss y par la conjonction : (plus bas dans la preuve on utiliser une définition un peu modifiée)

  • x ou y est un mot et x = y
  • x et y sont des applications x1 +f x2 et y1 +f y2 avec x1 =s y1 et x2 =s y2

On a xca +f xcb =ss yca +f ycb.
On montre que pour tout x,y tq x =ss y on a :

  • la terminalité du calcul de x et y est la même
  • si x et y ne sont pas des calculs terminaux, alors les 1-calculs sur x et y utilisent la même règle et le résultat de ces calculs vérifient la relation =ss.

Donc soit xca +f xcb et yca +f ycb sont incalculables, soit ils ont pour calcul terminal des formules vérifiant la relation =ss. Et donc on a xca +f xcb =s yca +f ycb.

Preuve

Si x1 ou y1 est incalculables alors, comme x1 =s y1, x1 et y1 sont incalculables. Alors x1 +f x2 et y1 +f y2 sont incalculables, et donc x1 +f x2 =s y1 +s y2. Il nous reste donc à traiter le cas où x1 et y1 sont calculables, ce que nous supposerons par la suite. Soit x1c et y1c les calculs terminés de x1 et y1. On a x1c =s y1c.

Nous allons définir une relation "égalité structurelle simple" qui ressemble à l'égalité structurelle mais où les formules ne sont pas déjà calculées. On l'utilisera pour prouver que la relation est au départ sur x1c +f x2 et y1c +s y2, et perdure après des 1-calculs.
On définit une relation a =ss b par la disjonction :

- a et b sont des mots et a = b
- a et b sont des applications a1 +f a2 et b1 +f b2 avec a1 =ss b1 et a2 =s b2.

D'après le théorème des équivalences entre =s et =ss, de x1 =s y1 et x2 =s y2, on déduit x1c =ss y1c, puis x1c +f x2 =ss y1c +s y2.

Pour n un entier naturel, on définit nCalculate n = 1calculaten (puissance fonctionnelle).

D'après le théorème des calculs et de =ss, on déduit par récurrence que soit :

  • x1c +f x2 et y1c +f y2 sont incalculables, ce qui implique que x1 +f x2 =s x1 +f x2.
  • il existe n tq :
    • les calculs de nCalculate n (x1c +f x2) et nCalculate n (x1c +f x2) soient terminés
    • nCalculate n (x1c +f x2) =ss nCalculate n (x1c +f x2).
D'après le théorème des équivalences entre =s et =ss, on a nCalculate n (x1c +f x2) =s nCalculate n (x1c +f x2), ce qui implique x1c +f x2 =s x1c +f x2 ce qui implique x1 +f x2 =s x1 +f x2. CQFD

Problème

Lors du calcul de x1 +f x2 et y1 +f y2, on tombe sur des sous-expression de x et y qui sont =s. Par exemple pour distribute, on a :
xa =s ya, xb =s yb, xc =s yc et les résultats des 1-calculs de x et y sont (xa +f xc) +f (xb +f xc) et (ya +f yc) +f (yb +f yc).
On a alors besoin, pour ces sous-parties, de la propriété que l'on cherche à démontrer.
Pour résoudre cela, je vois les solutions suivantes:

  • trouver un index pouir une récurrence.
  • calculer au préalable les sous-parties.

Étude de la solution "trouver un index pour une récurrence"
Étude de la solution "calculer au préalable les sous-parties"

L'idée est que chaque sous-formule calculable de x et y soit remplacée par son calcul terminé.

@theorem