Lazi

les essais de preuve de la finitude de la récurrences

Voir essai 15 du théorème de jonction des sous-calculs

Essai 10 pour la finitude de la récursion à un niveau donné (pas fini)

L'idée

Comme "junction" ajoute les calculs élémentaires un par un, on ne peut avoir une récursion infinie que si un ajout entraîne plusieurs ajout après ré-ordonnancement.
Cela peut se produire dans deux cas :

  1. Le calcul fait apparaître un "if x y z" et il fallait inverser avec un calcul sur la condition, qui devient un calcul de niveau inférieur.
  2. Le résultat du calcul (par exemple le calcul de "if 1b x y" où il y a un calcul sur x) entraîne le décalage d'un calcul vers un niveau inférieur.

Essai 9 (pas fini)

L'idée

On reprend l'idée du 8 mais en réduisant les calculs : on raisonne par l'absurde en supposant la récurrence infinie, on montre que l'on peut réduire les calculs aux NSFSP intérieurs à un SFP infini et où la récurrence est aussi infinie. Puis on raisonne sur les nombres de calculs.

On suppose désormais que l'on utilise la version réduite des calculs sous l'hypothèse de la récurrence infinie.

Pour n,m∈ℕ soient :

  • nc n m le nombre de calculs de niveau m de la version ordonnée de c +ll an
  • nd n m le nombre de calculs de niveau m de la version ordonnée de d +ll bn
  • na n le nombre de calculs de niveau n de an
  • nb n le nombre de calculs de niveau n de bn

Par hypothèse de récurrence , si m≤n on a nc n m = nd n m.

Pour n∈ℕ, comme le calcul est réduit à un seul SFP, on a (comme c'est le cas en général pour le niveau 0) soit an=0 soit bn=0.

On peut identifier un calcul élémentaire par sa position de départ, quand un calcul élémentaire est dupliqué ou déplacé, on peut continuer à lui attribuer cet identifiant, on l'appellera "identifiant du calcul élémentaire".

Soit II l'ensemble des identifiants de calculs élémentaires correspondant à un nombre infini d'occurences du calcul élémentaire dans la jonction.

Lors d'une inversion de 2 calculs élémentaires, pour qu'un calcul élémentaire soit placé à un niveau supérieur il faut que le calcul global soit un "distribute a1 a2 a3 ... an". Dans ce cas a3 est dupliqué et seul l'une des duplications de a3 est placé à une niveau supérieur (le deuxième dans "(a1 a3)(a2 a3)".
Pour qu'il y ait une récurrence infinie il faut qu'il y ait une augmentation du nombre de calculs élémentaires dans le SFP de restriction. Pour que l'inversion avec le distribute augmente le nombre de calculs à l'intérieur du SFP de restriction, il faut que les deux a3 se trouvent dans le même argument (le SFP de cet argument est de niveau n+1). Par exemple il faudrait que "(a1 a3)(a2 a3)" soit calculé en "b \ a3 a3".

Regardons l'expression sans notation fonctionnelle de : $F x →b \ x x
$F x → b \ x x = distribute (constF b) ($F x → x x)
$F x → x x = distribute identityF identityF
$F x → b \ x x = distribute (constF b) (distribute identityF identityF)
Donc on prend a1 = constF b et a2 = distribute identityF identityF
Donc (a1 a3)(a2 a3) = (constF b a3)(distribute identityF identityF a3)
Cet exemple illustre que l'on ne peut pas assembler les deux a3 en un même argument car pour cela il faudrait calculer à l'intérieur de l'argument (et donc utiliser des calculs de niveau n+1), alors que l'on fait des calculs de niveau n. Trouver une manière de prouver ça.

L'ajout d'un seul calcul élémentaire ne peut au maximum augmenter que de un niveau un nombre de calculs élémentaire égal au nombre que l'on doit inverser avec lui.

Essai 8 (pas fini)

L'idée

On reprend l'essai 7, qui marche presque mais pas car un calcul de même formule et de même niveau de NFSFP pourrait ne pas changer tandis qu'un autre change, donc on aurait alors une augmentation de la taille de l'ensemble.

L'idée ici est de combiner l'idée du 7 avec l'idée du 3.
Soient pour n∈ℕ :

  • En l'ensemble des NFSFP des calculs élémentaires des versions triés de c +ll an et d +ll bn
  • mn le maximum des nombres d'éléments de En à l'intérieur d'un même NFSFP maximal — dans le sens x>y ss y est le début de la liste x — dans En.

On montre que :

  • mn est borné
  • si la récurrence était infinie alors mn ne serait pas borné

Problème avec m(n)

La propriété semble être juste sauf pour le cas de la normalisation qui ramène un calcul à un niveau plus bas et peut engendre une augmentation du nombre de NFSFP sur cette branche.

Pareil avec "if 1b a2 a3 a4", si il y a un calcul sur a2 et a4 : le calcul sur a2 devient un calcul plus bas et peut se trouver ajouté avec le calcul sur a4.

Essai 7 (faux)

L'idée

Compter le cardinal de l'ensemble En des couples (sous-formule désignée par le NFSFP d'un calcul élémentaire, niveau du NFSFP). L'idée est qu'il peut y avoir une augmentation des calculs élémentaires du fait de l'inversion des calculs sur les formules "distribute", mais les calculs porte sur la même sous-formule du même niveau, donc il n'y a pas augmentation des couples désignés ci-dessus.

