Lazi

Théorème de jonction des sous-calculs

Contexte

Énoncé

Variables

x,y,z

Conditions

  • x,y et z sont des formules
  • x →c[loose]= y
  • x →c[loose]= z

Conclusion

Il existe t tq :

  • y →c[loose]= t
  • z →c[loose]= t

Preuve

Définitions

Définition de la fonction balancing :

Domaine de balancing :
  • x est une formule
  • c et d sont des calculs loose valides sur x

Nous définissons balancing x c d par récurrence :
- Si orderedCalc c = orderedCalc d :
balancing x c d = c
- Sinon :
Soient co = orderedCalc c et do = orderedCalc d.
Soit s un NFSFP de co ou do minimal suivant l'ordre par niveau tel que le nombre de calcul élémentaires représentés par s est différent entre co et do.
S'il y a moins de calculs élémentaires s dans co on définit balancing x c d = balancing x c (d +le s)
Sinon on définit balancing x c d = balancing x (c +le s) d

Définition de cb n et db n :

Soient cb n et db n les calculs engendrés par balancing pour l'occurence n de sa récursion.

Définition de cbt n et dbt n :

Soient cbt n et dbt n les arbres de la version ordonnée de respectivement cb n et db n.

Définition de "sous-liste d'un arbre" :

Remarque : cette définition est locale à cette preuve.
Soit t un arbre, on dit que l est une sous-liste de t ssi :
  • l est une liste
  • Le premier élément de l est le contenu du nœud racine de t
  • Si la racine de t a au moins un enfant : la liste privée du premier élément est une sous-liste d'un des arbres enfants de la racine.
  • Si la racine de t n'a pas d'enfant alors l contient un seul élément.

Preuve de la finitude de la récurrence de balancing

Niveau des calculs élémentaires et profondeur de l'arbre :

Un calcul élémentaire de NFSFP s sera placé dans l'arbre du calcul en fonction de sa liste binaire, donc la profondeur du nœud correspondant a pour valeur la longeur de la liste s. Donc la profondeur du nœud est supérieure ou égale au niveau argumental du NFSFP.

Niveau des calculs équilibré et partie communes des arbres :

Comme balancing équilibre les calculs par niveau, quand le niveau des NFSFP équilibrés augmentent les arbres cbt n et dbt n ont ont une base commune plus grandes.

Implication d'un balancing à la récursivité infinie :

Si balancing boucle indéfiniment alors cela implique que balancing ajoute de plus en plus de calculs, donc au moins un des arbres cbt n ou dbt n contient de plus en plus de calculs (en fait les deux car balancing équilibre). Supposons que cbt n contienne de plus en plus de calculs. Comme le nombre d'enfants de chaque nœud est fini, cela implique que l'on ait la disjonction :
- un des nœuds contient de plus en plus d'éléments
- l'arbre grandit indéfiniment

Comme ces arbres sont binaires, l'hypothèse "l'arbre grandit indéfiniment" implique qu'une sous-liste de l'arbre devient infini.

Donc l'hypothèse "balancing boucle indéfiniment" implique la disjonction :
- un des nœuds contient de plus en plus d'éléments.
- une sous-liste de l'arbre devient infini et contient un nombre croissant de calculs.

Le nombre de calculs élémentaires à équilibrer :

Comme l'équilibre se fait sur les versions triées des calculs (les co et do de la définition), le nombre de calculs élémentaires qu'il reste à équilibrer doit être compté sur les calculs triés. Il nous faut donc examiner la conséquence de l'ajout sur le calcul non trié c ou d d'un calcul élémentaire, une fois le calcul augmenté trié. En reprenant la démonstration du théorème du calcul trié, on voit que seul l'inversion avec un distribute engendre des calculs supplémentaires. Nous voyons donc que globalement la conséquence de l'ajout d'un calcul élémentaire par balancing peut être une augmentation.

Augmentation par distribute séparé ou non :

Rappelons que distribute a1 a2 a3 →c[univocal]1 (a1 a3)(a2 a3). Les calculs dupliqués sont ceux sur a3. Si les calculs suivants ne portent que sur la partie fonction ou argument de (a1 a3)(a2 a3) alors les calculs des deux a3 ne sont ni sur le même nœud ni sur une même sous-liste de l'arbre des calculs, et dans ce cas il ne peuvent contribuer ce que balancing boucle indéfiniment puisqu'il n'y a pas augmentation du nombre de calculs à équilibrer. Donc pour que des duplications de calculs entraînent une augmentation des calculs sur une sous-liste de l'arbre des calculs, il faut qu'il y ait par la suite des ajouts de calculs qui déplacent les calculs dupliqués vers la même sous-liste de l'arbre des calculs.

SFP de calculs s-loose disjoints et position dans l'arbre des calculs :

Une sous-liste d'arbre de calculs correspond à une liste de SFP imbriqués (le suivant est intérieur au précédant). Donc pour que deux calculs élémentaires s-loose soient dans la même sous-liste il est nécessaire que leurs deux SFP soient imbriqués.

Les calculs élémentaires disjoints le reste après le trie suivant l'ajout d'un calcul élémentaire

Les calculs sont éventuellement déplacés par les ajouts de calculs élémentaires ajoutés par balancing (lors du trie). Ces déplacements suivent les déplacements des sous-formules provoqués par le calcul élémentaire ajouté. Comme deux sous-formules de SFP disjoints restent disjoints, il en est alors de même pour les calculs élémentaires disjoins.
Remarquons que ce ne serait pas le cas en loose, par exemple pour
distribute if a2 a3 a4 →c[univocal]1 if a3 (a2 a3) a4
où un calcul sur a3, devenant condition du if, sera normalisé en calcul sur le if, et donc les SFP des calculs sur a3 deviennent imbriqués.

Nous venons de prouver qu'une sous-liste de l'arbre des calculs ne peut pas avoir d'augmentation du nombre de calcul élémentaire qu'elle contient lors de l'ajout de nouveau calculs par balancing. Donc une sous-liste ne peut contenir un nombre infini de calculs élémentaires. Donc balancing ne peut avoir une récurrence infinie.

Preuve de la convergence des cb n et db n

Pour deux calculs loose a,b sur une formule x, nous définissons la distance dist a b par :

- si les versions triées de a et b sont égales, alors dist a b = 0
- sinon soit n le niveau le plus petit où les versions triés de a et b diffèrent , alors dist a b = 1 / (1 + n)
Cette distance a valeur dans le segment [0,1], plus exactement dans {0} ∪ 1/ℕ*.

Nous allons montrer que la suite dist (cb n) (db n) converge vers 0.

Comme balancing a une récurrence finie, et qu'elle ajoute les calculs élémentaires par niveau, il existe un n0 minimal tq les versions triées de cb n0 et db n0 aient le même nombre de calculs élémentaires de niveau 0. Soit x0 le résultat de l'application de ces calculs sur x. Pour n ≥ n0 les autres calculs des versions triées de cb n et db n, ainsi que les calculs élémentaires ajoutés par balancing sont de niveau > 0, donc leurs NFSFP sont intérieurs aux NFSFP des arguments de x0. Donc si on relativise les calculs à ces arguments on voit que balancing les équilibrent de la même manière qu'au niveau 0. Donc par récurrence, puisque balancing produits des calculs dont les versions triées sont identique au niveau 0, il produit aussi des calculs dont les versions triées sont identique à tous les niveaux.
Nous voyons donc que la suite dist (cb n) (db n) converge vers 0.

Preuve de l'existance du t de la conclusion

Puisque balancing a une récurrence finie et que dist (cb n) (db n) converge vers 0, soit t le calcul qui est la limite (atteinte) des suites cb n et db n. On a alors

  • y →c[loose]= t
  • z →c[loose]= t
CQFD

Recherche d'une preuve

Essai 18

Contexte

On reprend les idées du 17 mais en se basant sur l'arbre de calcul.

Définitions

Définition de la fonction balancing :

Domaine de balancing :
  • x est une formule
  • c et d sont des calculs loose valides sur x

Nous définissons balancing x c d par récurrence :
- Si orderedCalc c = orderedCalc d :
balancing x c d = c
- Sinon :
Soient co = orderedCalc c et do = orderedCalc d.
Soit s un NFSFP de co ou do minimal suivant l'ordre par niveau tel que le nombre de calcul élémentaires représentés par s est différent entre co et do.
S'il y a moins de calculs élémentaires s dans co on définit balancing x c d = balancing x c (d +le s)
Sinon on définit balancing x c d = balancing x (c +le s) d

Définition de cb n et db n :

Soient cb n et db n les calculs engendrés par balancing pour l'occurence n de sa récursion.

Définition de cbt n et dbt n :

Soient cbt n et dbt n les arbres de la version ordonnée de respectivement cb n et db n.

Définition de "sous-liste d'un arbre" :

Remarque : cette définition est locale à cette preuve.
Soit t un arbre, on dit que l est une sous-liste de t ssi :
  • l est une liste
  • Le premier élément de l est le contenu du nœud racine de t
  • Si la racine de t a au moins un enfant : la liste privée du premier élément est une sous-liste d'un des arbres enfants de la racine.
  • Si la racine de t n'a pas d'enfant alors l contient un seul élément.

Preuve

Preuve de la finitude de la récurrence de balancing

Niveau des calculs élémentaires et profondeur de l'arbre :

Un calcul élémentaire de NFSFP s sera placé dans l'arbre du calcul en fonction de sa liste binaire, donc la profondeur du nœud correspondant a pour valeur la longeur de la liste s. Donc la profondeur du nœud est supérieure ou égale au niveau argumental du NFSFP.

Niveau des calculs équilibré et partie communes des arbres :

Comme balancing équilibre les calculs par niveau, quand le niveau des NFSFP équilibrés augmentent les arbres cbt n et dbt n ont ont une base commune plus grandes.

Implication d'un balancing à la récursivité infinie :

Si balancing boucle indéfiniment alors cela implique que balancing ajoute de plus en plus de calculs, donc au moins un des arbres cbt n ou dbt n contient de plus en plus de calculs (en fait les deux car balancing équilibre). Supposons que cbt n contienne de plus en plus de calculs. Comme le nombre d'enfants de chaque nœud est fini, cela implique que l'on ait la disjonction :
- un des nœuds contient de plus en plus d'éléments
- l'arbre grandit indéfiniment

Comme ces arbres sont binaires, l'hypothèse "l'arbre grandit indéfiniment" implique qu'une sous-liste de l'arbre devient infini.

Donc l'hypothèse "balancing boucle indéfiniment" implique la disjonction :
- un des nœuds contient de plus en plus d'éléments.
- une sous-liste de l'arbre devient infini et contient un nombre croissant de calculs.

Le nombre de calculs élémentaires à équilibrer :

Comme l'équilibre se fait sur les versions triées des calculs (les co et do de la définition), le nombre de calculs élémentaires qu'il reste à équilibrer doit être compté sur les calculs triés. Il nous faut donc examiner la conséquence de l'ajout sur le calcul non trié c ou d d'un calcul élémentaire, une fois le calcul augmenté trié. En reprenant la démonstration du théorème du calcul trié, on voit que seul l'inversion avec un distribute engendre des calculs supplémentaires. Nous voyons donc que globalement la conséquence de l'ajout d'un calcul élémentaire par balancing peut être une augmentation.

Augmentation par distribute séparé ou non :

Rappelons que distribute a1 a2 a3 →c[univocal]1 (a1 a3)(a2 a3). Les calculs dupliqués sont ceux sur a3. Si les calculs suivants ne portent que sur la partie fonction ou argument de (a1 a3)(a2 a3) alors les calculs des deux a3 ne sont ni sur le même nœud ni sur une même sous-liste de l'arbre des calculs, et dans ce cas il ne peuvent contribuer ce que balancing boucle indéfiniment puisqu'il n'y a pas augmentation du nombre de calculs à équilibrer. Donc pour que des duplications de calculs entraînent une augmentation des calculs sur une sous-liste de l'arbre des calculs, il faut qu'il y ait par la suite des ajouts de calculs qui déplacent les calculs dupliqués vers la même sous-liste de l'arbre des calculs.

SFP de calculs s-loose disjoints et position dans l'arbre des calculs :

Une sous-liste d'arbre de calculs correspond à une liste de SFP imbriqués (le suivant est intérieur au précédant). Donc pour que deux calculs élémentaires s-loose soient dans la même sous-liste il est nécessaire que leurs deux SFP soient imbriqués.

Les calculs élémentaires disjoints le reste après le trie suivant l'ajout d'un calcul élémentaire

Les calculs sont éventuellement déplacés par les ajouts de calculs élémentaires ajoutés par balancing (lors du trie). Ces déplacements suivent les déplacements des sous-formules provoqués par le calcul élémentaire ajouté. Comme deux sous-formules de SFP disjoints restent disjoints, il en est alors de même pour les calculs élémentaires disjoins.
Remarquons que ce ne serait pas le cas en loose, par exemple pour
distribute if a2 a3 a4 →c[univocal]1 if a3 (a2 a3) a4
où un calcul sur a3, devenant condition du if, sera normalisé en calcul sur le if, et donc les SFP des calculs sur a3 deviennent imbriqués.

