Lazi

Traduction des formules à variable globale

Contexte

Pour définir l'extension des variables globales il nous faut montrer que les formules LetG u f peuvent être traduites en formule $F u → ft où ft ne comporte pas de type de l'extension. Voir "Extension pour des variables globales".

Question

Existe-t-il une traduction possible et si oui laquelle ?

Étude 2

Pas de type étendus dans u

On ne peut pas traduire u qui n'est qu'un argument, et s'il amène des types étendus (notament subG u) alors il est clair que l'on ne peut pas traduire le letG. D'autre part faire référence à u à l'intérieur de lui même n'est pas utile (u peut être définie récursivement à la place).

Donc c'est une contrainte à ajouter aux règles de déduction : u ne doit pas contenir avoir de subG u.

Supposer qu'il n'y a pas de subG u

On peut remplacer les dvar (les variables définies par $Def) et remplacer les subG u par des setG u, donc pour la suite on supposera qu'il n'y a ni de setG u ni de dvar dans la formule.

Chercher une équivalence non totale ?

Pour avoir une équivalence, il faut remplacer les if x y z t par des if x (y t) (z t), mais ces deux formules ne sont égales que si x est un booléen. Donc on ne pourra fournir une formule équivalence que dans le cas où les conditions des if sont calculables.

Équivalence dans une fonction

Dans l'exemple suivant on voit que l'on ne peut pas factoriser le setG sur x dans l'argument c1 car il y a deux valeurs.
($F x,a,b → f (setG u x a) (setG u x b)) c1 c2 c3

Appliquer une fonction de traduction récursivement (1) ? (abandonné)

L'idée est de définir une fonction trad u f qui prend une formule avec des setG et qui retourne une fonction prendant u en argument et retournant $T[u,f] où le premier élément est la nouvelle valeur de u et le second la valeur.

Trad u ($F x → f ) = ?
Je ne vois pas comment faire car la valeur de x peut contenir des setG ce qui change la traduction, donc il faudrait appliquer la fonction avant de traduire.

Appliquer une fonction de traduction récursivement (2) ? (abandonné)

On définit trad u f qui traduit une formule f en une fonction qui prend u en argument et qui retourne $T[nu,g] où nu est le nouveau u et g la valeur.
On suppose que f ne contient pas de "subG u" (ils peuvent être remplacés avant) ni de dvar (ils peuvent aussi être remplacés avant).

setG u f uv est invalide si uv contient un "setG u", mais il peut contenir un ":lvar:u"

