Lazi

Recherche d'une preuve

Détermination de la relation =c

Il faut que ce soit une relation d'équivalence.

Essai 5

Contexte

La définition provenant de l'essai 4 parait prometeuse mais il y a un blocage pour prouver la transitivité.
Il est peut-être possible d'adapter la règle pour ralentir les étapes de calculs et permettre de prouver la transitivité.

Nouvelle définition de =c

Pour x et y deux formules, et x =c y ssi on a la disjonction:

  1. x = y
  2. si il existe xc1 tq x →c1 xc1 et xc1 =c y
  3. si il existe yc1 tq y →c1 yc1 et x =c yc1
  4. 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

Remarque : "=" est en fait l'égalité sur les formules, qui dépend du type des formules considérées.

Essai 4

Contexte

Voir l'essai 3, l'étude des contraintes sur =c a fournit une nouvelle définition à étudier.

Nouvelle définition de =c

Pour x et y deux formules, et x =c y ssi on a la disjonction:

  1. x = y
  2. si il existe xc1 tq x →c1 xc1 et xc1 =c y
  3. si il existe yc1 tq y →c1 yc1 et x =c yc1
  4. 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

Remarque : "=" est en fait l'égalité sur les formules, qui dépend du type des formules considérées.

Essai de démonstration avec cette définition

Utiliser la récurrence

Pour x et y deux formules tq x =c y, on définit le niveau de calcul de =c pour (x, y) par:

  1. si x = y: 0
  2. si il existe xc1 tq x →c1 xc1 et xc1 =c y : le niveau de (xc1,y) + 1
  3. si il existe yc1 tq y →c1 yc1 et x =c yc1 : le niveau de (x,yc1) + 1
  4. si x et y sont des applications x1 +f x2 et y1 +f y2 avec x1 =c y1 et x2 =c y2 : 1 + le maximum des niveau de (x1,y1) et (x2,y2)

Le niveau de calcul est un nombre car x =c y implique que le calcul de x =c y est fini.

Réflexivité

=c est réflexive grâce à la première condition.

Symétrie

On prouve la propriété par récurrence sur le niveau de calcul :
Niveau 0 : évident.

Si la propriété est prouvée pour le niveau n:
Soit x,y tq x =c y où le niveau de calcul de (x,y) est n+1:

  1. si il existe xc1 tq x →c1 xc1 et xc1 =c y : comme (xc1,y) est de niveau n, on a y =c xc1, et donc on a y =c x.
  2. si il existe yc1 tq y →c1 yc1 et x =c yc1 : similaire à au dessus.
  3. si x et y sont des applications x1 +f x2 et y1 +f y2 avec x1 =c y1 et x2 =c y2 : on a y1 =c x1 et y2 =c x2, donc y =c x.

Transitivité

On prouve la propriété par récurrence sur le couple (n,m) des niveaux de calcul de (x,y) et (y,z) :

Soit x,y,z tq x =c y et y =c z où les niveaux de calcul de (x,y) et (y,z) sont ≤1 :

  • Si x = y ou y = z : on a en fait que deux formules, donc x =c z.
  • cas 2 et 2 : on a xc1 =c y et yc1 =c z . Comme le niveau de (x,y) et (y,z) est 1, on a xc1 = y et yc1 = z. Donc x →c1 y et y →c1 z. On voit que x =c z par un calcul de niveau 2 utilisant la condition 2 pour les 2 calculs.
  • cas 2 et 3 : on a xc1 =c y et y =c zc1 . Comme le niveau de (x,y) et (y,z) est 1, on a xc1 = y et y = zc1. Donc x →c1 y et z →c1 y. Comme x =c y et z →c1 y, par la condition 3 on a x =c z.
  • cas 2 et 4 : on a xc1 =c y et y et z sont des applications y1 +f y2 et z1 +f z2 avec y1 =c z1 et y2 =c z2. Comme le niveau de (x,y) et (y,z) est 1, on a xc1 = y , y1 = z1 et y2 = z2. Donc y = z, donc xc1 = z. Par la condition 2 on a x =c z.
  • cas 3 et n : similaire à 2 et n.
  • cas 4 et n où n vaut 2 ou 3 : similaire au cas 2 et 4.
  • cas 4 et 4 : Comme le niveau de (x,y) et (y,z) est 1, on a x1 = y1, x2 = y2, y1 = z1 et y2 = z2. Donc on a x = y = z, donc on a x = z, donc on a x =c z.

Si la propriété est prouvée pour les niveaux (n,m) avec n≥1 et m≥1:

