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 :

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

Définition de cb n et db n :

Définition de cbt n et dbt n :

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

• 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 :

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

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

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

Augmentation par distribute séparé ou non :

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

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

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 :

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 :

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

Définition de cb n et db n :

Définition de cbt n et dbt n :

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

• 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 :

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

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

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

Augmentation par distribute séparé ou non :

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

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

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 :

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 :

- Sinon :

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

Définition de cb n et db n :

Propriétés de la fonction "balancing"

Croissance des niveaux :

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 :

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

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

Présentation de la démonstration :

Définition de cb n et db n :

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

Augmentation par distribute séparé ou non :

Augmentation par distribute non-séparé :

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 :

- Sinon :

Propriétés de la fonction "balancing"

Croissance des niveaux :

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 :

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

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 :

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 :

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

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 ?

Théorème à démontrer :

- 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 s_1-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 :

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.

"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é.

"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é.

"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.

"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.

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

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) :

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 :

Ce choix pose des contraintes, par exemple :

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 ?

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

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

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

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é ?

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 ?

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

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

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

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

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

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 :

- Si sce est strictement interne à sx3 :
- Si w est "if" :
- Si w est "distribute" :

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 :

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 :

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" :

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 :

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 :

Si cy1 = sy2 :

Si cy1 est le début de sy2 :

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" :

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

Quand le dernièer calcul élémentaire est un "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 :

Si cy1 = sy2 :
Si cy1 est le début de sy2 :

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 ?

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 :

Remarques :

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 :

• x une formule
• s un calcul élémentaire du langage "libre" (c'est un SFP) valide pour x
• t un SFP valide pour x
• y = calculate loose $L[s] x
• u un SFP valide pour y

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 :

Si l n'est pas vide :

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 E₀ = 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 E_n est défini, soit E_n+1 l'ensemble des sous-formules présentes en x, ayant toutes ses sous-formules dans E_n et apparaissant dans au moins l'un des résultats des deux calculs.

On peut unifier les calculs sur les E₁ puis E₂ 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∉E_n 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∉E_n 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∈ℕ y_k∈E_n.

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 :

- Si l'un des calculs a en premier 1-sur-calcul global un "if 0b" :
- Si l'un des calculs a en premier 1-sur-calcul global un "if 1b" :

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 :

• 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.

0. 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).
1. 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.
2. 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 :

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:

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 =

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