Nous venons de prouver qu'une sous-liste de l'arbre des calculs ne peut pas avoir d'augmentation du nombre de calcul élémentaire qu'elle contient lors de l'ajout de nouveau calculs par balancing. Donc une sous-liste ne peut contenir un nombre infini de calculs élémentaires. Donc balancing ne peut avoir une récurrence infinie.

Preuve de la convergence des cb n et db n

Pour deux calculs loose a,b sur une formule x, nous définissons la distance dist a b par :

- si les versions triées de a et b sont égales, alors dist a b = 0
- sinon soit n le niveau le plus petit où les versions triés de a et b diffèrent , alors dist a b = 1 / (1 + n)
Cette distance a valeur dans le segment [0,1], plus exactement dans {0} ∪ 1/ℕ*.

Nous allons montrer que la suite dist (cb n) (db n) converge vers 0.

Comme balancing a une récurrence finie, et qu'elle ajoute les calculs élémentaires par niveau, il existe un n0 minimal tq les versions triées de cb n0 et db n0 aient le même nombre de calculs élémentaires de niveau 0. Soit x0 le résultat de l'application de ces calculs sur x. Pour n ≥ n0 les autres calculs des versions triées de cb n et db n, ainsi que les calculs élémentaires ajoutés par balancing sont de niveau > 0, donc leurs NFSFP sont intérieurs aux NFSFP des arguments de x0. Donc si on relativise les calculs à ces arguments on voit que balancing les équilibrent de la même manière qu'au niveau 0. Donc par récurrence, puisque balancing produits des calculs dont les versions triées sont identique au niveau 0, il produit aussi des calculs dont les versions triées sont identique à tous les niveaux.
Nous voyons donc que la suite dist (cb n) (db n) converge vers 0.

Essai 17

Contexte

Dans le 16 il y a diverses recherches pour démontrer que jonction ne boucle pas indéfiniment. On reprend ici le 16 car il me semble que les idées pour réaliser la démonstration sont trouvées.

Essai de preuve

Définition de la fonction "balancing"

Domaine de balancing :

  • x est une formule
  • c et d sont des calculs loose valides sur x

Nous définissons balancing x c d par récurrence :
- Si orderedCalc c = orderedCalc d :

balancing x c d = c
- Sinon :
Soient ct = orderedCalc c et dt = orderedCalc d.
Soit s un NFSFP de ct ou dt minimal suivant l'ordre par niveau tel que le nombre de calcul élémentaires représenté par s est différent entre ct et dt.
S'il y a moins de calculs élémentaires s dans ct on définit balancing x c d = balancing x c (d +le s)
Sinon on définit balancing x c d = balancing x (c +le s) d

Preuve de la finitude de la récursivité de "balancing"

Définition de cb n et db n :

Soient cb n et db n les calculs engendrés par balancing pour l'occurence n de sa récursion.

Propriétés de la fonction "balancing"

Croissance des niveaux :

Le niveau des calculs élémentaires ajoutés par balancing est croissant car l'ajout d'un calcul élémentaire de niveau n à c ou d n'a pas d'influence sur les calculs élémentaires de niveau < n dans ct ou dt.

Nous venons de voir que balancing équilibre les calculs par niveau, en réalisant l'équilibre sur le niveau 0 puis en augmentant. Nous allons voir avec la propriété suivante que si deux NFSFP de sont disjoints alors l'équilibrage est indépendant.

Indépendance des calculs ajoutés par balancing sur des NFSFP disjoints :

Soit c et d deux calculs valides sur une formule x tq c et d sont identiques entre les niveau 0 et n-1. Remarquons que les verstions triées de c et d restent identiques entre les niveau 0 et n-1. Soit y le résultat du calcul de x par la partie commune de c et d entre les niveau 0 et n-1. Soient s et t deux NFSFP de niveau n, disjoints sur y. Comme les calculs ajoutés par balancing sont de niveau ≥ n tous les calculs ne changent pas la place de s et t. Donc les calculs en s et t sont indépendants.

Stabilité des NFSFP valides sur les résultats intermédiaires :

Soient cb n et db n les calculs engendrés par balancing pour l'occurence n de sa récursion. Comme le niveau des calculs élémentaires ajoutés par balancing est croissant, si pour n fixé, p est le niveau du calcul élémentaire ajouté, alors l'ensemble des NFSFP de niveau ≤ p valides sur les résultats du calcul de x par cb(n) est identique à celui pour db(n) et est constant pour les niveaux d'occurence de balancing supérieurs.

Preuve de la finitude de la récursivité de "balancing"

Présentation de la démonstration :

Nous allons trouver une valeur entière décroissant strictement et qui arrivée à zéro implique la fin de la récursion. Cette valeur sera le nombre de calculs restant à équilibrer pour un chemin de NFSFP imbriqués donné. Un chemin de NFSFP imbriqués est une liste de NFSFP où le suivent est intérieur au précédant et où les NFSFP sont pris dans les NFSFP stables (voir dernière propriété de la section ci-dessus). Comme à un niveau donné il n'existe qu'un nombre fini de NFSFP stables, si la récurrence de balancing était infinie il existerait un chemin (fini ou non) de NFSFP imbriqués tel que pour tout p∈ℕ il existe une occurence n de balancing ajoutant plus de p calculs élémentaires dans ce chemin. Donc la décroissance stricte du nombre de calcul à équilibrer par chemin de NFSFP imbriqués implique l'arrêt de la récurrence de balancing.

Définition de cb n et db n :

Soient cb n et db n les calculs engendrés par balancing pour l'occurence n de sa récursion.

Le nombre de calculs élémentaires à équilibrer :

Comme l'équilibre se fait sur les versions triés des calculs (les ct et dt de la définition), le nombre de calculs élémentaires qu'il reste à équilibrer doit être compté sur les calculs triés. Il nous faut donc examiner la conséquence de l'ajout sur le calcul non trié c ou d d'un calcul élémentaire, une fois le calcul augmenté trié. En reprenant la démonstration du théorème du calcul trié, on voit que seul l'inversion avec un distribute engendre des calculs supplémentaires. Nous voyons donc que globalement la conséquence de l'ajout d'un calcul élémentaire par balancing peut être une augmentation.

Augmentation par distribute séparé ou non :

Rappelons que distribute a1 a2 a3 →c[univocal]1 (a1 a3)(a2 a3). Les calculs dupliqués sont ceux sur a3. Soit ces calculs sont équilibrés dans des NFSFP séparés, soit dans un NFSFP commun. S'il sont équilibrés dans des NFSFP séparés alors ils ne contribuent pas à augmenter le nombres de calculs élémentaires à équilibrer dans un chemin de NFSFP imbriqus. Ils nous reste à voir le cas où les calculs sur les deux a3 sont à équilibrer dans le même NFSFP.

Augmentation par distribute non-séparé :

Donnons un exemple où ce cas se produit : Si un calcul est ajouté à c, qui ajoute le calcul de distribute a1 a2 a3, alors les calculs sur a3 sont dupliqués. Pour que ces calculs soient dans le même NFSFP, il faut que des calculs sur (a1 a3)(a2 a3) diminuent le niveau des calculs sur a3, car ils sont dans des NFSFP séparés. Comme (a1 a3), (a2 a3), (a1 a3)(a2 a3) sont le résultat d'un équilibrage provenant de d, c ne contient pas les calculs élémentaires pour baisser les niveaux des calculs de a3. Donc la seule origine possible proviendrait de calculs élémentaires de d. Notament d doit comporter le calcul de l'application de (a1 a3) sur (a2 a3).

Essai 16

L'idée

On reprend les idées du 15 avec les différences suivantes :

  • On définie une fonction de jonction, la définition est doublement récursive : à l'intérieur d'un niveau et pour passer d'un niveau à l'autre.
  • On montre que les deux récursions sont finies.
  • Pour simplifier les démonstrations, on montre et utilise l'indépendance des calculs et de l'algorithme si les NFSFP des calculs sont disjoints.

Essai de preuve

Définition de la fonction "balancing"

Domaine de balancing :

  • x est une formule
  • c et d sont des calculs loose valides sur x

Nous définissons balancing x c d par récurrence :
- Si orderedCalc c = orderedCalc d :

balancing x c d = c
- Sinon :
Soient ct = orderedCalc c et dt = orderedCalc d.
Soit s un NFSFP de ct ou dt minimal suivant l'ordre par niveau tel que le nombre de calcul élémentaires représenté par s est différent entre ct et dt.
S'il y a moins de calculs élémentaires s dans ct on définit balancing x c d = balancing x c (d +le s)
Sinon on définit balancing x c d = balancing x (c +le s) d

Propriétés de la fonction "balancing"

Croissance des niveaux :

Le niveau des calculs élémentaires ajoutés par balancing est croissant car l'ajout d'un calcul élémentaire de niveau n à c ou d n'a pas d'influence sur les calculs élémentaires de niveau > n dans ct ou dt.

Récursion finie de "balancing" à un niveau donné

Nous prouvons ici que pour un niveau fixé n, balancing ne peut pas boucler indéfiniment en ajoutant des calculs de niveau n.

Comme un calcul de niveau n ne change pas l'ensemble des NFSFP valides de niveaux ≤ n et comme les calculs élémentaires ajoutés par "balancing" ont un niveau croissant, on déduit que lors de l'ajout des calculs élémentaires de niveau n par "balancing" les NFSFP de niveau n valides sur les formules résultant des calculs produits par "balancing" sont finis.
Donc si "balancing" avait une récurrence infinie au niveau n alors il y aurait une infinité de calculs élémentaires pour un certain NFSFP de niveau n. Soit s un NFSFP de niveau n. D'après ce qui précède, il nous suffit de prouver qu'il ne peut y avoir une infinité de calculs de NFSFP s ajoutés par "balancing". Comme le théorème est symétrique en y et z, on pourra supposer que l'infinité de calculs est ajouté à c, ce que nous faisons désormais, pour raisonner par l'absurde :

Si orderedCalc ne générait au total qu'un nombre fini de calcul au niveau n (l'inversion de place des calculs élémentaires peut dupliquer des calculs) alors, comme "balancing" est une fonction par équilibrage (on ajoute ce qui manque de chaque côté), on ne pourrait arriver à une infinité de calculs élémentaires ajoutés de NFSFP s. Il y a donc un nombre infini de "distribute" (seul calcul produisant de nouveaux calculs élémentaires).

Si on a un "distribute a1 a2 a3" en tant que fonction d'un endroit de NFSFP s, alors il est calculé en "a1 a3 \ a2 a3". Si un seul des a3 était utilisé (sous-entendu pour les calculs à cet endroit) par les calculs s, alors on serait dans un cas équivalent à ce qu'il n'y ait pas de duplication des calculs et on a déjà vu que ce cas est impossible. Donc les calculs des deux a3 sont utilisés.

Au départ, un des calculs a le plus de calcul à cet endroit et ce niveau, regardons pour le dernier des calculs élémentaires ajoutés :
- Si l'ajout du dernier calcul n'engendre pas de calcul supplémentaire, alors la jonction à ce niveau est finie.
- Sinon la fonction minimale de la sous-formule à cet endroit est un distribute ou un if (sinon il n'y aurait pas de calcul possible) :
- Si c'est un distribute d'arguments a1, a2 et a3 :
Les calculs sur a1 sont ajoutés, ou si a1 est un if, les calculs sur la condition (a3) peuvent être ajoutés s'il y a assez d'arguments.
- Si c'est un if d'arguments 1b ou 0b, a2 et a3 :
Les calculs sur a2 ou a3 sont ajoutés.
- Si c'est un if d'argument a1, a2 et a3 ou a1 n'est ni 1b ni 0b : Voir le calcul de a1

rebut :
Soit c un calcul sur une formule x et s un NFSFP valide sur calculate loose c x. Si le nombre de calculs élémentaires dans orderedCalc c de NFSFP s est n, quel peut être le nombre de calculs élémentaires dans orderedCalc (c +le s) de NFSFP s ? Nous avons différents cas où ce nombre peut être >n+1 :
- si s fait apparaître un if alors la fonction "norm" peut transformer un calcul de condition en calcul de NFSFP s.
- si s est sur un if, il peut déplacer des calculs sur les arguments en calculs d'identifiant s
Ces cas sont des déplacements de calculs sans duplication. S'il n'y avait pas la duplication il ne pourrait y avoir qu'un nombre fini de déplacements et donc on ne pourrait avoir un nombre infini de récursion de balancing.
Le calcul "distribute" génère une duplication des calculs sur son dernier argument. Donc combiné avec un calcul de if nous pourrions avoir un apport infinie de calculs élémentaires.

Trouver des limites à la duplication (pas fini)

Sans duplication des calculs on ne peut avoir de récurrence infinie dans la définition de "balancing". L'idée, ici, pour montrer qu'il n'y a pas de récurrence infinie, est de prouver que les calculs dupliqués ne peuvent pas être tous les deux utilisés (et donc c'est comme s'il n'y avait pas de duplication).→c[loose]1