Règles définissant trad (xt = trad u x etc) (écritures laxistes) :

  • si x ne contient pas de "setG u" : trad u x = $F u → $T[u,x]
  • trad u (if x y z) = $F u → $Let $T[uv,xv] = xt u; if(xv, yt uv, zt uv)
  • trad u :dvar:x = :lvar:x
  • trad u $F x → f = $F u → $F x → ft u (bug: n'est pas une paire)
  • trad u (x +f y) = $F u $Let $T[uvx,xv] = xt u; $Let $T[uvy,yv] = yt uvx; $T[uvy, xv yv]
  • trad u (setG u f uv) = $F u → ft uv
  • trad u (letG u f uv) = $F u → pairSecond \ ft uv

Abandonné car on ne peut pas convertir le résultat pour les fonctions.

Appliquer une fonction de traduction récursivement (3) ?

@todo

On définit trad u x qui traduit une formule f en une paire $T[xf,uf] tq si uv est la valeur de la variable globale alors xf uv est la partie "valeur normale" et "uf u" est la valeur de la variable globale.

On suppose que x ne contient pas de "subG u" (ils peuvent être remplacés avant) ni de dvar (ils peuvent aussi être remplacés avant).
Pour les formules en argument de trad (tq x, on définit xf,uf par trad u x = $T[xn,xg]).

trad u (letG u x uv) = xn uv

trad u (if x y z) = $T[

$F u → if (xn u , yn \ xg u, zf \ xg u),
$F u → if (xn u , yg \ xg u, zf \ zg u)
]

trad u if = $T [ $F u → if, $F u → u ]
pb sur if
trad u (x y) = $T[ $F u → (xn u) (yn \ xg u) , $F u → yg \ xg u ]

Isoler la récursivité ?

Comme il me parait impossible de traduire directement les fonctions (voir ci-dessus), on peut les appliquer avant de traduire (il reste les "if"). Mais on ne peut pas appliquer les fonctions récurrentes car on aboutit à une formule infinie. L'idée est alors de traduire spécifiquement pour les récurrence et d'appliquer le reste.
Exemple sophistiqué de fonction utilisant recurse (g est la fonction récursive) :

$Def mapOneToUsage  = $F f → 
  recurse $F g → $F r,place,list,x → // r est inutilisé
      $Let my = f x; 
      if(isThing my
      ,
        // Si c'est l'élément à changer, on remplace x.
        just \ toListAdd place list \ getThing my
      ,
        // Si on doit continuer, on fait le map sur list et si ce n'est pas nothing ou rajoute x où il était.
        applyJust ($F l → toListAdd place l x) (list g nothing)
      )

Exemple 1

Comment traduire :

x recurse $F g → $F r,place,list,x → setL u uf y

On peut ajouter la variable globale en argument supplémentaire à la fonction récursive.

Distribuer les setL sur les variables globales / 2

On suppose ici que ($F u → setL u uf r) a = ($F u → r) \ uf a

Remarque : on utilise une écriture laxiste.

L'idée est de traduire certaines fonctions avec setL en fonctions sans setL. Le critère de traductabilité est que le calcul univocal (où l'on ajoute les règles pour setL et les d'autres éventuelles extentions) du corps de la fonction élimine les setL, en supposant que les conditions des if peuvent prendre toujours une valeur binaire (0b ou 1b). Par exemple la fonction $F u → if (setL u uf r) ne répond pas au critère de traductabilité.

À quoi sert cette traduction :

Pour traduire une preuve de l'extension il faut traduire les déductions comprenant des formules avec setL. La traduction définie ici change peu la phisionomie des formules. On remplace les formules avec setL par leur traduction et on adapte la preuve.
Les setL qui ne sont pas traduisibles ne sont pas calculables, donc on peut les remplacer par n'importe quoi.

Pour définie la traduction par une fonction tr qui prend en arguments une fonction f et qui retourne le couple $T[ t, fu ]t est la fonction tradute et fu est la fonction telle que si on calcul f x alors fu x est la valeur de la variable globale à la fin du calcul.
Par exemple si f = $F u → f1 f2f1 est traduisible et si tr ($F u → f1) = $T[t1,fu1] alors on aura :
tr ($F u → f1 f2) = $F u → t1 u \ ($F u → f2) \ fu1 u

La définition de tr suivante doit s'appliquer dans l'ordre des conditions :
Traduction de :
$F u → x où x ne contient pas de setL u libre :

$F u → x

$F u → x y où x est traduisible :

Si tr ($F u → x) = $T[tx,fux], alors :
tr ($F u → x y) = tr ($F u → tx u \ ($F u → y) \ fux u)

$F u → if c x yc ne contient pas de setL u libre :

tr ($F u → if c x y) =

$F u → if c x y

Comme la formule est traduisible, cela implique que c l'est. Si tr ($F u → c) = $T[tc,fuc], alors :
tr ($F u → if c x y) = tr ( $F u → if (tc u) ($F u → x\fuc u) ($F u → y\fuc u) )

Problèmes :
1) Pour calculer comment faire les remplacements de la variable globale, il faut faire comme si on réalisait le calcul de la formule, mais les remplacements se font sur la formule originèle, et non celle modifiée par le calcul. Il faut donc une sorte de traçage.
2) De plus il faut un système spéciale pour distribute puisqu'il y a dédoublement de l'argument "z".
3) On peut étendre le domaine de la fonction de traduction, de sorte que l'on peut faire tous les remplacements de setL possibles et on laisse ceux que l'on ne peut pas traiter.

Problème 1 : traçage

Exemple : if c (if c2)(distribute x) y z

Si on définit tr u uf x vn vv où :

  • u est le nom de la variable locale modifiable
  • uf est la fonction qu'il faut déjà appliquer à la valeur de la variable locale, c'est à dire que l'on remplacera dans l'expression traduite u par uf u. uf sera composé avec d'autres fonctions au fur et à mesure des setL
  • x est, après avoir remplacé la variable de nom vn par vv, la formule globale à traduire. Sachant que tr ne doit retourner que le résultat de la traduction de vv.
  • vn est le nom de la variable spécifiant l'endroit à traduire dans x
  • vv est la valeur que doit prendre la variable de nom vn dans x
et qui retourne :
la traduction de vv dans x.
Remarques :
  • Pour éviter les collisions de variables il faut choisir un nom inutilisé.
  • Au premer appel à tr on utilise pour x la formule ne contenant que la variable de nom vn.

Donc par exemple pour traduire la formule de l'exemple ci-dessus, après avoir traduit c, il faut traduire "if c2" et "distribute x" mais on ne peut les traduire seuls, ils faut les traduire dans la formule "if c2 y z" et "distribute x y z".

Problème 2 : distribute

Si une formule contient une fonction récursive f, alors l'avaluation de f n'utilise pas d'autre argument (à éclaircir). On peut transformuer f pour qu'elle prenne la valeur de u en argument (à éclaircir).

