Lazi

Variables globales, validité

Contexte

Pour l'extension "variables globales" (qui devrait être renommé en extension "fonctions"), des règles sont déterminées.
Mais il reste à prouver que l'extension est valide.

Question

Comment prouver la validité de l'extension "fonctions" ?

Étude

Étude 1

Les fonctions peuvent être traduites grâce à "distribute". Mais il reste à traduire "setL". Le problème est que quand un setL n'est pas en position de fonction, les parties sur lesquelles s'applique le setL sont très difficiles à déterminer. Cela vient du fait que distribute change les éléments de place tout en en dupliquant. Les formules dupliquées pourront être impactées différement par un setL.

On ne peut pas simplement remplacer les distribute (remplacer les "distribute x y z" par "x z \ y z"), car il peut y avoir des formules récurrentes.

Mais la preuve à traduire est finie et sans setL, donc en traduisant seulement les "distributes" nécéssaires on peut peut être obtenir une traduction des setL.

Il faut donc déterminer :

  • Quels sont les distributes à traduire ?
  • Si une preuve contient ses setL qui ne sont pas dans des distribute, comment la traduire ?
  • Comment les traduire ?
  • Prouver que la preuve traduite est équivalente.

Quels sont les distributes à traduire

Ce sont les distributes qui contiennent des setL, car ce sont les seuls à changer la place des formules sur lesquelles le setL s'applique.

Si une preuve contient ses setL qui ne sont pas dans des distribute, comment la traduire ?

On applique d'abord des règles dites de "maximisation" à appliquer successivement :

Si x ou y contient un "setL u uf" libre :
if c x y z if c (x z) (y z)

if (setL u uf r) x y setL u uf \ if r x y

setL u uf r x setL u uf (r x)

Si x y ou z contient un "setL u uf" libre:
distribute x y z → x z \ y z

($F u → setL u uf r) uv → ($F u → r) \ uf uv

Si x ou y contient un "setL u uf" libre mais pas c (on aura pu extraire ceux de la condition avant) :
($F u → if c x y) uv → if ( ($F u → c) uv ; ($F u → x) uv ; ($F u → y) uv)

@todo

Comment les traduire

Quelques faits :

  • La preuve à traduire ne contient pas de setL sans sa cTruth. Car les preuves à traduire sont celles dont l'objet est dans la mathématique parent de l'extension.
  • La règle d'application des setL ne peut s'appliquer que quand le setL est la fonction de la formule, la preuve contient donc au préalable les déductions appliquant les distributes contenant le setL.
  • Si un setL n'est pas contenu dans un distribute
  • Si on arrive à déplacer ces distributes au début de la preuve,

@todo

Réponse