Théorème de l'indexation des couples égaux par calcul
Contexte
Pour faire des démonstration par récurrence sur les couples (x,y) tq x =c y, il nous faut trouver une injection de ces couples sur ℕ qui se calque sur la récurrence de la définition de =c.
Énoncé
Il existe une fonction I de l'ensemble des couples égaux par calcul vers ℕ tq si I x y = n alors on a la disjonction :
- x = y et n = 0
- il existe xc1 tq x →c1 xc1 et xc1 =c y et I xc1 y = n-1
- il existe yc1 tq y →c1 yc1 et x =c yc1 et I x yc1 = n-1
- x et y sont des applications x1 +f x2 et y1 +f y2 avec x1 =c y1, x2 =c y2, I x1 y1 < n et I x2 y2 < n
Preuve
Soit I la fonction partant de l'ensemble des couples égaux par calcul vers ℕ : pour (x,y) un tel couple on définit I x y par :
- soit i0 défini par :
- sinon i0 = ∞
- sinon i1 = ∞
- sinon i2 = ∞
- sinon i3 = ∞
I étant défini par récurrence, il faut nous assurer que la définition est valide (qu'elle ne boucle pas). Comme elle est calquée sur la définition de =c, la finitude de la récursion de la propriété =c implique la finitude de la récursion de I.
Montrons les propriétés de I annoncés dans l'énoncé :
- si c'est i0 : on a x = y et n = 0
- si c'est i1 : il existe xc1 tq x →c1 xc1 et xc1 =c y et I x y = (I xc1 y) + 1, donc I xc1 y = n-1
- si c'est i2 : similaire à i1
- si c'est i3 : x et y sont des applications x1 +f x2 et y1 +f y2 avec x1 =c y1 et x2 =c y2 et on a n = I x y = 1 + max (I x1 y1) (I x2 y2), donc I x1 y1 < n et I x2 y2 < n
CQFD
Recherche d'une preuve
Essai 1
Si on utilise la définition suivante :
- si x = y : I x y = 0
- si il existe xc1 tq x →c1 xc1 et xc1 =c y : I x y = (I xc1 y) + 1
- si il existe yc1 tq y →c1 yc1 et x =c yc1 : I x y = (I x yc1) + 1
- si x et y sont des applications x1 +f x2 et y1 +f y2 et que l'on a x1 =c y1 et x2 =c y2 : I x y = 1 + max (I x1 y1) (I x2 y2)
Le problème est que l'on peut avoir x =c y et I x y = infini, car y peut être incalculable et si on applique la dernière règle on peut boucler.
D'autre part les différents cas ne sont pas exclusifs, donc soit on indique qu'il faut les prendre dans l'ordre (par des "sinon..."), soit on les rend exclusifs. Les rendre exclusifs me parait difficile.
On peut peut-être définir I de sorte qu'il prenne les valeurs minimales des différentes voies possibles.
Nouvelle définition :
- soit i0 défini par :
- sinon i0 = ∞
- sinon i1 = ∞
- sinon i2 = ∞
- sinon i3 = ∞
@theorem