Lazi

Recherche d'une preuve

Récurrence

Si on fait une récurrence sur la profondeur des formules, comme on calcul des sous-formules calculables, il faut le faire sur la profondeur max de toutes les sous-formules calculables calculées.

Égalité après remplacement

Il faut aussi calculer les parties calculables. Donc la transformation T x d'une formule x est la suivante:

  • Si x est incalculable, T x = la variable de nom v
  • Si x est calculable, soit xc son calcul.
    • Si xc n'est pas une application on retourne xc.
    • Si xc est une application xc1 +f xc2, on retourne T xc1 +f T xc2

T et récurrence infinie

Remarquons que T peut boucler indéfiniment: pour f tel que f = if f, T f entre dans une récursivité infinie.
Dans ce cas, T ne retourne pas une formule (ou retourne une formule infinie).
On peut avoir x =c y (par exemple si x = y) avec T x qui n'est pas une formule.

Étendre l'égalité des formules aux formules infinies

L'idée

On garde la définition de T, beaucoup (mais pas toutes) de fonction sur les formules fonctionnent sur les formules infinies. Par exemple la comparaison de formule peut retourner 0b (mais pas 1b). Remarquons que dans l'énoncé du théorème, on utilise l'égalité et non la comparaison de formules, donc même avec des formules infinies ça peut marcher. On n'a pas besoin de calculer littéralement une valeur par T pour prouver une égalité (par exemple T x = T x).

Et le critère de récurrence ?

Nous avons vu que le critère de récurrence doit porter sur la profondeur max des calculs des sous-formules. Mais avec certaines formules (comme "if f") il y a un nombre infini de sous-formules. Comment alors utiliser la récurrence ?
La profondeur de la formule est infinie après application de T, mais est-ce que la profondeur des sous-formules calculées récursivement est infini ? Pas dans l'exemple du "if f". Mais on peut trouver un exemple où la profondeur de la sous-formule calculée augmente.
Profondeur des sous-formules augmentant: Soit h tel que h = $Def x → if \ h \ if 1b x 0b.
Calculons h 1b = if \ h \ if 1b 1b 0b
Puis on calcule la sous-formule h \ if 1b 1b 0b = if \ h \ if 1b (if 1b 1b 0b) 0b
Donc on voit que la sous-formule grossit à chaque itération du calcul, que ce soit lors du calcul par T ou pour =c.

On peut utiliser une récurrence sur une paire d'entiers ( le niveau d'imbrication de la sous-formule calculée, la profondeur de la sous-formule calculée).

T avec une paire de formules en argument ? (semble pas bien)

Pour éviter le problème, on peut peut-être plus calquer le calcul de T sur =c : il prendrait en argument les deux formules à comparer.

Est-ce que c'est utilisable pour le théorème ?

J'ai l'impression que cela complique son utilisation.

La nouvelle définition

T x y est égal à :

  • Si x ou y est incalculable: $T