Soit x,y,z tq x =c y et y =c z où le niveau de calcul de (x,y) est ≤ n+1 et le niveau de calcul de (y,z) est ≤ m+1 :

  • Cas 1 et m ou m et 1 : on a en fait que deux formules, donc x =c z.
  • Cas 2 et 2 : on a xc1 =c y et yc1 =c z : on a aussi x =c xc1 et y =c yc1. Le niveau de calcul de (xc1,y) et (yc1,z) est ≤ n. Celui de (x,xc1) et (y,yc1) est 1. Donc on peut utiliser l'hypothèse de récurrence pour les égalités x =c xc1, xc1 =c y, y =c yc1, yc1 =c z. Donc x =c z.
  • Cas 2 et 3: on a xc1 =c y et y =c zc1 . Similaire au cas 2 et 3.
  • Cas 2 et 4: on a xc1 =c y et y et z sont des applications y1 +f y2 et z1 +f z2 avec y1 =c z1 et y2 =c z2. Étude démonstration cas 2 et 4.

Essai 3

Contexte

Dans l'essai 2 il semble y avoir un problème pour faire des preuves par récurrence.

Peut-être qu'en définissant un algorithme de teste d'égalité par calcul viable, puis en transcrivant en relation, cela serait plus simple.

Algorithme de comparaison par calcul

Soit x et y deux formules à comparer par calcul.

  • Si x et y sont incalculable alors elles sont égales par calcul.
  • Sinon, on calcul x et y et on compare leur nombres d'arguments :
    • cas d'inégalité : on retourne 0b
    • cas d'égalité :
      • on compare leur fonction minimale (qui est un mot) :
        • cas d'inégalité : on retourne 0b
        • cas d'égalité :
          • chaque argument doit être égal par calcul

L'algorithme se termine-t-il toujours ?

Si on a deux arguments:

  • a 1b
  • a (if 1b 1b 1b)
tels que ∀ x; a x = 0b \ a x
alors pour les comparer, on les calcul, ce qui donne:
  • 0b \ a 1b
  • 0b \ a (if 1b 1b 1b)
ce qui amène au calcul des 2 arguments a 1b et a (if 1b 1b 1b)

Cet exemple nous montre un cas où l'algorithme boucle. De plus ce serait aussi le cas si l'algorithme comportait une comparaison de formules avant calcul car les formules "a 1b" et "a (if 1b 1b 1b) " sont différentes.

Si l'algorithme boucle, cela implique que l'on ne peut pas indéxer une récurrence dans une preuve sur la longueur de l'algorithme. Cela limite énormément les preuves possibles.

Comment gérer les imbrications infinies d'arguments ?

Le cas à éliminer est quand le calcul d'un argument mène à une formule qui a un argument qui, quand on le calcul mène à un argument et ce indéfiniment. La position de l'argument peut changer.

Est-ce que cet argument est équivalent à une formule incalculable ?

L'argument contient en lui un argument de calcul infini, mais à une certaine profondeur l'argument pourrait être ignoré et donc la formule englobante pourrait être calculée en un mot. Par contre si la chaîne infinie d'arguments n'est jamais ignorée alors la formule globale est équivalente à une formule incalculable.
Remarquons que l'on ne peut pas savoir dans quel cas on se trouve puisque cela peut dépendre d'arguments supplémentaires qui seraient ajoutés à la formule globale.

Une solution serait de ne rien faire de spécial, mais cela interdit les raisonnements par récurrence sur =c car on ne peut pas mesurer la profondeur d'une formule au regard d'=c car certaines ont une profondeur infinie.

Essai de démonstration avec cette définition

Réflexivité

=c est réflexive car R l'est.

Symétrie

Soit x,y tq x =c y.

  • Si R x y, alors R y x et donc y =c x.
  • Si il existe x1,x2,y1,y2 tels que :
    • R x (x1 +f x2)
    • R y (y1 +f y2)
    • x1 =c y1
    • x2 =c y2

On voit que l'on a besoin d'une récurrence pour prouver y1 =c x1 et y2 =c x2.

Étude des contraintes sur =c

Voir la sous-page.

Essai 2

Contexte

Dans l'essai 1 la relation n'est pas assez large et il manque des relations pour la transitivité.

Définition

Soit =c la relation définie sur les formules : x =c y ssi on a la disjonction :

  • R x y
  • il existe x1,x2,y1,y2 tels que:
    • R x (x1 +f x2)
    • R y (y1 +f y2)
    • x1 =c y1
    • x2 =c y2

Problème de récurrence infinie

Avec cette définition, si on veut faire des preuves par récurrence, on peut avoir une récurrence infinie pour la partie argument sans pour autant qu'il soit incalculable, par exemple si l'argument a vérifie a →c 1b +f a.

Essai 1 (rejeté)

Définition

Soit =c la relation définie sur les formules : x =c y ssi on a la disjonction :

  • R x y
  • x, y sont des applications x1 +f x2, y1 +f y2 et x1 =c y1 et x2 =c y2

Contre exemple

Montrons que =c n'est pas transitive. On prend les valeurs:
x = ($F x → x x) 1b
y = 1b 1b
z = 1b \ if 0b 0b 1b

Ce qui donne:
xc = 1b 1b
yc = 1b 1b
zc = 1b \ if 0b 0b 1b

On voit que l'on a R x y et y =c z, mais on n'a pas x =c z.