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
- Si orderedCalc c = 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 :
Définition de cbt n et dbt n :
Définition de "sous-liste d'un arbre" :
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 :
Niveau des calculs équilibré et partie communes des arbres :
Implication d'un balancing à la récursivité infinie :
- l'arbre grandit indéfiniment
- une sous-liste de l'arbre devient infini et contient un nombre croissant de calculs.
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
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 :
- 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)
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
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
- Si orderedCalc c = 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 :
Définition de cbt n et dbt n :
Définition de "sous-liste d'un arbre" :
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 :
Niveau des calculs équilibré et partie communes des arbres :
Implication d'un balancing à la récursivité infinie :
- l'arbre grandit indéfiniment
- une sous-liste de l'arbre devient infini et contient un nombre croissant de calculs.
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
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 :
- 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)
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 :
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 :
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 :
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 :
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 :
- 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) :
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 :
- 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 :
- "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
- Sinon on retourne au début
- 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 ?
Théorème à démontrer :
- s1 et s2 deux SFP sur x disjoints
- c un calcul univocal sur x
alors il existe un k∈{0,1} et t un SFP des traces de sk tq :
- 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 :
Cette méthode s'appuie sur diverses propriétés comme :
- 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.
→ 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é.
→ 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 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.
→ 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.
→ 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.
→ 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) :
2) on parcourt les calculs élémentaires en échangeant deux calculs élémentaires si on a soit :
- 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 :
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 ?
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
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 ?
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 ?
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 :
Soit l et s tq Trace c1 x s sx3 l = 1b
On définit Trace c x s sx3 l = 1b
Soit l et s tq Trace c1 x s sx3 l = 1b
On définit Trace c x s sx3 l = 1b
- 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 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é.
On définit Trace c x s sx3 \ l +ll lc +ll $L[0b] +ll lr = 1b
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
- tenir compte du cas spécial de la nouvelle sous-formule "b c"
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
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
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
On définit Trace c x s sx3 (l +le 1b) = 1b.
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
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 :
- xd n = calculate loose x \ d +ll ad n
- sa un NFSFP de longueur n+1 valide sur 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 :
- 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" :
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 :
Donc la relation Trace c2 x sx sy2 = Trace c1 x sx sy2
Si il existe l tq l'on ait Trace c1 x sx sy2 l :
Donc on aura Trace c2 x sx sy2 (l +le 0b)
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) :
Remarques :
- 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" :
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 :
sinon pour tout k on n'a pas de relation Tracec2 x sx sy2 k.
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 ?
- 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 :
- 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 :
- "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)
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
- si s pointe sur une formule de la forme $F[if 0b] +f a +f b :
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 pointe sur une formule de la forme $F[if 0b] +f a +f b :
- 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 :
- lt = listTail l
- x2 = calculate loose $L[s] x
- (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]
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 :
- Étendre l'hypothèse de récurrence pour que la méthode de l'essai 8 fonctionne.
- Reprendre l'essai 6 en corrigeant les erreurs.
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 :
Pour produire les calculs à ajouter aux calculs de départ :
Pour produire les calculs à ajouter aux calculs de départ :
Pour produire les calculs à ajouter aux calculs de départ :
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.
- 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.
- 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
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.
- 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).
- 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.
- 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 et y sont des applications respectivement x1 +f x2, y1 +f y2 et on a x1 =c y1 et x2 =c y2.
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 le calcul global est un if : le sous calcul ne peut porter que sur les deux derniers arguments. On a les cas suivants :
- 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 :
- On réordonne les calculs suivant l'ordre des calculs sur les grandes parties de formule en premier
- On ajoute ce qui manque pour unifier les deux calculs
- 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:
- 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.
- 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
- 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-calcul "if 1b" global
devient :
- 1-calcul global "if 1b"
- 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 =
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