Puis il faut prouver que si le nombre de ces couples est borné alors la récurrence est finie :

Si la récurrence était infinie il y aurait un nombre infini de calcul élémentaires d'ajouter et le niveau de ces calculs élémentaires ne serait pas borné. Hors par le raisonnement précédant nous avons montré que le niveau de l'ensemble des calculs élémentaires ajouté est borné puisque l'ensemble des couples est fini.

Essai 6 (pas fini)

L'idée

Compter le cardinal des sous-formules désignées par les NFSFP des calculs élémentaires. L'idée est qu'il peut y avoir une augmentation des calculs élémentaires du fait de l'inversion des calculs sur les formules "distribute", mais les calculs porte sur la même sous-formule, donc il n'y a pas augmentation des sous-formules objets des calculs.
Puis il faut prouver que si le nombre total des sous-formules désignées par les NFSFP des calculs élémentaires est constant alors il y a un nombre fini de calculs élémentaires. Ce n'est pas évident car les calculs bouclant n'utilisent qu'un nombre fini de sous-formules.

Essai 5 (pas fini)

L'idée

Compter le nombre de calculs.

Essai 4 (pas fini)

L'idée

Suivre l'évolution du niveau des calculs non triés.

Essai 3 (pas fini)

L'idée

Comme à chaque n de l'hypothèse de récurrence on ajoute des calculs de niveau n, pour que la récurrence soit infinie il faut que l'on ajoute des calculs de niveau toujours plus grands. Donc le résultat partiel des calculs doit lui-même posséder des niveaux toujours plus grands (et donc tendre vers une formule infinie).
Pour chaque étape n il existe un nombre fini de NFSFP sur la formule résultant du calcul, comme la récurrence est infinie, il existe donc un NFSFP de niveau n sur la formule qui contient (au sens "intérieur") une infinité de calculs produits par la récurrence infinie. Donc il existe (au moins dans l'un des deux calculs) une suite infinie de NFSFP, chacun étant le début de l'autre, correspondant au calculs.
Cette suite infinie ne peut être que dans un des calculs car on ajoute des calculs élémentaires pour qu'ils correspondent à l'autre calcul, donc si l'un est fini pour un certtain début de chemin, l'autre doit l'être aussi.
Nous avons donc une suite infinie de NFSFP où le suivant est intérieur au précédant, suite se trouvant dans les deux calculs.

Essai 2 (pas fini)

Pour cela nous allons raisonner sur le niveau max des NFSFP.

Pour n∈ℕ, soient :

  • an et bn les calculs ajoutés à c et d, tq définis dans l'hypothèse H n.
  • mc et md les niveaux maximum des calculs élémentaires c et d
  • mcan et mdbn les niveaux maximum des calculs élémentaires de la version triée de c +ll an et c +ll bn.
  • Mn = max ( mcan, mdbn )

En examinant les différents cas d'inversion listés dans la démonstration du théorème du calcul trié on peut constater que pour qu'il y ait une augmentation du niveau du calcul résultant, il faut inverser le calcul d'un "distribute a1 a2 a3" avec un calcul précédant concernant a3 (entier ou à l'intérieur). Donc une inversion de 2 calculs élémentaires ne peut augmenter le niveau que le calcul élémentaire précédant est de niveau supérieur à celui introduit.

Donc pour que Mn+1>Mn il faut que

Sachant qu'une inversion de deux calculs élémentaires ne peut faire augmenter le niveau du calcul que de 1 au maximum et que an et bn sont composés de calculs élémentaires de niveau n, nous avons (length est la fonction "longueur de liste") :

  • mcan ≤ max ( mc + length an , n )
  • mdan ≤ max ( md + length dn , n )

Essai 1 (faux)

On a donc pour tout n, H n. Comme le niveau des NFSFP de x est borné, on déduit qu'il existe c1 et d1 tq calculate loose (c +ll c1) x = calculate loose (d +ll d1) x.