On a distribute a1 a2 a3 →c[loose]1 (a1 a3 \ a2 a3)

On a distribute distribute distribute a3 a4 →c[loose]1 distribute a3 (distribute a3) a4

→c[loose]1 a3 a4 ( distribute a3 a4 )

Duplication et nombre de calculs excédentaires (pas fini)

Quand on ajoute un calcul qui porte sur un distribute, les calculs de a3 sont dupliqués. Sans cette duplication on pourrait prouver que la récursion de "balancing" est finie en comptant les calculs restant à ordonner (les calculs inférieurs au niveau auxquels on ajoute des calculs sont déjà ordonnés).

Regardons la quantité de calculs qui ne sont pas encore équilibrés (NUC = Number of Unballanced Calculations), en additionnant les quantités des deux calculs.
Par exemple :

- Si un calcul ajouté ne s'applique pas sur un distribute, alors NUC diminue de 1 plus le nombre de calculs qui deviennent communs du fait de déplacements de calculs. Par exemple si on introduit un calcul sur "if 1b a2 a3" et qu'il y a un calcul sur a2 et que du côté excédentaire il y a encore un calcul à ajoute, alors NUC diminue d'au moins 3, car le calcul introduit par a2 s'équilibre.
- Si un calcul s'applique sur un "distribute a1 a2 a3" (qui devient "a1 a3 \ a2 a3"), alors les calculs qui étaient sur et dans a3 sont dupliqués et donc augmentent NUC.

Examiner le dernier calcul élémentaire ajouté (pas fini)

On suppose que pour un endroit (un NFSFP) donné, on doit ajouter des calculs élémentaires car d est en excédent. Si la formule résultante à cet endroit après le dernier ajout provient d'un :

- "distribute a1 a2 a3" : alors la sous-formule résultante est un "a1 a3 \ a2 a3". Les calculs élémentaires provenant de la formule elle-même à cet endroit ne peuvent provenir que de a1.
- "if a1 a2 a3" où a1 = 1b ou 0b : Les calculs élémentaires provenant de la formule elle-même à cet endroit ne peuvent provenir que de a2 ou a3.
- "if a1 a2 a3" où la condition a1 n'a pas finie d'être calculée : Les calculs élémentaires provenant de la formule elle-même à cet endroit ne peuvent provenir que de a1.

Essai de boucle (pas fini)

Soit f = $FR f → f, on a f = self \ selfx $F f → f = self \ selfx \ if 0b 0b = selfx (if 0b 0b) \ selfx \ if 0b 0b
= (if 0b 0b) ( selfx \ if 0b 0b ) ( selfx \ if 0b 0b ) = ( selfx \ if 0b 0b ) ( selfx \ if 0b 0b ) = selfx (if 0b 0b) \ selfx \ if 0b 0b
On a bien une boucle infnie si on veut calculer la valeur.
selfx = $F f, x → f \ x x = $F f → $F x → f \ x x = $F f → distribute ($F x → f) ($F x → x x)
= $F f → distribute (constF f) (distribute identF identF)

Faire la jonction sur l'argument a3 avant le distribute ? (pas fini)

L'idée est de ne pas dupliquer de calcul. L'idée est que si on a à ajouter un calcul élmentaire qui fait calculer un "distribute a1 a2 a3", alors on commence par faire la jonction de a3. Est-ce possible ?

Récapitulatif (pas fini)

On se place dans le cas où il y a plus de calculs du côté d.
- Un calcul est ajouté à c

-Si ça n'engendre pas de calcul supplémentaire en c :
- Si il y a équilibre, c'est fini à cet NFSFP
- Sinon on retourne au début
-Si ça engendre des calculs supplémentaires en c, on réévalue l'équilibre :
- Si il y a équilibre, c'est fini à cet NFSFP
- S'il y a toujours plus de calculs du côté d : on retourne au début
- S'il y a plus de calculs du côté c : les calculs ne peuvent concerner que la partie de la sous-formule qui est le résultat du calcul (et non tout l'endroit). On rééquilibre en ajoutant du côté d.

On voit que quand il y a un changement du côté excédentaire alors la zone concernée par le calcul est réduite aux calculs de la sous-formule résultant du dernier calcul élémentaire. Donc la jonction de cette partie sera réduite au SFP ( et non NFSFP ) de ce résultat.
En réduisant la zone concernée on réduit le nombre de calculs élémentaires concernés. Il faut prouver que le NUC réduit à cette zone décroît (raisonner sur la profondeur de la formule parait difficile car les calculs peuvent l'augmenter).
Le NUC d'un SFP n'est pas forcément décroissant, car le calcul d'un distribute peut engendrer une augmentation des calculs. Mais pour que ces calculs ne soient pas abandonnés par réduction du SFP de l'endroit de jonction, que faut-il ?
Exemple :

Utiliser des SFP pour les calculs (pas fini)

On peut définir le calcul floose qui est comme le calcul loose mais où l'on peut utiliser des SFP à la place de NFSFP.
L'intérêt du calcul floose est de préciser la zone fonctionnelle concernée par le calcul.
On peut montrer que l'on peut traduire un calcul loose en calcul floose et inversement.
Le théorème de calcul trié ne change pas, car pour un même niveau argumental on ne peut pas trier les calculs suivant le niveau fonctionnel.

Tracer par le calcul ?

On a déjà défini un système de trace, qui est un arbre, et qui est relié par un calcul. Il y a peut-être une manière plus pratique, qui consiste à déterminer les calculs élémentaires d'un calcul qui concerne une sous-formule de départ. Ce serait une liste binaire, de même longueur que le calcul, indiquant si le calcul concerne l'élément de départ ou non. Cette forme de trace prend en compte les duplications, déplacements et disparitions lors du calcul. Par ce système on ne sait pas combien il y a de duplication.

Calcul des deux arguments a3 d'un distribute (pas fini)

L'augmentation du nombre de calcul ne peut venir que du calcul d'un distribute a1 a2 a3, qui retourne a1 a3 \ a2 a3. Pour qu'il y ait doublement des calculs, il faut que les deux a3 soit calculés dans le même NFSFP. On se propose ici d'étudier comment cela est possible.

Problème : si on a une formule "x y", combien faut-il de calculs pour que le calcul suivant concerne y ?

Il faut au moins le nombre de caluls univocal que l'on peut faire sur x seul + 1.

Théorème à démontrer :

Énoncé :
Soient
- x une formule
- s1 et s2 deux SFP sur x disjoints
- c un calcul univocal sur x
tq la trace de s0 et s1 soient calculées chacunne au moins en partie,
alors il existe un k∈{0,1} et t un SFP des traces de sk tq :
- la partie du calcul c sur t est terminée
- il existe un calcul élémentaire englobant la trace de t et une trace de s1-k

Essai 15

Contexte

On reprend l'essai 14 qui est ok sauf pour la preuve de l'application de la récurrence. En effet, ce n'est pas évident que la récurrence est finie.

Nous devons prouver que la récurrence s'arrête (un calcul valide a un nombre fini de calculs élémentaires).

Début de preuve

Soient :

  • cn et dn deux calculs valides sur une formule x.
  • y = calculate loose cn x
  • z = calculate loose dn x.

D'après le théorème du calcul trié il existe c et d des calculs équivalents à respectivement cn et dn, où c et d sont triés par l'ordre défini dans ce théorème.

Soit H n l'hypothèse de récurrence : il existe des calculs a et b valides sur y et z de sorte que si on trie les calculs (c +ll a) et (d +ll b) alors ils sont identiques jusqu'au niveau n.

Précision : "identiques jusqu'au niveau n" signifie que les débuts des deux listes contenant les calculs élémentaires de niveau 0 à n sont identiques.

Preuve de H 0

Remarque : nous avons vue que le résultat de l'inversion d'un calcul élémentaire de niveau 0 avec un calcul élémentaire de niveau strictement supérieur contient un unique calcul élémentaire de niveau 0 qui est celui de départ.
Supposons nc et nd le nombre de calcul élémentaires de niveau 0 de c et d. Soit n = nc - nd. Nous supposerons que n>0 (sinon, la proposition étant symétrique, on inverse c et d).
Soit b, n calculs élémentaires de niveau 0 (c'est une liste de n ∅l). Si on ordonne d +ll b, on a un calcul de nc calculs élémentaires de NFSFP ∅l. Donc en prenant a = ∅l on vérifie H 0.

Preuve de H (n + 1) sous l'hypothèse H n

D'après l'hypothèse de récurrence il existe des calculs a1 et b1 valides sur y et z de sorte que si on trie les calculs (c +ll a1) et (d +ll b1) alors ils sont identiques jusqu'au niveau n.

Soient :

  • cat le calcul c +ll a1 trié
  • dat le calcul d +ll b1 trié
  • t la troncature de cat et dat aux calculs élémentaires de niveau ≤ n
  • c1 et d1 les restes des calculs (on a donc cat = t +ll c1 et dat = t +ll d1)
  • x2 le résultat du calcul de x par t
  • S l'ensemble des NFSFP de x2 de niveau n+1

Comme c1 et d1 ne sont constitutés que de calculs de niveau >n, tous les NFSFP correpondants commencent par un NFSFP de S. Donc tout au long des calculs de c1 et d1 l'ensemble des NFSFP de niveau n+1 de la formule calculée reste S. De plus deux calculs n'ayant pas le même commencement dans S sont indépendant (et donc inversables).
Donc pour un s de S, on peut relativiser les calculs de c1 et d1 de cette partie pour les voirs comme des calculs sur la sous-formule à l'endroit s. Ces calculs relativisés ont un niveau diminués de n+1. On peut donc appliquer l'hypothèse de récurrence pour unifier les calculs concernant l'endroit s. On obtient ainsi l'unification au niveau n+1 à l'endroit s. Comme les calculs des différents endroits désignés par S sont indépendants, on peut ajouter toutes les unifications des différents endroits désignés par S.
On peut donc ainsi construire c2 et d2 de sorte que t +ll c1 +ll c2 et d = t +ll d1 +ll c2 soient unifiés au niveau n+1.

Finitude de la récurrence

Pour n∈ℕ soit an
Pour prouver le théorème, il nous faut trouver des calculs à ajouter (a et b dans l'hypothèse de récurrence) satisfaisant pour tout niveau. Pour cela nous allons montrer que

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

Essai 14

Contexte

L'essai 13 a deux problèmes :

  • La fonction Trace doit refléter tout le calcul, mais quand la condition d'un if est rassemblée avec le if, on ne reprend pas tout les calcul provenant de la condition si la condition est une formule crée (voir dans l'essai 13 "Propriétés sur les calculs et la relation Trace" , le dernier paragraphe).
  • C'est une preuve complexe.

L'idée explorée ici est la suivante :

On réordonne les calculs de sorte qu'ils soient équivalents (même formule de départ et d'arrivée) et avec l'ordre suivant : les calculs élémentaires sont sont classés en ordre croissant par niveau. Puis on unifie les deux calculs en ajoutant les calculs élémentaires par ordre de niveau. À chaque calcul ajouté il faut recalculer les calculs équivalent dans l'ordre.
Cette méthode s'appuie sur diverses propriétés comme :
- la possibiliter de réordonner les calculs
- un calclul élémentaire ne disparait pas si on le place avant celui d'un niveau plus grand

Nécessiter de séparer les niveaux de calcul

Pour pouvoir réordonner les calculs par niveau, il faut que soit :

  • Le calcul élémentaire d'un niveau plus élevé ne soit pas nécessaire à un niveau plus bas (sinon la dépendance empêcherait d'inverser les calculs élémentaires).
  • Le calcul élémentaire d'un niveau plus élevé puisse être vu comme d'un niveau plus bas (c'est le cas pour la condition d'un if).

C'est pourquoi nous devons modifier les calculs pour que les calculs des conditions des if soient vu comme des calculs sur les if.

Normalisation des calculs sur les conditions

La fonction de normalisation transforme un calcul quelconque en un calcul équivalent point à point, en transformant les calculs directs sur les conditions des if (où le NFSFP pointe directement sur la condition) en calculs sur le if.
Donc après normalisation il n'y a plus de calcul directement sur la condition du if (mais bien sûr il peut y en avoir sur les arguments de la condition des if).

