Lazi

Variables globales, quelles règles de déduction

Contexte

Pour définir l'extension permetant de modifier une variable dite "globale", il faut définir les règles de déductions de cette extension. Les règles ont besoin d'être réentrantes car on peut vouloir calculer une fonction se trouvant à l'intérieur d'une fonction.

Question

Quelles sont les/la nouvelles extensions à ajouter et leurs règles ?

Étude 2

On reprend l'étude 1 mais en séparant en plusieurs extensions.

Fusion avec les fonctions

La spécificité de pouvoir modifier la variable est compatible avec les fonctions, donc il suffit d'ajouter deux nouveaux types de formule :

  • setL u uf r : valides dans le corps des fonctions. Retourne r et , assigne uf x à u x est la valeur actuelle de u. Le type des formules setL ne définit que deux arguments car le troisième est sans contrainte.
  • subF u f : valide n'importe où, signifie que f est une sous-partie du corps d'une fonction de variable u.

Les critères d'utilisation d'une variable

Contexte : pour calculer la validité des déductions, il peut exister des critères comme "la formule x utilise une variable locale libre de nom n". Avec le nouveau concept de modification globale d'une variable, il est nécessaire de définir un nouveau concept d'utilisation de variable : celui d'utiliser une variable locale en écriture. On aura donc deux concept :

  • lecture d'une variable
  • écriture d'une variable

On ne peut pas unifier ces deux critères car :

  • On peut accepter la lecture et refuser l'écriture (cas où calcul une fonction appliquée à un argument).

Avec l'introduction des sous-fonctions (subF), il devient nécessaire — pour les deux critères — de lire les valeurs des variables définies.
Remarquons que cela rend les calculs du critère "lecture d'une variable plus long.

Les extensions à définir

Fonctions

Cette extension définie ce qu'est une fonction et comment calculer l'application d'un argument à une fonction.
Elle ajoute la syntaxe $F x → f.

Voir la définition de l'extension.

Sous-fonction

Cette extension ajoute la syntaxe subF x f, qui signifie que f est une sous-partie d'une fonction de variable x.
Elle ajoute la règle pour calculer une sous-fonction dans une fonction.

Est-ce que ça pose un problème car un argument peut changer la valeur d'une autre variable ? Voir avec le quantificateur universel.

@todo

Voir la définition de l'extension.

Quantificateur universel

Cette extension définie comment prouver qu'une fonction est vraie et comment appliquer cette vérité. Elle définie aussi comment prouver que deux fonctions sont égales.
Cette extension n'ajoute pas de syntaxe.

Voir la définition de l'extension.

Assignation d'une valeur à une variable locale

Cette extension ajoute la notion d'assignation d'une valeur à une variable locale.
Elle définie une nouvelle syntaxe : setL x xf r

Voir la définition de l'extension.

Étude 1

Abandonnée car il vaut mieux séparer en plusieurs extensions.

Fusion avec les fonctions

La spécificité de pouvoir modifier la variable est compatible avec les fonctions, donc il suffit d'ajouter deux nouveaux types de formule :

  • setL u uf r : valides dans le corps des fonctions. Retourne r et , assigne uf x à u x est la valeur actuelle de u. Le type des formules setL ne définit que deux arguments car le troisième est sans contrainte.
  • subF u f : valide n'importe où, signifie que f est une sous-partie du corps d'une fonction de variable u.

Les règles de déductions à ajouter

On ne peut appliquer un argument à une fonction (ie remplacer la variable par l'argument) que s'il ne contient plus d'assignation (de setL). Donc il faut des règles pour calculer les fonctions. Une fonction peut contenir une autre fonction avec des SetL pour la sous-fonction, donc il faut que les règles soit réentrentes.

Donc le mieux est de définir des règles prenant en argument une règle dans une mathématique correspondant au corps de la fonction.

Montrons qu'une mathématique calculant le corps d'une fonction ne peut avoir de règle pour calculer les setL :

Une règle calculant un setL doit contenir en argument la valeur de la variable globale.
D'autre part, on ne peut déduire la valeur de la variable globale que quand elle est en position de fonction minimale, ce qui interdirait d'utiliser les règles de déductions normales (par égalité) pour remplacer les valeurs. On ne pourrait pas déduire des chaînes d'égalités sur le corps de la fonction.

Il faut donc une règle permetant de faire des preuves sur le corps de la fonction et par ailleur une règle permetant de déduire que deux fonctions et leurs arguments sont égales et qui applique un setL.

Règle "calcul du corps" :
Soit M une mathématique.
Argument :

  • u : un nom
  • d : une déduction dans la mathématique M où l'on a ajouté le mot u ainsi que les nouveaux types de formules setL et subF correspondantes.

Soit c l'objet de d.
On déduit la ctruth où l'on remplace les conditions et la conclusion x par $F u → x.

Règle "application quantificateur universel" :
Pour toutes formules f et x ( f dans la mathématique de $F u), si

$F u → f
alors
($F u → f) x

Règle "setL" :
uf doit être une formule de la mathématique externe à $F u →
($F u → setL u uf r) a = ($F u → r) \ uf a

Mais alors, puisque les déductions "setL" déduisent des vérités du type "f a = g b" où f et g sont des fonctions, a l'ancienne valeur de la variable globale et b la nouvelle, il est nécessaire que la règle déduisant des vérités dans le corps des fonctions puissent au final aussi aboutir à des vérités sur les fonctions elles-mêmes. Sinon on ne pourrait pas faire des calculs par chaînes d'égalités.

Règle "extension d'égalité"
Si

$F u → (cf = cg )
alors
($F u → cf) = ($F u → cg).

La lecture de la variable u ne pouvant non plus se faire dans la règle de déduction sur les corps des fonctions, il faut ajouter une règle :

Règle "get read value" :
Si

  • f est une formule dans la mathématique interne à $F u→ sans de setL u libre
  • g est f où l'on a remplacé les u libres par a

alors

($F u → f) a = g

Remarque : ($F u → g) a = g, donc ($F u → f) a = ($F u → g) a. Couplé à la règle suivante, cela permet de faire des remplacements de certains u.

La règle ci-dessus permet de lire la valeur de la variable globale dans un cas particulier, il faut deux autres règles pour appliquer celle lecture plug généralement (pas de contrainte sur h):

Règle "fonctions égales dans corps" :
Si

($F u → f) a = ($F u → g) b
alors
($F u → f h) a = ($F u → g h) b

Règle "conditions égales dans if" :
Si

($F u → f) a = ($F u → g) b
alors
($F u → if f) a = ($F u → if g) b

Règle "subF" :
à l'intérieur d'une mathématique $F u → on a pour toute formule f :

subF u f = f

Règle "Application quantificateur universel" :
Si

$F x → f
alors
($F x → f) a

Relations avec les quantificateurs

Quantificateur universel

Si on déduit une vérité $F x → f, alors cela est équivalent à ∀ x; f. Il faut donc ajouter la règle que si on a $F x → f alors on peut déduire pour n'importe quel a : ($F x → f) a.

Quantificateur existentiel

Si on a ($F x → f) a alors on déduit ∃ x; f.

Règle d'application : pareil qu'avant.

Validité de ces règles

Voir l'étude.

Réponse

Je trouve 9 règles qui permettent de définir l'extension à la fois pour :

  • les fonctions
  • assignation de valeur
  • le quantificateur universel

Voir l'étude pour les règles.

@todo