Problème 3 : domaine plus large

Domaine d'arrivée de tr

Plutôt qu'un couple, on peut utiliser $F u → setL u uf rsetL u uf r est "libre" (voir def ci-dessous).
On définira setL u uf r valide, quand uf ne contient pas de setL u libre.
On définira setL u uf r libre quand il est valide et que r ne contient pas de setL u libre.

Simplifier le domaine de départ et d'arrivée de tr

On définit tr sur le corps de la fonction, avec l'argument u en plus. Car que ce soit le départ ou l'arrivé on avait un "$F u →".

Distribuer les setL sur les variables globales / 1, abondonné

Abandonné car il faut corriger la fonction de traduction et établir un critère de traductabilité.

On suppose ici que ($F u → setL u uf r) a = ($F u → r) \ uf a

Soit tr la fonction de traduction des formules, elle prend en argument le corps f d'une fonction $F u → f et trb f est le corps de fonction équivalente sans "setL u" libre.
trf f est la fonction de modification de la variable globale,
ainsi on a $F u → f = $F u → (($F u → trb f) \ (trf f) u)
Voici les règles de calcul de tr (écriture informelle) :
trb "if (setL u uf r ; y; z) a1 ... an" → if ( trb r ; trb y; trb z) a1 ... an
trf "if (setL u uf r ; y; z) a1 ... an" → if (trb r; trf y; trf z) ∘ (trf r)

trb "distribute x y z"

Calculer jusqu'au bout

On traduit les formules en les calculant jusqu'à ce qu'il n'y ait plus de setL. Il faut voir sur quelles formules on le fait dans une traduction de preuve car le calcul peut être infini sur certaines formules. Il faut aussi voir comment alors on traduit une preuve car les formules ainsi traduites sont très modifiées.

Traduire en remplaçant les formules par des paires de fonctions (abandonné)

Abandonné car

Remarques : on utilise des notations laxistes.

On traduit $F u → f où f peut contenir des setL u libres par pairFirst (tr f) ( pairSecond (tr f) est la fonction qui retourne la nouvelle valeur de u en fonction du u de départ) défini ainsi :

tr (if x y z) = $Let $T[txf, txu] = tr x;

$T[
$F u → if(txf u; pairFirst (tr y) (txu u); pairFirst (tr z) (txu u)),
$F u → if(txf u; pairSecond (tr y) (txu u); pairSecond (tr z) (txu u))
]

tr (distribute x y z) = $Let $T[txf, txu] = tr x; 
			$Let $T[tyf, tyu] = tr y; 
			$Let $T[tzf, tzu] = tr z; 
			distribute (
				$F z → x (z 0b), 
				$F z → y (z 1b), 
				$F p → if (p, 

Traduire chaque mot et chaque application

L'avantage de ce système est que l'on garde la même structure de formule.

Un mot ou une formule est de la forme $T[ expression à retourner, fonction expression, fonction variable ], dite "triplet de calcul à état"
Chaque application est traduite par une fonction prenant en argument deux triplet

Divers

Une preuve sous LetG ne peut être faite que dans un ordre unique.

setG dans les fonctions

Les fonctions changent les places c'est pourquoi il faut pouvoir appliquer les fonctions, sinon on ne sait pas à quoi s'applique le setG. Mais il peut y avoir des fonctions récursives.

Étude 1 (abandonnée)

Car elle date d'une veille version des variables globales.

Traduction possible ?

La traduction est syntaxique, il faut que la syntaxe détermine l'ordre d'exécution des writeGlobal lors du calcul car la traduction fixe l'ordre des writeGlobal. L'ordre des writeGlobal est important car les valeurs des arguments sont dépendants des valeurs des arguments précédents (du fait que la variable globale peut être utilisée).

Il nous faut donc résoudre la sous-question : l'ordre d'exécution est-il fixe ?

L’interaction du calcul avec les valeurs se trouve dans l'exécution des "if". Mais le if ne change pas l'ordre d'exécution, il ne fait que choisir la partie de la formule à calculer.
Donc l'ordre d'exécution est fixe.

Comment déterminer l'ordre d'exécution ?

Si on a un writeGlobal dans x et un dans y, celui de x s'exécute-t-il avant pour la formule "x y" ?

On peut avoir ($F x,y → y x) a b et donc b est interprété avant a, donc un writeGlobal dans un argument peut être interprété après un se trouvant dans la fonction.
Donc la réponse est non.

Comment traduire un "distribute"

distribute x y z = x z \ y z

On a un calcul en parallèle : celui de la variable globale et celui de la valeur proprement dite.

Réponse

@todo