Remarquons que la normalisation doit éventuellement être faite après une réordonancement entre deux calculs élémentaires, par exemple (à voir si c'est le seul cas) si on calcul a1 a2 ... an que l'on inverse avec le calcul de a2, où le calcul élémentaire de a1 a2 ... an aboutit à "if a2 ... an".

Étude sur le réordonancement des calculs par niveau

On étudie ici comment inverser deux calculs élémentaires (dénomés "principal" et "précédent") quand le principal est de niveau strictement inférieur au précédent.

On a deux cas, les deux NFSFP des deux calculs sont disjoints ou non. S'il ne sont pas disjoints, alors le calcul précédent porte sur l'intérieur du calcul principal.

Si les NFSFP des deux calculs élémentaires sont disjoints

Voir SFP disjoints.
Dans ce cas les deux calculs ne s'impactent pas l'un l'autre.
→ On a juste à inverser les deux calculs élémentaires.

Si le niveau de calcul principal est 0 et que le calcul précédent porte sur l'intérieur du calcul principal

On se place dans ce cas pour simplifier, on généralisera ces cas plus tard.

Nous divisons les cas suivant que la forme de la formule sur laquelle porte le calcul principal :

"f a1 a2 ... an" où le calcul précédent porte sur ou à l'intérieur d'un argument ak où k>3.

Comme l'argument calculé dans le calcul précédent ne concerne pas la partie de formule modifiée, et que l'adresse de l'argument reste inchangé par le calcul principal :
→ On a juste à inverser les deux calculs élémentaires.

"if a1 a2 ... an" où a1 est 0b ou 1b et où le calcul précédent porte sur ou à l'intérieur de l'argument (a2 ou a3) abandonné.

Comme l'argument sur calcul précédent n'a pas de conséquence :
→ On détruit le calcul préçédant.

"if a1 a2 ... an" où a1 est 0b ou 1b et où le calcul précédent porte sur ou à l'intérieur de l'argument (a2 ou a3) retourné.

On peut inverser les deux calculs, il faut juste tenir compte du changement de SPF.
→ On inverse les deux calculs en relativisant le NFSFP du calcul préçédant pour l'adapter au nouvel endroit.

"if a1 a2 ... an" où a1 n'est ni 0b ni 1b et si le calcul précédent porte sur la condition du if.

C'est donc la condition du if qui est calculée. Le calcul préçédent étant de niveau supérieur, il porte sur l'intérieur de la condition. On se retrouve donc dans le même cas qu'une inversion de calcul où la formule générale est la condition. On peut donc appliquer les mêmes règles.
→ On relativise les deux calculs élémentaires comme si la condition était la formule générale, on applique les règles d'inversion, puis on relativise le résultat pour qu'il porte sur la condition.

"if a1 a2 ... an" où a1 n'est ni 0b ni 1b et si le calcul précédent porte sur autre chose que la condition du if.

Les calculs sont indépendants, on peut donc les inverser sans les modifier.
→ On a juste à inverser les deux calculs élémentaires.

"distribute a1 a2 ... an" où le calcul précédent porte sur ou à l'intérieur d'un argument ak où 1 ≥ k ≥ 3.

La sous-formule calculée par le calcul précédent n'est pas modifiée par le calcul "distribute", mais seulement déplacée et éventuellement dupliqué pour a3. On pourra donc inverser en s'adaptant au déplacement et à l'éventuelle duplication.
→ On inverse les deux calculs. On adapte le calcul précédant à la nouvelle place de l'argument. On duplique le calcul précédent s'il portait sur l'argument a3 où chacun des calculs dupliqué portera sur l'une des duplication.

Si le niveau de calcul principal est >0 et que le calcul précédent porte sur l'intérieur du calcul principal

On peut appliquer les règles où le calcul principal est de niveau 0, en relativisant à la sous-formule concernée.

Calcul trié

Nous venons de voir que nous pouvons toujours faire remonter un calcul élémentaire s'il est de plus faible niveau que le calcul précédant, que cette inversion pouvait changer (voir détruire ou dupliquer) le calcul précédant, mais qu'il ne changeait pas le calcul de plus faible niveau.

Nous allons définir ici le tri (basé sur l'algorithme du tri à bulles) suivant sur un calcul c :
1) on répète l'opération suivante autant de fois que la longueur maximale du calcul en cours le plus grand (la taille peut varier) :

1) on normalise le calcul (voir plus haut)
2) on parcourt les calculs élémentaires en échangeant deux calculs élémentaires si on a soit :
- le calcul suivant est de plus bas niveau
- si les deux calculs élémentaires sont de même niveau : si le NFSFP du suivant est plus petit suivant l'ordre binaire des listes des NFSFP

On voit que l'on obtient par cette fonction de tri un calcul équivalent (qui a la même formule d'arrivée) et trié par un ordre stricte.

Remarque : deux calculs équivalent peuvent avoir être différents une fois triés car le tri n'élimine pas les calculs élémentaires inutils.

Preuve de la jonction des calculs

Soit c et d deux calculs sur une formule x.

Nous avons vu que pour tout calcul il existe un calcul équivalent normalisé et trié. C'est pourquoi nous allons supposer que c et d sont normalisés et triés.

Soit H c d x n l'hypothèse de récurrence : il existe a et b de sorte que si on trie les calculs (c +ll a) (d +ll b) alors ils sont identiques jusqu'au niveau n.

Preuve de H c d x 0

Remarque : nous avons vue que le résultat de l'inversion d'un calcul élémentaire de niveau 0 avec un calcul élémentaire de niveau strictement supérieur contient un unique calcul élémentaire de niveau 0.
Supposons nc et nd le nombre de calcul élémentaires de niveau 0 de c et d. Soit n = nc - nd. Nous supposerons que n>0 (sinon on inverse c et d).
Soit b, n calculs élémentaires de niveau 0 (c'est une liste de n ∅l). Si on ordonne d +ll b, on a un calcul de nc calculs élémentaires de NFSFP ∅l. Donc en prenant a = ∅l on vérifie H c d x 0.

Preuve de H c d x (n + 1) sout l'hypothèse H c d x n

On suppose que c et d sont triés.
D'après l'hypothèse de récurrence c et d sont égaux dans la partie allant jusqu'au niveau n.

Soient :

  • t la partie de c et d des calculs élémentaires de niveau ≤ n
  • c1 et d1 les restes des calculs (on a donc c = t +ll c1 et d = t +ll d1)
  • x2 le résultat du calcul de x par t
  • S l'ensemble des NFSFP de x2 de niveau n+1

Comme c1 et d1 ne sont constitutés que de calculs de niveau >n, tous les NFSFP correpondants commencent par un NFSFP de S. Donc tout au long des calculs de c1 et d1 l'ensemble des NFSFP de niveau n+1 de la formule calculée reste S. De plus deux calculs n'ayant pas le même commencement dans S sont indépendant (et donc inversables).
Donc pour un s de S, on peut relativiser les calculs de cette partie pour les voirs comme des calculs sur une formule globale. On peut donc appliquer l'hypothèse de récurrence pour unifier les calculs concernant l'endroit s. Comme les calculs des différents endroits désignés par S sont indépendants, on peut ajouter toutes les unifications des différents endroits désignés par S.
On peut donc ainsi construire c2 et d2 de sorte que t +ll c1 +ll c2 et d = t +ll d1 +ll c2 soient unifiés au niveau n+1.

Application de la récurrence

On a donc pour tout n, H c d x 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)

CQFD

Essai 13

Contexte

L'essai 12 ne prend pas en compte les formules crées (c'est à dire les "b c" provenant des "distribute a b c", voir l'explication au paragraphe ci-dessous). Hors il me semble maintenant que ce serait difficile d'unifier les calculs par étapes, en traitant déjà les formules non créer puis en recommençant le processus. Donc l'idée ici est de faire comme dans l'essai 12 mais en changeant la relation "Trace" de sorte que les formules crées soient aussi représentées. Pour cela on remplace dans la relation Trace l'argument "chemin du calcul" par une liste dénomée "chemin du calcul" où chaque élément représente l'exécution d'un calcul ainsi que la partie de la formule produite que l'on désigne : 0b pour le résultat entier ou 1b pour le "b c" d'un distribute.

Seulement des NFSFP pour désigner les sous-formules

On a vu dans l'essai 12 que seul les NFSFP sont utilisées pour représenter les calculs élémentaires. Nous utilisons ici seulement des NFSFP pour désigner les sous-formules.
Pourquoi ce choix :

Nous avons besoin de représenter les calculs en évitant les duplicités de représentation, car il nous faut comparer les calculs. Hors on peut se limiter, au prix de réorganiser les traces (voir ci-dessous), à ne désigner que les NFSFP. Cette limitation est nécessaire car une fonction d'une formule peut disparaitre (par exemple le "if a" de "if a b c"). Hors ce qui disparait peut être un calcul ayant une influance sur la suite, qu'il faut donc représenter dans la trace des calculs. Pour ne pas avoir ces disparitions il nous faut désigner la formule la plus grosse possible (donc par un NFSFP) contenant la fonction.
Ce choix pose des contraintes, par exemple :
Si on calcul "if 0b a b c", comment tracer "b" (car on passe par la formule "b c") ? : un calcul sur b appliqué à b c revient au même. D'autre part, pour n'avoir qu'une trace par SFP sur la formule finale, il faudrait rassembler la trace de b avant le calcul du if avec la trace de "if 0b a b c". La solution est de supprimer la trace de b précédent le calcul élémentaire sur le if et d'appliquer le calcul sur b à la suite du calcul du if. Remarquons que l'on a alors une trace qui ne reflète pas le calcul réel, mais qui représente un calcul équivalent. b peut être apparu lors du calcul (par un distribute), il faut alors ne prendre en compte, de la liste "chemin du calcul", que la partie après sa création (car avant elle ne concerne pas "b" mais l'expression qui l'a engendré).
Pour distribute, on a distribute a b c = (a c) (b c). On ne peut pas continuer de tracer purement a après le calcul élémentaire sur distribute, car il est une fonction d'une formule plus grande (sinon on contredirait la règle que l'on s'est donné de n'utiliser que des NFSFP). Donc comme pour le if on doit supprimer la trace de a et appliquer le calcul sur a à la suite du calcul du distribute. Remarquons que l'on doit faire la même chose pour b.

On vient de voir que l'on réorganise le calcul dans la trace. Qu'en est-il pour le calcul de la condition d'un if ?

En effet, on pourrait calculer la condition, puis calculer une formule pour s'appercevoir que c'est un if. Donc on peut comprendre que l'on a calculé une condition après seulement s'être apperçu que l'on est dans une formule "if". Mais la règle de calcul de la condition d'un if ne fonctionne que s'il a 3 arguments, on pourrait avoir d'abord le calcul d'une condition, puis de la partie qui aboutit à un if, et enfain l'adjonction d'autres arguments.
On pourrait réorganiser le calcul de la condition juste avant d'appliquer le if (car là on est sûr d'avoir tous les arguments). Il suffirait d'appliquer le calcul (argument "chemin du calcul" de la trace) sur la formule if juste avant l'application du if.

Donc que ce soit pour la condition du if ou les sous-formules devenant des fonctions, on réorganiser les traces.

Représenter les calculs

L'idée est de désigner dans la formule de départ, un SFP ainsi que les calculs subits par ce SFP.

Nous voulons représenter un calcul par une relation "Trace" qui prend en argument :

  • le calcul c (argument dénomé "le calcul")
  • la formule subissant le calcul (argument dénomé "formule de départ")
  • un SFP de la formule de départ (argument dénomé "SFP de départ")
  • un SFP de la formule résultante du calcul (argument dénomé "SFP d'arrivée")
  • une liste représentant les exécutions de calcul (argument dénomé "chemin du calcul"), où un élément :
    • 0b : représente l'exécution où le résutlat entier est désigné
    • 1b : représente l'exécution d'un "distribute a b c" où le résultat "b c" est désigné.

Propriétés sur les calculs et la relation Trace

Étendue des Traces

Tout NFSFP doit être tracé. Il est inutile de tracer les FSFP car, contrairement à un argument, une partie fonction ne peut être séparer de sa formule et les calculs sont représentés par des NFSFP.

Quand une sous-formule peut disparaître lors d'un calcul :

Quand on exécute le calcul élémentaire sur "if a b c" on fait disparaître les sous-formules "if a b", "if a", "if", "a" et suivant la valeur de a, "b" ou "c". Quand on exécute le calcul élémentaire sur "distribute a b c", on fait disparaître les sous-formules "distribute a b", "distribute a" et "distribute".

Dans l'argument "chemin du calcul", quels sont les éléments spécifique à la sous-formule désigné par le SFP d'arrivé ?

Ceux après le dernier 1b. Car à chaque 1b cela signifie que la sous-formule est nouvelle.

Pour un certain calcul c, une certaine formule de départ, un certain SFP de départ, un certain chemin de calcul l, le SFP d'arrivé est-il fixé ?

Oui car pour chaque étape de calcul le SFP d'arrivé suivant est déterminé par la calcul élémentaire effectué sur la formule et le chemin de calcul (qui déterminé éventuellement si l'on désigne l'argument ou non).

Pour un certain calcul sur une certaine formule de départ, un NFSFP d'arrivé sy fixé, a-t-on un et un seul chemin du calcul et NFSFP de départ ?

Oui, on le montre par résurrence (sur la longeur du calcul) sur Trace.

Pourquoi il faut définir Trace en commençant par la fin du calcul :

Si on calcul x1 x2 x2 x3 en commençant par calculer x2, puis x1. Alors si le résultat du calcul de x1 est "if", on ne sait qu'à posteriori que x2 est la condition d'un if. Donc pour définir la relation Trace il faut commencer par examiner la fin du calcul et réinterpréter éventuellement des calculs précédent (comme les calculs des conditions des if) comme calcul plus global.

Un calcul élémentaire ne doit apparaître au plus qu'une fois dans la relation Trace.

Par exemple si on calcul if (if 1b 1b 1b) 0b 1b , le calclul interne de if 1b 1b 1b ne doit apparaître que comme calcul sur la formule globale (puisqu'il faut calculer la condition du if global pour calculer la formule globale). Voir aussi les cas du paragraphe ci-dessus.

Si deux calculs partant de la même formule ont des relations Trace identiques alors le résultat est-il identique ?

Oui. Cette propriété est à démontrer.

Comment déplacer les calculs effectués (et sous-calculs) effectués sur une certaine sous-formule sur une autre sous-formule ?

Remarque : on a besoin de cela dans la définition de Trace, pour réordonner certains calculs.
Soit le NFSFP sy d'arrivé désignant cette formule (disons y) une fois les calculs effectués.

Comment peut-on associer le calcul de la condition du if avec le calcul du if ?

Par exemple is on calcule : distribute (constF if) c d a b
Ce calcul aboutit à if (c 1b) a b. La formule "c d" est crée par le distribute. Mais c ou d peuvent avoir été calculé avant ou non. à continuer

Définition de Trace

On définit Trace récursivement sur la longueur des calculs. Pour un certain calcul et une certaine formule de départ nous définissions Trace par extension de la manière suivante : pour chaque NFSFP d'arrivé (valide) nous donnons les uniques paramètres manquant (le SFP de départ et le chemin de calcul) permetant de vérifier la relation Trace. Cela s'appuit donc sur des propriété d'unicité sur Trace, que l'on pourra vérifier par récurrence.

Si le calcul est de longueur 0

Soit c un calcul de longeur 0 et x la formule de départ. Pour tout SFP sx et sy valide pour x et toute liste binaire l, on a Trace c x sx sy l ssi :

  • sx = sy
  • sx est un NFSFP
  • l = ∅l

Si le calcul est de longueur n+1

Soit c un calcul de longeur n+1, soit c1 et ce tq c = c1 +le ce.
Soit x1 une formule tq c soit un calcul valide sur x1.

Soient :

  • sce le NFSFP représentant ce
  • x2 = calculate loose c1 x1
  • x3 = calculate loose c x1
  • scw le SPF désignant la fonction minimale de la formule désignée par sce sur x2
  • w le mot désigné par scw (une fonction minimale est un mot).
  • scf = listInit \ listInit \ listInit scw (c'est à dire le SPF pointant sur la fonction minimale avec ses 3 arguments).

Comme sce est un calcul valide sur x2, w est soit "if" soit "distribute".
Soit sx3 un NFSFP valide.

- Si sx3 et scf sont disjoints :

Dans ce cas le calcul n'impacte pas la formule pointée par sx3. Donc les traces sont les mêmes entre c1 et c.
Soit l et s tq Trace c1 x s sx3 l = 1b
On définit Trace c x s sx3 l = 1b
- Si sce est strictement interne à sx3 :
Dans ce cas le calcul se fait sur/dans un argument de la formule pointée par sx3. Cela n'impacte ni l'endroit où se trouve la formule en sx3, et Trace n'a pas à tenir compte ici d'un calcul sur la formule en sx3 elle-même.
Soit l et s tq Trace c1 x s sx3 l = 1b
On définit Trace c x s sx3 l = 1b
- Si w est "if" :
- si sce = sx3 :
Dans ce cas sx3 est l'endroit où le calcul est effectué, il désigne donc la formule résultant du calcul. Le calcul du "if" fait que la trace de la condition et de la sous-formule retournée disparaissent, car, pour la condition la formule elle-même disparait, pour la sous-formule retournée car il ne peut y avoir deux traces par NFSFP et qu'il y a la trace de la formule entière. Hors ces deux traces impactent le calcul et doivent donc être incorporéess d'une manière ou d'une autre. C'est pourquoi on change l'ordre des calculs ainsi :
- le calcul de la condition est déplacé juste avant le calcul élémentaire du if, en tant que calcul sur la formule entière (rappelons que le calcul loose permet ce calculer la condition d'un "if").
- le calcul de la valeur retournée qui a été effectué avant le calcul du if est déplacé juste après le calcul du "if".
Pour le calcul de la condition :
Comme son calcul aboutit à 0b ou 1b (donc une formule sans argument), il n'y a qu'une seule trace qui porte donc sur la condition entière. Il nous suffit donc de prendre la liste du chemin de calcul à partir du dernier 1b (non compris, ou depuis le début s'il n'y a pas de 1b), car ce 1b (s'il existe) correspond à la création de la condition. Soit lc la liste (de 0b) correspondant au nombre de calculs élémentaires sur la condition.
Pour l'argument retourné par "if" :
Pour les sous-formules de l'argument, il suffit de relativiser leur SFP sans rien changer d'autre.
Pour l'argument lui-même, les calculs sur celui-ci (qui sont indépendant de ses sous calculs, par construction de Trace), sont ajoutés après le calcul du if. Pour déterminer ses calculs il suffit de prendre la liste "chemin de calcul" après le dernier 1b (sa création) ou s'il n'y en a pas depuis le début. Soit lr la liste (de 0b) correspondant au nombre de calculs élémentaires sur l'argument retourné.
Soit l et s tq Trace c1 x s sx3 l = 1b
On définit Trace c x s sx3 \ l +ll lc +ll $L[0b] +ll lr = 1b
- Si sx3 est strictement interne à sce :
sx3 désigne alors un endroit à l'intérieur de l'argument retourné par if. L'intérieur de cet argument n'est pas modifié, par contre son adresse a changé. Il nous faut juste reprendre le trace correspondant à son ancienne adresse, qu'il nous faudra d'abord calculer.
Calculons sr, l'endroit désigné par sx3 relativement à l'argument retourné. Soit sr tq sx3 = sce +ll sr (remarque : sr n'est pas la liste vide).
Calculons sa, l'endroit dans x2 de l'argument retourné par le if : scf +ll $L[1b] si la condition du if est 0b et sinon scf +ll $L[0b, 1b].
Soit l et s tq Trace c1 x s (sa +ll sr) l = 1b
On définit Trace c x s sx3 l = 1b
- Si w est "distribute" :
- si sce = sx3 :
Dans ce cas sx3 est l'endroit où le calcul est effectué, il désigne donc la formule résultant du calcul. On a distribute a b c = (a c) (b c). Nous avons ici la création d'une nouvelle trace : "b c". Pour la même raison que l'argument retourné pour "if", la trace de "a" se joint à la trace en sx3 et la trace de "b" se joint à la nouvelle trace à l'endroit de "b c". D'autre part l'argument "c" est dupliqué dans le résultat, cela ne demande pas d'adaptation et prouve qu'à un SFP de départ peut correspondre plusieurs SFP d'arrivée. Il nous faudra donc :
- que le calcul sur les arguments "a" et "b" qui ont été effectués avant le calcul de distribute soient déplacés juste après le calcul du distribute.
- tenir compte du cas spécial de la nouvelle sous-formule "b c"
Soit lr la liste (de 0b) provenant du chemin de calcul de a après le dernier 1b (ou toute la liste s'il n'y en a pas).
Soit l et s tq Trace c1 x s sx3 l = 1b.
On définit Trace c x s sx3 \ l +ll $L[0b] +ll lr = 1b
- Si sx3 est strictement interne à sce :
sx3 désigne alors un endroit à l'intérieur de la formule retournée par distribute. Nous avons alors les possibilités suivantes par rapport à l'endroit désigné par sx3 qui peut être :
- strictement à l'intérieur de "a c" : on a alors les sous-cas sur l'endroit désigné :
- strictement à l'intérieur de "a" : il suffit de continuer ce calcul mais en le déplaçant au nouvel endroit :
Calculons sr, l'endroit désigné par sx3 relativement à "a" dans x3 : soit sr tq sx3 = scf +ll $L[0b,0b] +ll sr (remarque 1 : $L[0b,0b] est l'endroit de "a" dans "(a c) (b c)"; remarque 2 : sr n'est pas la liste vide).
Calculons l'endroit dans x2 correspondant à sx3 dans x3 : sx2 = scf +ll $L[0b,0b,1b] +ll sr
Soit l et s tq Trace c1 x s sx2 l = 1b.
On définit Trace c x s sx3 l = 1b
- à l'intérieur de c : similaire au cas du "a" ci-dessus, sauf que sr peut être une liste vide :
Calculons sr, l'endroit désigné par sx3 relativement à "c" dans x3 : soit sr tq sx3 = scf +ll $L[0b,1b] +ll sr (remarque 1 : $L[0b,1b] est l'endroit du premier "c" dans "(a c) (b c)").
Calculons l'endroit dans x2 correspondant à sx3 dans x3 : sx2 = scf +ll $L[1b] +ll sr
Soit l et s tq Trace c1 x s sx2 l = 1b.
On définit Trace c x s sx3 l = 1b
- à l'intérieur de "b c" : on a alors les sous-cas sur l'endroit désigné :
- "b c" : ici il y a création d'une nouvelle formule, on reprend la trace du distribute en indiquant la création dans le chemin de calcul par l'ajout de "1b".
Soit l et s tq Trace c1 x s sce l = 1b.
On définit Trace c x s sx3 (l +le 1b) = 1b.
- strictement à l'intérieur de b : similaire au cas du "a" ci-dessus :
Calculons sr, l'endroit désigné par sx3 relativement à "b" dans x3 : soit sr tq sx3 = scf +ll $L[1b,0b] +ll sr (remarque 1 : $L[1b,0b] est l'endroit de "b" dans "(a c) (b c)"; remarque 2 : sr n'est pas la liste vide).
Calculons l'endroit dans x2 correspondant à sx3 dans x3 : sx2 = scf +ll $L[0b,1b] +ll sr
Soit l et s tq Trace c1 x s sx2 l = 1b.
On définit Trace c x s sx3 l = 1b
- à l'intérieur de c : similaire au cas du "a" ci-dessus, sauf que sr peut être une liste vide :
Calculons sr, l'endroit désigné par sx3 relativement à "c" dans x3 : soit sr tq sx3 = scf +ll $L[1b,1b] +ll sr (remarque 1 : $L[1b,1b] est l'endroit du deuxième "c" dans "(a c) (b c)").
Calculons l'endroit dans x2 correspondant à sx3 dans x3 : sx2 = scf +ll $L[1b] +ll sr
Soit l et s tq Trace c1 x s sx2 l = 1b.
On définit Trace c x s sx3 l = 1b

Définition de "traces égales jusqu'au niveau n"

Soit t et u les traces de deux calculs sur une même formule et n∈ℕ. On dit que t et u sont égales jusqu'au niveau n ssi la restriction de t et u sur les NFSFP d'arrive de niveau ≤n est identique.

Définition de "traces compatibles au niveau n"

Soit t et u les traces de deux calculs sur une même formule et n∈ℕ. On dit que t et u sont compatibles au niveau n ssi les couples de NFSFP — où les NFSFP d'arrivée sont de niveau n — sont égaux.

Fonction d'unification des calculs

Soit x une formule de départ et c,d deux calculs valides sur x.

On cherche à définir acf et adf tq Trace (c +ll acf) = Trace (d +ll adf). Pour cela on procède par récurrence sur les NFSFP les plus courtes jusqu'aux plus grandes (donc de la formule globale aux sous-formules les plus profondes). Donc pour n∈ℕ on définira ac n et ad n qui seront les calculs ajoutés pour faire correspondre les Traces sur les NFSFP de départ de longueur ≤n.

En plus de définir ac et ad nous démontrerons en même temps la propriété suivante qui signifie que quand on a joint les calculs jusqu'au niveau n alors les endroits au niveau n+1 correspondent même s'il ne contiennent pas les mêmes calculs :

Soient
- xc n = calculate loose x \ c +ll ac n
- xd n = calculate loose x \ d +ll ad n
- sa un NFSFP de longueur n+1 valide sur xc n
alors
- sa est un SFP valide pour xc n
- Soit ss et lc tq Trace (c +ll ac n) x ss sa lc = 1b, alors il existe ld tq Trace (c +ll ad n) x ss sa ld = 1b

Cas n = 0

Nous allons définir ac 0 et ad 0, c'est à dire les calculs à ajouter à respectivement c et d de sorte que les calculs sur la formule globale elle-même soient les mêmes.

Soilt lc,ld tq Trace c x ∅l ∅l lc = 1b et Trace d x ∅l ∅l ld = 1b. lc et ld sont des listes de 0b.
Soit lm la plus grande des deux listes.
Soit lcd tq lm = lc +ll lcd.
Soit ldd tq lm = ld +ll ldd.

On définit :

- ac 0 = la liste lcd où l'on remplace les 0b par des ∅l.
- ad 0 = la liste ldd où l'on remplace les 0b par des ∅l.

On voit que l'on a Trace (c +ll ac 0) x ∅l ∅l lm = 1b et Trace (d +ll ad 0) x ∅l ∅l lm = 1b.

Cas n > 0

Soit n∈ℕ, supposons que les relations Trace des deux calculs (c +ll ac n et d +ll ad n) soient égales sur les NFSFP d'arrivée de niveau ≤ n.

Il nous faut : la liste des NFSFP de niveau n+1 est la même pour les deux calculs.

Soit ls la liste des NFSFP de niveau n+1 sur les formules d'arrivées des deux calculs.

Il nous faut : les listes des chemins de calcul des NFSFP de niveau n+1 des deux calculs sont compatibles (la plus courte est le début de l'autre) pour les NFSFP identiques. Et aussi que dans les chemins de calculs la partie de liste qui dépasse est constitué de 0b.

À détailler : On définit ac (n+1) et ad (n+1) par les NFSFP de niveau n+1 manières à ce que les chemins de calculs soient identiques.

Démonstration

Nous allons prouver que :

  • La récursion de la définition de la fonction d'unification est finie.
  • Les traces des calculs unifiés sont identiques.
  • Si deux calculs ont les mêmes traces alors les résultats sont identiques.

À détailler.

Essai 12

Contexte

On reprend l'essai 11 car en cours je me suis apperçu que la définition des calculs loose était trop large et qu'il fallait que le SFP ne soit pas un SFP fonction.

Propriétés sur les calculs

Quand une sous-formule peut apparaître lors d'un calcul ?

Seul un calcul élémentaire sur un distribute peut faire apparaître des sous-formules. "distribute a b c" fait apparaître deux sous-formules : "a c" et "b c".

Quand une sous-formule peut disparaître lors d'un calcul ?

Quand on exécute le calcul élémentaire sur "if a b c" on fait disparaître les sous-formules "if a b", "if a", "if", "a" et suivant la valeur de a, "b" ou "c".
Quand on exécute le calcul élémentaire sur "distribute a b c", on fait disparaître les sous-formules "distribute a b", "distribute a" et "distribute".

Représenter les calculs

Nous voulons représenter le calcul c sur une certaine formule x par une relation Trace c x prenant en arguments :

  • un SFP de la formule de départ
  • un SFP de la formule résultante du calcul
  • le nombre de calculs élémentaires effectués sur ce SFP au cours du calcul (ce peut être zéro)

Un calcul élémentaire ne doit apparaître au plus qu'une fois dans la relation Trace. Par exemple si on calcul if (if 1b 1b 1b) 0b 1b , le calclul interne de if 1b 1b 1b ne doit apparaître que comme calcul sur la formule globale (puisqu'il faut calculer la condition du if global pour calculer la formule globale).

Un calcul élémentaire n'apparait pas dans la relation Trace ssi ce calcul était inutile (sans conséquence sur le résultat du calcul). Par exemple le calcul de if 0b (if 1b 1b 1b) 1b peut passer par le calcul de la sous-formule if 1b 1b 1b, qui est inutile si on calcul après la formule globale car la sous-formule calculée disparait.

Remarque: si on calcul x1 x2 x2 x3 en commençant par calculer x2, puis x1. Alors si le résultat du calcul de x1 est "if", on ne sait qu'à posteriori que x2 étant calculé en tant que condition d'un if. Donc pour définir la relation Trace il faut commencer par examiner la fin du calcul et réinterpréter éventuellement des calculs précédent comme calcul plus global.

Quand le dernièer calcul élémentaire est un "if" :

Le calcul de la condition dans les calculs antérieurs doit être intégré (et compté) au calcul du if. On doit aussi reprendre l'argument retourné.

Quand le dernier calcul élémentaire est un "distribute" :
On doit aussi reprendre les arguments retourné (4 entrées à ajouter à Trace).

Tracer les calculs sur les sous-formules apparues :

Si un calcul commence par le calcul élémentaire "distribute a b c", puis que l'on fait un calcul sur la sous-formule "a c" alors ce derniier calcul n'est pas pris en compte par Trace car il n'y a pas de sous-formule correspondante dans la formule de départ.

Définition de Trace

Définition de Trace sur un calcul vide

Pour tout SFP sx pointant sur x entier ou se terminant par 1b, les seuls relations sont Trace c x sx sx ∅l

Définition de Trace sur un calcul de longueur n+1

On suppose que l'on a défini Trace c1 x où c1 est de longeur n. Soient :

  • y1 = calculate loose c1 x,
  • cy1 un SFP valide en tant que calcul élémentaire sur y1
  • c2 = c1 +le cy1
  • y2 = calculate loose c2 x.
  • sx un SFP sur x
  • sy2 un SFP sur y2

Nous allons chercher à définir Trace c2 x pour sx et sy2.

Si cy1 n'est pas le début de sy2 et sy2 n'est pas le début de cy1 :

On est dans le cas où la sous-formule de chemin sy2 n'est ni dans le calcul ni modifiée par le calcul cy1.
Donc la relation Trace c2 x sx sy2 = Trace c1 x sx sy2
Si cy1 = sy2 :
On est dans le cas où sy2 est l'emplacement du résultat du calcul.
Si il existe l tq l'on ait Trace c1 x sx sy2 l :
On est dans le cas où il y a une relation de calcul pour c1 entre l'emplacement de départ sx et l'emplacement d'arrivé sy2. Hors le calcul cy1 à l'emplacement sy2 laissera son résultat à cet emplacement, donc on aura une relation de calcul pour c2 entre sx et sy2.
Donc on aura Trace c2 x sx sy2 (l +le 0b)
Si

Si on a pour un certain k Trace c1 x sx sy2 k, alors on a Trace c2 x sx sy2 (k+1),
sinon pour tout k on n'a pas de relation Tracec2 x sx sy2 k.
Si cy1 est le début de sy2 :
Dans ce cas sy2 est le chemin d'une partie du résultat du calcul élémentaire cy1.

Essai 11

Contexte

On reprend l'idée de l'essai 10 mais en changeant les règles des calculs. Car le système fonctionne en formalisant et représentant les différents calculs, hors pour représenter le calcul de x1 x2 qui après calcul de x1 devient distribute a b x2, il faut associer les calculs de x1 x2 permettant d'arriver à distribute a b x2.

Définition des calculs

On reprend l'idée du calcul univocal, mais associé à un certain SFP. Remarquons qu'un calcul univocal élémentaire n'a pas besoin de spécifier la règle à appliquer, car elle se déduit de la formule. On garde les deux définitions des calculs (loose et univocal), le calcul loose a les mêmes règles mais donne en plus le choix de la sous-formule calculée. Remarquons que deux calculs loose identiques peuvent s'écrire différemment car le calcul de la condition de if (if 1b 1b 1b) 0b 1b peut être vu comme un calcul sur la formule globale ou comme un calcul localisé à la condition.

Représenter les calculs

Nous voulons représenter le calcul c sur une certaine formule x par une relation Trace c x prenant en arguments :

  • un SFP de la formule de départ
  • un SFP de la formule résultante du calcul
  • le nombre de calculs élémentaires effectués sur ce SFP au cours du calcul (ce peut être zéro)

Un calcul élémentaire ne doit apparaître au plus qu'une fois dans la relation Trace. Par exemple si on calcul if (if 1b 1b 1b) 0b 1b , le calclul interne de if 1b 1b 1b ne doit apparaître que comme calcul sur la formule globale (puisqu'il faut calculer la condition du if global pour calculer la formule globale).

Un calcul élémentaire n'apparait pas dans la relation Trace ssi ce calcul était inutile (sans conséquence sur le résultat du calcul). Par exemple le calcul de if 0b (if 1b 1b 1b) 1b peut passer par le calcul de la sous-formule if 1b 1b 1b, qui est inutile si on calcul après la formule globale car la sous-formule calculée disparait.

Remarque: si on calcul x1 x2 x2 x3 en commençant par calculer x2, puis x1. Alors si le résultat du calcul de x1 est "if", on ne sait qu'à posteriori que x2 étant calculé en tant que condition d'un if. Donc pour définir la relation Trace il faut commencer par examiner la fin du calcul et réinterpréter éventuellement des calculs précédent comme calcul plus global.

Quand le dernièer calcul élémentaire est un "if" :

Le calcul de la condition ainsi que le calcul de la partie fonction "if a b" doivent être ignorés dans les calculs antérieurs puisqu'ils sont intégrés au calcul du if.

Quand le dernier calcul élémentaire porte sur la partie (x1) fonction d'une sous-formule (x1 x2) :

Alors on doit l'exprimer comme calcul sur x1 x2.
Remarques :
- Cette règle se superpose aux autre règles.
- Par récursivité de la construction de Trace , on est assuré que l'on n'a pas de relation Trace sur une sous-formule qui est la fonction d'une sous-formule.

Quand le dernièer calcul élémentaire est un "distribute" :

Le calcul de la partie fonction "distribute a b" doit être ignoré dans les calculs antérieurs puisqu'ils sont intégrés au calcul du distribute.

Simplifier la représentation des calculs loose

La section précédente me suggère que la définition du calcul loose pourrait peut être être restreinte pour éviter les formulations multiples d'un même calcul.

Pour éviter les expressions équivalentes d'un calcul loose on peut demander à ce que le SPF porte sur une sous-formule qui n'est pas une fonction.

Il reste que si on calcul la condition d'un if, on peut le voir ou non comme le calcul du if, ce qui n'est pas évident car au stade où l'on calcul la condition on n'a pas forcément connaissance que c'est un if.
Peut-on alors exiger d'ordoner l'ordre des calculs de sorte que si on calcul un argument cela implique que l'on ne calculera pas la fonction après ou que le calcul de la fonction est terminé ? Non car on ça deviendrait très compliqué, par exemple ajouter un calcul élémentaire à un calcul pourrait le rendre invalide.

Propriétés sur les calculs

Quand une sous-formule peut apparaître lors d'un calcul ?

Seul un calcul élémentaire sur un distribute peut faire apparaître des sous-formules. "distribute a b c" fait apparaître deux sous-formules : "a c" et "b c".

Quand une sous-formule peut disparaître lors d'un calcul ?

Quand on exécute le calcul élémentaire sur "if a b c" on fait disparaître les sous-formules "if a b", "if a", "if", "a" et suivant la valeur de a, "b" ou "c".
Quand on exécute le calcul élémentaire sur "distribute a b c", on fait disparaître les sous-formules "distribute a b", "distribute a" et "distribute".

Propriétés de la relation Trace

Ces propriétés sont à démontrer.

Si deux calculs partant de la même formule ont des relations Trace identiques alors le résultat est identique.

Définition de Trace

Définition de R0 et R1

Pour x une formule et sc un SFP sur x où l'on peut opérer un calcul élémentaire, on définit les relations suivantes sur sx un SFP de x et sy un SFP du résultat du calcul :
On définit les relations :
- R0 sc x sx sy : ssi sy est une copie dans le résultat de l'emplacement sx de x.
- R1 sc x sx : ssi sx est l'emplacement d'un calcul élémentaire "if 1b", "if 0b" ou "distribute" engendré par sc (remarque: on peut avoir sc ≠ sx, par exemple avec "if (if 1b 1b 1b) 0b 1b" où on peut avoir sc = $L[] et sx = $L[0b,0b,1b] ).

Définition de Trace sur un calcul vide

Pour tout SFP sx sur x, les seuls relations sont Trace c x sx sx 0

Définition de Trace sur un calcul de longueur n+1

On suppose que l'on a défini Trace c1 x où c est de longeur n. Soient :

  • y1 = calculate loose c1 x,
  • cy1 un SFP valide en tant que calcul élémentaire sur y1
  • c2 = c +le cy1
  • y2 = calculate loose c2 x.
  • sx un SFP sur x
  • sy2 un SFP sur y2

Nous allons chercher à définir Trace c2 x pour sx et sy2.

Si cy1 n'est pas le début de sy2 et sy2 n'est pas le début de cy1 :

La sous-formule de chemin sy2 n'est ni dans le calcul ni modifiée par le calcul cy1. Donc la relation Trace c2 x sx sy2 = Trace c2 x sx sy1
Si cy1 = sy2 :
Si on a pour un certain k Trace c1 x sx sy2 k, alors on a Trace c2 x sx sy2 (k+1),
sinon pour tout k on n'a pas de relation Tracec2 x sx sy2 k.
Si cy1 est le début de sy2 :
Dans ce cas sy2 est le chemin d'une partie du résultat du calcul élémentaire cy1.

Essai 10

Contexte

On explore la deuxième idée expliquée dans l'essai 9 : reprendre l'essai 6 en corrigeant les erreurs. Donc on part des sous-formules ne subissant pas de sous-calculs stricts pour remonter aux plus gros calculs.

Le problème du traçage

On peut suivre une sous-formule a à travers un calcul, mais on ne peut pas faire correspondres les différentes duplications d'un calcul à l'autre. Par contre on peut prendre le nombre maximal de calculs subit par les différentes duplications de la sous-formule et ajouter les calculs pour que toutes les duplications de a soient l'objet du même nombre de calculs.
a peut disparaitre par un calcul "if", dans ce cas il n'y a plus à s'en occuper.
Si a se calcule en $F[ distribute ] +f b +f c , il peut après (par un autre distribute qui lui donne un argument) disparaître dans le calcul de $F[ distribute ] +f b +f c +f d. De même si a = $F[ if ] +f b +f c. Est-ce un problème ?

On peut attribuer un niveau aux sous-formules pour les hiérarchiser :
- une formule présente au départ et jamais calculée dans aucunne de ses duplications aura un niveau 0.
- une formule existant avant aura un niveau plus faible qu'une formule apparaissant après
- une formule contenant une sous-formule calculée aura un niveau supérieur à la sous-formule calculée

Relations R1

Soient sc un calcul loose élémentaire (c'est un SFP), x et y deux formules tq y = calculate loose sc y. Soient sx et sy des SFP de x et y. On aura sx R1 sy ssi on a la disjonction :

- le calcul c copie le contenu de sx en sy
- sx = sy et le calcul c réalise un calcul élémentaire de la formule en sx (les calculs élémentaire se réalise à un endroit fixé).

Remarques :

- Une copie peut se réaliser de différentes manières :
- il n'y a pas de calcul à cet endroit, et on aura alors sx = sy
- "if 1b" ou "if 0b" copie la sous-formule réaliser, dans ce cas sx ≠ xy
- distribute a b c copie a, b et c (copie double pour c)
- Pour un même calcul élémentaire, on pourra avoir plusieurs relations R1, par exemple "if (if 1b 1b 1b) 0b 1b" peut être vue comme un calcul élémentaire sur la formule globale mais aussi comme un calcul élémentaire sur la condition, les deux manièrs de voire se traduirons en relations R1.

Remarque:

  • si sc est le début de sx : sx est un endoit qui est à l'intérieur d'un calcul.
  • si sx est le début de sc : le calcul est à l'intérieur de l'endroit pointé par sc.
  • si sx n'est pas le début de sc et sc n'est pas le début de sx : le calcul est en dehors de l'endroit pointé par sx (et donc on a sx R1 sx).

On a R1 x sc sx sy ssi on a la disjonction :

  • si sx n'est pas le début de sc et sc n'est pas le début de sx et sx = sy
  • si sc est le début de sx. Soit st tq t = s +ll st :
    • si s pointe sur une formule de la forme $F[if 0b] +f a +f b :
      • si st commence par $L[ 1b] et si u = s +ll listTail st
    • si s pointe sur une formule de la forme $F[if 1b] +f a +f b :
      • si st commence par $L[ 0b, 1b ] et si u = s +ll listTail \ listTail st
    • si s pointe sur une formule de la forme $F[distribute] +f a +f b +f c et si on a la disjonction :
      • (cas du c) si st commence par $L[1b] et si u = s +ll $L[ 0b, 1b] +ll listTail st ou u = s +ll $L[ 1b, 1b] +ll listTail st
      • (cas du b) si st commence par $L[0b,1b] et si u = s +ll $L[ 1b, 0b] +ll listTail \ listTail st
      • (cas du a) si st commence par $L[0b,0b,1b] et si u = s +ll $L[ 0b, 0b] +ll listTail \ listTail \ listTail st

Relations pour tracer les copies et les calculs

Relations R1

Cette relation définie les relations de copie entre SFP pour un calcul élémentaire sur une certaine formule. C'est à dire que pour un certain calcul élémentaire, une certaine formule, on reliera un SFP sur la formule de départ avec un SFP sur la formule d'arrivée ssi le calcul engendre une copie du contenue du premier SFP sur le second (et donc les deux sous-formules pointées seront égales). La copie peut avoir deux origines : cette partie de la formule n'est pas affectée par le calcul ou le calcul engendre une copie (par exemple le calcul de "if 1b a b" engendre une copie de a, le calcul de "distribute a b c" engendre entre autres une double copie de c).

Soient :

Remarque:

  • si t est le début de s : t pointe sur un endroit dont le contenu sera changé par le calcul
  • si s est le début de t : t pointe à l'intérieur de la sous-formule calculée, donc cette partie peut disparaitre ou être copiée suivant le calcul.
  • si s n'est pas le début de t et si t n'est pas le début de s : les deux sous-formules pointées n'ont pas de parties communes.

On a R1 x s t u ssi on a la disjonction :

  • si s est le début de t. Soit st tq t = s +ll st :
    • si s pointe sur une formule de la forme $F[if 0b] +f a +f b :
      • si st commence par $L[ 1b] et si u = s +ll listTail st
    • si s pointe sur une formule de la forme $F[if 1b] +f a +f b :
      • si st commence par $L[ 0b, 1b ] et si u = s +ll listTail \ listTail st
    • si s pointe sur une formule de la forme $F[distribute] +f a +f b +f c et si on a la disjonction :
      • (cas du c) si st commence par $L[1b] et si u = s +ll $L[ 0b, 1b] +ll listTail st ou u = s +ll $L[ 1b, 1b] +ll listTail st
      • (cas du b) si st commence par $L[0b,1b] et si u = s +ll $L[ 1b, 0b] +ll listTail \ listTail st
      • (cas du a) si st commence par $L[0b,0b,1b] et si u = s +ll $L[ 0b, 0b] +ll listTail \ listTail \ listTail st
  • si s n'est pas le début de t, t n'est pas le début de s et t = u (cas d'une partie non calculée)

Relations R

Cette relation étend R1 par transitivité aux calculs (non élémentaires) et en plus ajoute la notion de nombre de calcul, c'est à dire que 0 représente une copie, 1 représente un seul calcul opéré sur la sous-formule etc.
Ainsi par le calcul de R on aura entre la formule de départ et le résultat du calcul toute les relations de copie et de calcul.

Soient:

  • x une formule
  • l un calcul du langage "libre" (c'est une liste de SFP)
  • t un SFP valide pour x
  • y = calculate loose l x
  • u un SFP valide pour y
  • n est un entier naturel (le nombre de calcul sur la formule)

On définir R récursivement sur la longeur de l:

Si l est vide :

On a R x l t u n ssi t = u et n = 0

Si l n'est pas vide :

Soient
- s = listHead l
- lt = listTail l
- x2 = calculate loose $L[s] x
On a R x l t u n ssi on a la disjonction :
- (cas où la sous-formule pointée par t est calculée) si s = t et R x2 lt t u (n-1)
- (cas où la sous-formule pointée par t est copiée) si il existe t2 tq R1 x s t t2 et R x2 lt t2 u n

Remarquons que les sous-formules apparaissant lors du calcul ne sont pas prise en compte par R.
Par exemple si x = distribute a b c, l = $L[], on aura entre autres :

  • R x l $L[] $L[] 1
  • R x l $L[1b,0b]
$L[0b,1b,b0] 0
mais on n'aura rien de la forme R x l * $L[0b] * car (a c) ne provient ni d'un calcul et n'est pas le résultat d'un calcul.

Propriétés sur les calculs

Pourquoi une formule peut apparaître lors du calcul ?

Si on considère que les copies et les résultats des calculs élémentaires ne sont pas des apparitions, que reste-t-il ?
Le if ne produit pas de nouvelle formule. distribute a b c produit (a c)(b c) soit deux nouvelles formules (a c et b c).

Méthode pour unifier les calculs

Soit E0 = l'ensemble des sous-formules présentes en x, n'ayant subit aucun calcul ou sous-calcul et apparaissant dans au moins l'un des résultats des deux calculs.
Pour n un entier naturel, si En est défini, soit En+1 l'ensemble des sous-formules présentes en x, ayant toutes ses sous-formules dans En et apparaissant dans au moins l'un des résultats des deux calculs.

On peut unifier les calculs sur les E1 puis E2 etc (à démontrer).

On peut donc supposer ∀n∈ℕ les sous-formules sont identiques dans y et z.

Soit y1 une sous-formule de y. Si ∀n∈ℕ y1∉En alors y1 provient d'une sous-formule du résultat d'un distribute. Donc le résultat y2 de ce distribute se trouve dans y (puisqu'y1 s'y trouve). On peut alors recommencer sur y2, si ∀n∈ℕ y2∉En alors y2 provient d'une sous-formule du résultat d'un distribute. On voit que par récurrence on arrive à une sous-formule de x et donc pour un certain k∈ℕ et n∈ℕ yk∈En.

Essai 9

Contexte

L'essai 8 fonctionne bien pour les calculs ayant en premier calcul global un if, mais pas pour un distribute, car pour ce cas il y a des interactions entre les différentes sous-parties de la formule. Je vois deux solutions à ce problème :

  1. Étendre l'hypothèse de récurrence pour que la méthode de l'essai 8 fonctionne.
  2. Reprendre l'essai 6 en corrigeant les erreurs.
Nous allons explorer ici l'idée de solution 1.

L'hypothèse étendue

Soit x,y tq

  • x →c+= x1
  • x →c+= x2
  • y →c+= y1
  • y →c+= y2
  • x1 +f y1 →c+= xy1
  • x2 +f y2 →c+= xy2

alors

il existe t tq

  • xy1 →c+= t
  • xy2 →c+= t

En quoi l'hypothèse est utile ?

Avant le calcul glogal "distribute" , la formule de départ peut s'écrire x +f y et comme il n'y a pas de calcul global, il y a un calcul sur la partie fonction (x) et la partie argument (y). Donc avant la déduction "distribute" on a des formules x1 +f y1 et x2 +f y2.

Je trouve que l'hypothèse ne marche pas, de toute manière la suite du calcul (x1 +f y1 →c+= xy1 etc) est un cas plus général de la première partie (x →c+= x1 etc) qui n'a donc pas d'intérêt.

Essai 8

Contexte

L'idée de l'essai 7 n'est pas bonne car deux calculs peuvent être équivalent et ne pas avoir les mêmes calculs globaux. Par exemple si on 1-calcul l'argument puis on fait un 1-calcul global "if 0b", cela est équivalent à faire d'abord un 1-calcul global "if 0b" puis un 1-calcul global.

On reprend les définitions de l'essai 7.

La nouvelle idée est de faire une récurrence sur la taille des calculs en trouvant des équivalents en réduisant les calculs par le début. Par exemple un calcul qui commence par un "if 0b" revient au calcul moins ce premier 1-sur-calcul et portant sur l'argument. Nous allons donc chercher à faire des réductions dans tous les cas.
Pour cela nous aurons besoin :

  • de vérités sur les calculs pour prouver par exemple que le premier 1-sur-calcul global le même dans les deux calculs.
  • de définir une représentation des 1-sous-calculs en utilisant les chemins associé à un identifiant d'un des 3 1-sur-calculs.

L'hypothèse de récurrence

On l'indexe sur la taille maximale des calculs et la profondeur de la formule.

L'algorithme

La s'interesse au premier 1-calcul global et on divise en différent cas. On transforme les calculs de sorte à pouvoir utiliser l'hypothèse de récurrence, puis on utilise la conclusion obtenue par l'hypothèse de récurrence pour ajouter les calculs nécessaires pour aboutir à une formule identique pour les deux calculs.

- Si les deux calculs n'ont aucun 1-sur calcul global :

Alors on peut diviser chacun des deux calculs suivant que le calcul porte sur la partie fonction ou la partie argument. On obtient alors un index plus petit et on peut donc appliquer la récurrence. Pour utiliser le résultat de la récurrence, on transforme les calculs ajoutés pour les relativiser à la formule à calculer.
- Si l'un des calculs a en premier 1-sur-calcul global un "if 0b" :
Si l'autre a un 1-sur-calcul global :
Alors d'après un théorème à préciser les deux on pour premier 1-sur-calcul global la même règle "if 0b". On transforme les deux calculs ainsi:
Le calcul portera sur l'argument de la formule calculée. Avant les if global, on ne garde que les calcul sur l'arguments mais en les transformant en calcul global. On élimine le calcul du if global. Après le if global on garde les calculs tels quels.
On obtient ainsi deux calculs plus courts et on peut donc appliquer la récurrence. On obtient donc une formule t et des calculs ajouté, que l'on peut directement utiliser sur les calculs de départ et ainsi obtenir la conclusion.
Si l'autre n'a pas de 1-sur-calcul global :
On transforme le calcul comportant un 1-sur-calcul global comme dans le cas précédent, on transforme celui sans 1-sur-calcul global en ne premant que les calculs sur l'argument. On obtient deux calculs d'index plus petits sur l'argument de la formule. On peut donc appliquer l'hypothèse de récurrence.
Pour produire les calculs à ajouter aux calculs de départ :
Pour le calcul contenant le 1-sur-calcul "if 0b", on ajoute les calculs ajoutés, pour l'autre on ajoute le calcul "if 0b" (il faut éventuellement ajouter d'abord les calculs de la fonction puis de la condition) puis on ajoute les calculs ajoutés.
- Si l'un des calculs a en premier 1-sur-calcul global un "if 1b" :
Si l'autre a un 1-sur-calcul global :
Alors d'après un théorème à préciser les deux on pour premier 1-sur-calcul global la même règle "if 1b".
La formule calculée sera la partie fonction de x. On transforme les calculs avant le 1-calcul global en calculs sur la partie fonction (on élimine les calculs dont le chemin commence par 1b et pour les autres on élimine le premier 0b). On élimine le calcul "if 1b". On transforme les 1-calculs suivant le "if 1b" en calculs sur la partie argument de la partie fonction (on ajoute 1b à tous les chemins).
On obtient donc des calculs plus petits, on peut donc appliquer la récurrence. Les calculs ajoutés provenant de la récurrence ne comportent pas de calculs globaux car ils portent sur une formule de départ de la forme "if 1b a".
Pour produire les calculs à ajouter aux calculs de départ :
On transforme les calculs ajoutés en relativisant à l'argument (on enlève le 1b des chemins).
Si l'autre n'a pas de 1-sur-calcul global :
On transforme les deux calculs ainsi :
On transforme le calcul comportant un 1-sur-calcul global comme dans le cas précédent. On transforme l'autre calcul en ne prenant que les calculs de la partie fonction et en les remontant au parent (on enlève le 0b et on élimine les calculs commençant par 1b).
On peut alors appliquer la récurrence, la formule calculée étant la partie fonction de x.
Pour produire les calculs à ajouter aux calculs de départ :
On transforme les calculs ajoutés suivant le calcul : pour le calcul avec un 1-sur-calcul global on fait comme dans le cas précédent. Pour l'autre on ajoute le calcul "if 1b" (il faut éventuellement ajouter d'abord les calculs de la fonction puis de la condition) puis on ajoute les calculs ajoutés en enlevant le premier 1b des chemin.
Si l'un des calculs a en premier 1-sur-calcul global "distribute" :
Si l'autre a un 1-sur-calcul global :
Alors d'après un théorème à préciser les deux on pour premier 1-sur-calcul global la même règle "distribute".

Essai 7

Contexte

L'essai 6 est intéressant pour sa représentation en chemin, mais la récurrence proposée, partant des sous-formules les plus "petites" ne fonctionne pas car tant que les calculs sur les sous-formules les plus grosses ne sont pas exécutés on n'a pas la disposition finales pour les petites formules. Et comme les petites sous-formules peuvent être calculées différemment après duplication, on ne peut pas savoir comment les calculer avant. Il faut donc commencer par les sous-formules les plus grosses (dont la formule globale). Mais alors il faut montrer que, malgrer les sous-calculs éventuels préalables, la formule plus grosse se calcule pareil. Il faut probablement élargir l'hypothèse de récurrence.

Algorithme

On décrit ici l'algorithme qui définit les calculs à ajoutés aux deux calculs pour obtenir le même résultat.

  1. On part de la formule globale et on ajoute pour chaque calcul, le nombre de calcul — par les règles if ou distribute — de sorte que le nombre de ces calculs soit le même pour les deux calculs . Pour se faire on doit aussi faire les sous-calculs (de l'argument du if ou de la partie fonction) nécessaires au calcul global.
  2. On refait alors le 1. pour la partie fonction et la partie argument.

Si on a le théorème suivant :

Soit x une formule et deux sous-calculs qui ont le même nombre de calculs globaux par les règles if ou distribute. Alors on a l'égalité structurelles entre les deux résultats des calculs. a =s b est défini par la disjonction :
  • a = b
  • a et b sont des applications et on a a1 =c b1 et a2 =c b2
alors on peut par récurrence construire l'union des deux caculs ainsi que le résultat du calcul. Mais il faut prouver que la récurrence est finie, car comme les sous-formules sont modifiées à chaque étape, on pourrait construire une formule infinie. Peut-être que l'on peut prouver la finitude en ajoutant dans le théorème que les calculs des parties sont de taille plus petite que le calcul global duquel on a éliminer les calculs sur la formule globale.

Pour cette solution, il faut définir un calcul plus réduit que le 1-sur-calcul où il n'y a que les règles if et distribute.

Théorème de jonction des calculs globalement identiques

Nous voyons que nous avons besoin d'un théorème qui est le coeur de la démonstration.

Essai 6

Contexte

On part sur de nouvelles idées.

Les chemins

On identifie les sous-formules par un chemin. Un chemin est une liste binaire finie, qui peut être vide. La liste vide identifie la formule globale, chaque élément de la suite sélectionne la partie fonction (0b) ou argument (1b).
Représentons ici dans le contexte d'une formule le contenu par le chemin, par exemple $C[ 0b, 1b] est la sous-formule argument de la fonction de la formule globale.
On peut représenter les 3 instructions par des transformations qui remplacent la formule concernée par :

  • instruction "if 1b" : $C[ 0b, 1b ]
  • instruction "if 0b" : $C[ 1b ]
  • instruction "distribute" : ($C[ 0b, 0b, 1b] +f $C[ 0b, 1b]) +f ($C[ 0b, 0b, 1b] +f $C[ 1b])

Récurrence

Il nous faut ajouter des calculs aux deux calculs existant pour obtenir un résutat identique.

  1. Pour cela on procède à partir des sous-formules les plus petites qui ne sont pas l'objet d'un calcul ou sous-calcul dans les deux calculs. Elles sont donc uniquement soit détuites ou copiées (en un ou multiples exemplaires).
  2. Puis on traite les sous-formules qui sont l'objets de calculs mais pas de sous-calculs. Pour une sous-formule particulière, on peut caractériser les calculs appliqués par le nombre de ces calculs car il n'y a pas de choix du calcul appliqué. On fait alors en sorte que de chaque côté, et pour toutes les copies, le même nombre de calculs soit appliqués.
  3. Puis on traite le niveau au dessus, c'est à dire les sous-formules qui ont des sous-calculs de niveau 1. Comme on a égaliser les valeurs des sous-formules de niveau 1, les formules de niveau 2 sont devenus identiques et on les caractérise aussi par le nombre de calculs globaux.

Il y a un problème ? dans la récurrence décrite ci-dessus car il peut y avoir un calcul global sur une sous-formule, suivit par un calcul sur une de ses sous-formules, suivit par un autre calcul global.

Essai 5

Contexte

L'idée est de séparer le problème par la taille de la formule concernée car le calcul des sous-formules ne change pas la forme globale de la formule sur laquelle elle porte.

Il y a des erreurs dans la suite :
On doit d'abord montrer que, peu importe les sous-calculs, ils aboutirons à la même fonction minimale et le même nombre d'arguments. Pour cela on peut montrer que si x →c+= y et x →c+= z où y et z sont des mots, alors y = z.
On peut montrer que si les deux calculs ont des calculs globaux alors ce sont les mêmes 1-calculs dans le même ordre et on montre que les arguments et la fonction minimales sont deux à deux égaux par calcul. On peut redéfinir l'égalité structurelle ainsi, x =s y ssi on a la disjonction :

- x = y
- x et y sont des applications respectivement x1 +f x2, y1 +f y2 et on a x1 =c y1 et x2 =c y2.
On peut alors exprimer la vérité ci-dessus ainsi : si x →c+= y et x →c+= z et que les calculs ont le même nombre de calculs globaux alors x =s y.

Essai 4

Contexte

Je suis bloqué pour trouver comment unifier. L'idée de l'essai 4 est de chercher à prouver le théorème sur des calculs de longueur limité (0,1,2) pour trouver à généraliser.

Remarque préalable : les règles du 1-cacul sont exclusives. Si on connait la formule il suffit donc de savoir la partie de la formule qui est 1-calculée pour connaître le 1-calcul éxécuté.

Si la somme des longueurs des deux calculs est 0 ou 1

Trivial

Si chaque calcul est de longueur 1

On a les cas suivants :

  • Si les deux sont des 1-calculs sur la globalité de la formule : c'est le même calcul, donc cas trivial.
  • Si l'un est un calcul global et l'autre un sous-calcul :
    • Si le calcul global est un if : le sous calcul ne peut porter que sur les deux derniers arguments. On a les cas suivants :
      • le sous-calcul porte sur l'argument non retourné : l'union est pour l'un le calcul global, pour l'autre le sous-calcul puis le calcul global.
      • le sous-calcul porte sur l'argument retourné : l'union est
        • pour l'un le calcul global puis le sous-calcul de l'autre mais transformé en calcul global
        • pour l'autre, on ajoute le calcul global
    • Si le calcul global est un "distribute" : le sous-calcul porte sur l'un des 3 arguments. L'union est :
      • pour l'un le calcul global puis le sous-calcul, mais décalé à la nouvelle place de l'argument, et doublé si c'est le dernier argument (car le dernier argument est dupliqué)
      • pour l'autre on ajoute le calcul global
  • Si les deux sont des sous-calculs :
    • Si ils portent sur la même sous formule : c'est le même calcul, donc cas trivial.
    • Si ils portent sur des sous-formules séparées : comme il n'y a pas d'interaction, l'union des calculs consiste à ajouter à l'un le calcul de l'autre.
    • Si l'un porte sur une sous-formule de la portée de l'autre : on se trouve dans un cas similaire au cas du calcul global et d'un sous-calcul car on peut transposer

Essai 3

Contexte

Les points nouveaux par rapport à l'essai 2 :

  • Il faudrait redéfinir →c1+ de manière à ce qu'il n'y ait pas de doublon, pour cela il faut partir sur juste les 3 règles sans sous-calculs de →c1 et les règles de sous-calculs.
  • L'étape 3 décrite est quasi-impossible car comment réordonner sachant que le changement d'ordre change les calculs (avec même des disparitions).

Les idées

En ayant une formule à 1-calculer on pour décrire un calcul on n'est pas obliger de précier l'instruction du calcul à réaliser car il n'y a qu'une seule possibilité. Là c'est aussi le cas.

Un sous-calcul ne peut pas forcément être déplacé après un 1-calcul sur la formule globale, car il peut servir à calculer la condition d'un if ou la partie fonction de la formule globale.

On peut remarquer que pour unir les deux calculs ils faut qu'ils aient le même nombre de 1-calcul sur la formule entière.
Donc il faut ajouter à celui qui a le moins de 1-calcul blogaux, les calculs globaux manquant. Mais pour cela, il faut aussi ajouter les sous-calculs nécessaires à la réalisation des calculs globaux.

Méthode d'union :

  1. On réordonne les calculs suivant l'ordre des calculs sur les grandes parties de formule en premier
  2. On ajoute ce qui manque pour unifier les deux calculs
  3. On prouve que

Essai 2

Contexte

L'hypothèse de récurrence de l'essai 1 ne fonctionne pas car l'influence d'un 1-calcul se fait sur tout le calcul.

L'idée

On passe par les étapes suivantes:

  1. On réordonne les deux calculs de départ pour que les calculs plus petits (dans le sens que ça concerne une plus petite partie de la formule) soient après les plus grands.
  2. On fait l'union des calculs réordonnés , le résultat du calcul sera t, mais il reste à prouver y →c+= t et z →c+= t
  3. On réordonne l'union de deux manière différente pour que les calculs passe par y pour l'un des réordonnancement et z pour l'autre.

Pourquoi réordonner les calculs : un sous calcul peut s'avéré sans effet par un calcul plus global suivant. Réordonner permet de comparer facilement les calculs.

On voit qu'il nous faut un théorème sur le réordonnancement des calculs. Si on a un théorème sur l'inversion de deux 1-sous-calculs cela est une base suffisante pour réordonner les calculs.
Remarque 1 : l'inversion de deux 1-sous-calculs est indépendante du calcul dans lequel il est inclu.
Remarque 2 : l'inversion peut avoir comme résultat une suite de 1-sous-calculs de longueur différente de 2.

Exemples d'inversions entraînant des modifications:

1)
- 1-calcul c de l'argument
- 1-calcul "if 1b" global
devient :
- 1-calcul global "if 1b"
2)
- 1-calcul c de l'argument
- 1-calcul "if 0b" global
devient:
- 1-calcul global "if 0b"
- 1-calcul c global

Comment réaliser la phase 3 ?

Comme réordonner entraîne des modifications, le problème est que l'union ne contient pas forcément les 1-calculs des versions de départ.

Essai 1

Pour n∈ℕ, on définit l'hypothèse de récurrence P n =

si on a les conditions de l'énnoncé et Icp x y ≤ n et Icp x z ≤ n
alors il existe t tq y →c+= t et z →c+= t

Prouvons P 0

Icp x y = 0 ⇒ x = y, de même y = z. Donc x = y = z, donc on peut prendre pour y pour t et on a alors y →c+= t et z →c+= t.

Supposons P n et prouvons P (n+1)

@theorem