Lazi

Extension pour des variables globales

Contexte

Pour définir un langage de programmation avec des effets de bord il serait très pratique de pouvoir utiliser une variable globale "univers" ?

Question

Comment définir une extension mathématique pour pouvoir utiliser des variables globales ?

Étude 6

On reprend l'idée du 5 mais en séparant en multiples extensions. Voir "Variables globales, quelles règles de déduction".

Étude 5

On reprend l'idée du 4 mais en fusionnant $F et letG.

L'idée globale est d'ajouter des types de formules pour modifier une variable locale d'une fonction et des règles pour réaliser les calculs à l'intérieur des fonctions.

Les extensions de formule

setL u f uv

Validité :

  • à l'intérieur d'une fonction de variable u
  • uv ne doit pas contenir de "setL u" ou "subF u"
setL u f uv représente la valeur f où l'on a d'abord assigné uv à u.

Exemple : setLV u u uv = uv

subF u f

Validité : f peut contenir la variable locale u ou des setL u ou subF u

subF u f représente la valeur f à l'intérieur d'une fonction (non fournie) de variable u (on aura "($F u → subF u f) = ($F u → f)"). L'intérêt est de pouvoir définir une partie d'une fonction en dehors de celle-ci (par exemple par un $Def). Cela n'avait pas grand intérêt sans les setL, mais avec les setL si.

Remarque : on ne peut pas remplacer un subF u f par un $F u → f car par exemple le $F u → f ne permet pas de récupérer la valeur de u.

Une grande utilisation est de définir des fonctions à effet de bord. Par exemple $Def printText = sub universe ...

Problème dans la démonstration des quantifications universelles ?

Question :
Les règles de déductions dans le corps d'une fonction ne permettent pas d'utiliser un setL car ces règles implique d'avoir l'argument de la fonction. Mais alors si on veut prouver un quantificateur universel, est-ce que cela gêne que l'argument puisse contenir un setL, par exemple :

$F x → if x y z
$F x → x x

Étude :
Dans le premier exemple, pour pouvoir déduire des choses il faut une condition sur x, cette condition (du type "x est un booléen" ou encore plus restreint) implique que x ne contient pas un "setL x".
Dans le deuxième exemple, on peut faire le même raisonnement que pour le premier mais en plus subtil : pour déduire des choses sur "x x", il faut des conditions sur l'argument, et cela impliquera que l'argument ne contient pas de setL x.

Réponse :
Non, pas de problème.

Exemples d'utilisation

L'instruction à effet de bord

print x
peut être défini par
$Def x,r → subF u setV u r (printU x u)
où :
  • r est la valeur à retourner
  • printU prend l'univers en deuxième argument et retourne l'univers modifié par l'effet de bord de l'impression.
Le programme en langage simili C
print "titi"; print "toto"; return 1b;
peut s'écrire en simili lazi (et avec une syntaxe particulière cela pourrait être encore plus simple.
print "titi" \ print "toto" \ 1b

Les règles de déductions ajoutées par l'extension

Function Apply

Cette règle permet de calculer une fonction appliquée à un argument

Si f ne contient pas de setL u ou subF u libres (non inclus dans un autre $F u) alors

($F u → f) uv = {f où la variable u est remplacée par uv}

Function get value

Cette règle permet de lire la valeur de la variable sans appliquer la fonction.

Si uv ne contient pas de référence à u : ni la variable u, ni "setL u", ni "subF u" libres alors :

($F u → u) uv = ($F u → uv) uv

Problème de l'imbrication (pareil pour d'autres règles) (ajouter une règle de changement de variable ?):

- ($F u → (($F u → u) uv)) uv2
- ($F v → ($F u → f) uv )) vv : Comment calculer l'application intérieur (règle Function Apply),f pourrait contenir des setL v et donc il pourrait être impossible d'appliquer d'abord vv ?

Glob set

Si uv ne contient pas de référence à u : ni la variable u, ni setG u ni subG u libres ,
et si uv2 ne contient ni setG u ni subG u libres, alors :

($F u → setG u f uv2) uv = ($F u → f) \ ($F u → uv2) uv

Glob function equal

Si

letG u f1 uv1 = letG u f2 uv2
alors
letG u (f1 g) uv1 = letG u (f2 g) uv2

Glob if condition equal

Si

letG u c1 uv1 = letG u c2 uv2
alors
letG u (if c1 x y) uv1 = letG u (if c2 x y) uv2

Glob if 1b

letG u (if 1b x y) uv = letG u x uv

Glob if 0b

letG u (if 0b x y) uv = letG u y uv

Glob distribute

letG u (distribute x y z) uv = letG u (x z \ y z) uv

Glob globalize function

Pareil que la règle ci-dessus, mais ici on propage dans le cas d'un setG dans une fonction.

letG u (setG u x uv2 y) uv = letG u (setG u (x y) uv2) uv

Étude 4 (abandonnée)

Abandonnée car je passe à letG = $F

On reprend les idées de l'étude 3 que l'on remet au propre car il y a eu des changements en cours.

L'idée globale est de créer un nouveau type de formule qui représente deux valeurs qui sont calculées en parallèle :

  • la valeur standard : elle correspond à la valeur des formules sans extension
  • la valeur globale : elle correspond à la valeur de la variable globale

Les extensions de formule

  • letG u f : u est le nom de la variable globale, f est le corps (ce qui correspond au code source dans les programmes). f peut contenir des variables de nom "u". letG u f est une fonction qui prend en argument la valeur initiale de la variable globale.
  • setG u f : même arguments que letG. setG a pour sens de modifier la valeur de la variable globale à l'intérieur d'un letG.
  • subG u f : même arguments u et f que letG mais ne prend pas la valeur de u en argument supplémentaire, qui à la place est pris en lisant u. Donc à l'intérieur d'un letG on a subG u f = setG u f u. Ce sera utilisé par exemple pour définir (avec $Def) des formules utilisant la variable globale en dehors d'un letG.

Exemples d'utilisation

L'instruction à effet de bord

print x
peut être défini par
$Def x,r → subG u setG u r (printU x u)
où :
  • r est la valeur à retourner
  • printU prend l'univers en deuxième argument et retourne l'univers modifié par l'effet de bord de l'impression.
Le programme en langage simili C
print "titi"; print "toto"; return 1b;
peut s'écrire en simili lazi
print "titi" \ print "toto" \ 1b

Les règles de déductions ajoutées par l'extension

Glob flat

Cette règle permet de récupérer le résultat d'un letG.

Si f ne contient pas de setG u ou subG libres (non inclus dans un autre letG u) alors

letG u f uv = ($F u → f) uv

Remarque : On peut par exemple retourner la valeur de la variagle globale grâce à letG u u.

Glob get function

Cette règle permet de lire la variable globale.

Si uv ne contient pas de référence à u : ni la variable u, ni setG u ni subG u libres alors :

letG u u uv = letG u uv uv

Glob set

Si uv ne contient pas de référence à u : ni la variable u, ni setG u ni subG u libres ,
et si uv2 ne contient ni setG u ni subG u libres, alors :

LetG u (setG u f uv2) uv = letG u f \ ($F u → uv2) uv

Glob function equal

Si

letG u f1 uv1 = letG u f2 uv2
alors
letG u (f1 g) uv1 = letG u (f2 g) uv2

Glob if condition equal

Si

letG u c1 uv1 = letG u c2 uv2
alors
letG u (if c1 x y) uv1 = letG u (if c2 x y) uv2

Glob if 1b

letG u (if 1b x y) uv = letG u x uv

Glob if 0b

letG u (if 0b x y) uv = letG u y uv

Glob distribute

letG u (distribute x y z) uv = letG u (x z \ y z) uv

Glob globalize function

Pareil que la règle ci-dessus, mais ici on propage dans le cas d'un setG dans une fonction.

letG u (setG u x uv2 y) uv = letG u (setG u (x y) uv2) uv

Traduction des formules

Pour traduire l'extension on définira d'abord une fonction de traduction des formules, que l'on utilisera pour traduire les déductions de l'extension.
Comme d'hatitude il s'agirat de traduire les preuves qui ont pour objet une formule valide en dehors de l'extension (dans la mathématique destination de la traduction).

Nous allons donner des règles d e traductions des formules letG u. Cela ne s'applique qu'aux formules f où letG u f n'a pas de variable libre tel qu'il existe un calcul prouvant l'égalité letG u f = letG u g où g ne contient pas de setG u ou subG u.

Trad (LetG u x) = $F u → $Let $T[uv,vx] = (Trad x) u; vx

$Def applyG = $F u → $F x,y → $Let $T[u1,xf] = x u; xf y

TradI (x y) = applyG xt yt

TradI (SetG u x) = $F u → $F u2 → $Let $T[u3,u2f] = u2 u; xt u2f

TradI if = $F u → $F c,x,y → $Let $T[u1,cv] = c u; if (cv , x u1 , y u1 )

TradI distribute = $F u → $F x,y,z → applyG (applyG x z) (applyG y z)

Pour w un mot clé dans 1b,0b : TradI u w = $F u → $T[u,w]

TradI u '=' = $F u → ?

Problème : si on veut retourner $T[1b,0b], le "if" étant traduit ça ne retourne pas un vrai "if".

Comme le "if" peut être un argument d'une fonction, quand on traduit un "if", on ne sait pas à l'avance si il aura des arguments avec variable globale, donc on ne peut pas traduire de différentes manière les "if".

Mais on n'est pas obligé de traduire les formules, l'important est de traduire les déductions.

setG u f uv g → setG u (f g) uv

if (setG u c uv) x y → setG u (if c x y) uv

setG u (setG u f uv1) uv2 → setG u f (($F u → uv1) uv2)

distribute x y z → x z \ y z

Étude 3 (abandonnée)

Quand modifier la variable globale ?

La variable globale doit être modifiée quand on interprète la valeur lors du calcul naturel. Par exemple si on calcul if c x y alors si c peut contenir une modification de la variable globale. Cette modification doit être prise en compte pour le reste de la formule.

Comment lire la variable globale ?

Il semble pratique qu'elle soit représentée par un mot particulier, ce serait par exemple une variable de type "global" (malheureusement il y a déjà un type "gvar", voir comment renommer).

Comment représenter les formules contenant des effets de bord ?

Par exemple si la variable globale est :glob:u , il faut que les :glob:u puissent avoir des valeurs différentes suivant l'endroit où il se trouve dans la formule (puisque suivant l'endroit on peut avoir rencontrer des effets de bords lors de l'exécution de la formule globale).

Il est donc nécessaire qu'une formule contenant une variable globale ne soit pas vue comme une formule ordinaire (pour que l'on ne puisse pas voir les :glob:u comme identiques, ce qui entraînerait des absurdités). Pour cela il faut encapsuler la formule, par exemple "glob u f" où f est la formule et u le nom de la variable globale utilisée.

glob u f x assignerait la valeur x à u et retournerait un glob u g u2 où u2 est la valeur finale de u lors du calcul et g la valeur du calcul.

Dans f l'assignation d'une nouvelle valeur se ferait par setg u x uv où u est le nom de la variable globale, uv la valeur à lui assigner et x la valeur de setg u x uv. x peut contenir le nom "u", qui devra représenter la nouvelle valeur (ou une encore assignée encore plus récente si x contient des "setg u * *".

glob u f x retourne $T[g,u2] ou glob u g u2 ?

glob u g u2 car on a besoin d'avoir une représentation spéciale pour pouvoir distinguer des autres formules, voir les règles de déduction.

Fusionner glob et setg ?

Idées en vrac

  • glob et setg ont les mêmes types d'arguments
  • glob n'est pas sensé avec d'effet extérieur
  • Il semble cohérent de fusionner glob et setg car glob n'a pas d'effet extérieur mais pourrait en avoir s'il se trouve lui-même dans un glob.

Comment utiliser les dvar dans des formules utilisant les variables globales

Idées en vrac

  • Il faut distinguer l'utilisation d'une formule sans glob d'une avec.
  • Quel sens donner à : "$Def bla = :glob:u" ? Ça me parait insensé car on veut pouvoir utiliser les variables globales localement dans les calculs, et donc qu'il n'y ait pas un à priori sur leurs existence.
  • Quel sens donner à : "$Def bla = glob u f" ? Dans ce cas on a une fonction qui prend en argument la valeur de la variable globale u et qui retourne un "glob u * *". Mais le problème est que pour l'utiliser il faut lui donner en argument la valeur. Cela dit ce pourrait être fait automatiquement ? Pour le faire automatiquement il faudrait un autre type de définition : les définitions à variables globales : "$GDef u bla = f". Alors "bla" n'est plus une dvar mais une gdvar
  • Une solution plus simple que la précédante est de créer un nouveau type de formule : "subglob u f" avec la règle "glob u (subglob u f) uv = glob u f uv". Ainsi on n'a pas besoin de définition spéciale.

Conclusion

On crée un nouveau type de formule : "subglob u f" avec la règle "glob u (subglob u f) uv = glob u f uv"

Par exemple pour définir une fonction qui retourne l'heure de l'univers :
$Def getTime = subglob Univers Univers .o'time

Comment utiliser les variables globales dans les calculs ordinaires ?

Introduction : En dehors de la représentation de l'univers, on peut vouloir utiliser les variables globales dans un calcul récursif.

Il faut une règle pour qu'une formule contenant un "glob" soit égale à une formule sans.

Nous verrons que pour la traduction il est impossible de trouver automatiquement la dernière valeur de la variable globale. C'est pourquoi il n'y aura pas d'automatisme pour cela et donc ce sera f qui retourneras directement ce qui doit être retourné.

D'autre part, il me semble bien de distinguer le type de la formule créant la variable globale des autres, ne cerait-ce que pour distinguer sur quoi on peut retourner une formule sans variable globale.

Donc on utilisera letG u f uv pour créer une nouvelle formule f à variable globale u, et setG u f uv pour assigner cette variable globale.

flatG \ letG u f uv sera la valeur retournée par le calcul de f. Remarquons que flatG pour permettre de retourner des éléments de la variable globale, par exemple avec flatG \ letG u u uv = uv.

Comment exprimer les propriétés ?

Exemple : Comment exprimer que la fonction getTime définie plus haut retourne un entier ?

Pour tout univers U vérifiant P U, isInteger \ pairFirst \ flatGlob \ glob Univers getTime U

Traduction de l'extension

Nous traduirons l'extension en définissant une traduction des formules puis en montrant que les déductions spécifiques à l'extensions ont une traduction triviale sur les formules traduites.
L'idée de base de cette extension est d'éviter un travail de passage de valeurs (celles contenues dans la variable globale), passage que nous allons expliciter par la traduction.

On suppose que les formules n'utilise pas le nom de la variable globale comme nom d'une variable locale, si ce n'était pas le cas on pourrait déjà renomer la variable globale pour que ce le devienne.

Remarquons que les règles de déductions sur les formules "letG" imposent qu'une seule déduction maximum puisse être faite sur une formule à variable globale. Donc si on des déductions sur une formule à variable globale il n'y a pas de choix des déductions, c'est pourquoi nous parlerons de calcul pour les formules à variable globale. Ce calcul n'est autre que l'interprétation du source.

Nous allons définir la fonction TradG u f où :

  • u est le nom de la variable globale
  • f est une 1-formule lazi de type "letG"
TradG u f retourne le couple $T[ g, ft ] où g et ft sont des 1-formules lazi dans la mathématique sans l'extension où si uv est une 1-formule représentant la valeur de la variable globale au début du calcul de f, alors :
  • ($F u → g) uv est une 1-formule représentant la valeur de la variable globale à la fin du calcul de f
  • ($F u → ft) uv est une 1-formule représentant la traduction de f

Remarque : nous utilisons des écritures laxistes, par exemple "$F u → ft" signifie "la fonction de variable dont le nom est u et de corps ft".

Autrement dit, on traduit une formule letG par les corps d'un couple de fonctions :

  • la fonction prenant en argument la valeur de la variable globale au début du calcul de f et retournant la valeur de la variable à la fin du calcul de f
  • une fonction prenant en argument la valeur de la variable globale au début du calcul de f et retournant la valeur de f (sous forme d'une 1-formule n'utilisant pas l'extension).

Soit $T[ g, ft ] = TradG u f, alors :

  • letG u f uv se traduit par ($F u → ft) uv
  • si on calcul letG u f uv par les règles données ci-dessous, à la fin du calcul la valeur de la variable globale u sera g uv.

Mais nous devons définir la traduction de toute formule de la mathématique extension, TradG étant limité aux formules letG. C'est pourquoi nous définissons Trad u f par :

  • si f est un letG : Trad u f = pairSecond ∘ TradG u f
  • sinon, si f ne contient rien de l'extension : Trad u f = f
  • sinon, si f =
flatG \ letG u g uv (voir la règle ci-dessous) et si f ne contient aucunne référence à u (y compris les setG u), alors Trad u f = g
  • sinon, si f = g +f h, alors Trad u f = Trad u g +f Trad u h

La traduction des formules letG suit les types de formules des règles ci-dessous, c'est pourquoi nous définissons les traductions à l'intérieur de la définission des règles ci-dessous. Les conditions des règles s'appliquent aux conditions de traduction.

Les règles de déduction de l'extension "glob"

Pour chaque règle, nous définissons :

  • la règle elle-même
  • la fonction "Trad", voir ci-dessus
  • la traduction des déductions de la règle, ce qui permet, entre autres, de prouver la validité de l'extension.

Pour traduire une preuve dans l'extension glob on traduit les formules qu'elle comprend par Trad puis les déduction par les règles de traduction définies ci-dessous.

Glob flatG

La règle

Si f ne contient aucunne référence à u (y compris les setG u), alors flatG \ letG u f uv = f

Traduction de la règle

Soit $T[ g, ft ] = TradG u f, comme letG u f uv est traduit par ($F u → ft) uv , il faut traduire la déduction "flatG" par la preuve que ($F u → ft) uv = ft dans le cas où u est inutilisé dans ft.

Glob Fonctions égales

La règle

Si letG u f x = letG u f2 x2 alors letG u (f g) x = letG u (f2 g) x2

Définition de TradG

TradG (letG u (f g) x) = TradG (letG u (f2 g) x2) (faux, on n'a pas l'égalité dans la traduction)

Traduction

de la règle

Il faut traduire par la preuve que Trad u (letG u (f g) x) = Trad u (letG u (f2 g) x2),
or par définition de TradG, Trad u (letG u (f g) x) et Trad u (letG u (f2 g) x2) sont les mêmes formules, donc on peut utiliser la réflexivité de l'égalité pour traduire la déduction.

Glob If condition

Cette règle est similaire à "Glob Fonctions égales" : Glob Fonctions égales permet d'avancer le calcul sur la partie fonction, ici on avance le calcul sur la condition du if.

La règle

Si letG u c uv = letG u c2 uv2 alors letG u (if c x y) uv = letG u (if c2 x y) uv2

Définition de TradG

Soit $T[ct,ut] = TragG u letG u c
Soit $T[xt,uxt] = TragG u letG u x
Soit $T[yt,uyt] = TragG u letG u y

TradG (letG u (if c x y)) = $F u → if (ct u) (xt (ut u)) (yt (ut u))

Glob If 1b

La règle

Si letG u c uv = letG u 1b uv2 alors letG u (if c x y) uv = letG u x uv2

Définition de TradG

TradG (letG u (if c x y) uv) =

Traduction de la règle

Glob distribute

La règle

glob u (distribute x y z) uv = glob u (x z \ y z) uv

Traduction

Glob glob

La règle

glob u (glob u x uv2) uv1 = glob u x uv3
où uv3 est uv2 où l'on a remplacé u par uv1

Traduction

Glob sub

La règle

glob u (subglob u f) uv = glob u f uv

Traduction

Remarques

On n'a que les règles minimales de calcul, notament pas la règle "égalité et vérité" ni "Glob arguments égaux" car on doit calculer les formules dans l'ordre naturel pour déduire les valeurs de la variables globale. Or l'ordre naturel calcul toujours la fonction en premier quand cela est possible. En utilisant que les règles minimales données ci-dessus on impose le calcul naturel et donc un ordre sur l'application des changements de la variable globale.

Étude 2 (abandonnée)

Abandonnée car je veux remettre au propre en essayant de raisonner.

Une déduction de calcul spéciale

La valeur de la variable globale "univers" ne peut être initialisée en interne, car tout l'intrêt est que le calcul soit dépendant de cette valeur. Il faut donc que la déduction de calcul ait un argument supplémentaire qui soit la valeur de "univers".

On pourrait qualifier de telles types de déduction d'"informatique", ainsi on aurait une règle de déduction d'informatique. La différence est qu'il y a en argument supplémentaire un univers et l'expression de propriétés sur le source. Les règles de déduction d'informatique ont deux arguments : le source et l'unviers.

L'objet d'une déduction est une vérité. Il nous faut donc exprimer par une vérité le résultat du calcul. Cette vérité doit contenir l'univers de départ et celui d'arrivé. Nous verrons cela après avoir définie l'extension des formules.

Étendre les formules lazi

On ajoute un nouveau type de formule : writeGlobal v x vv où :

  • v : le nom de la variable globale
  • vv : la nouvelle valeur assignée à v
  • x : la valeur de writeGlobal v x vv

Par exemple si on veut écrire le code "print a; print b; return 2;" cela consiste en un changement d'univers et une valeur retournée. On voit donc que writeGlobal peut incorporer plusieurs modifications de l'univers quand elles se suivent.

writeGlobal change la valeur de la variable globale v pour la suite de la formule, les v qui ont la valeur attribué par le writeGlobal sont ceux qui seront évalué par l'ordre du calcul avant qu'un nouveau writeGlobal soit évalué. Il faut donc que l'on ne puisse pas remplacer les v dans les formules puisque suivant la place dans la formule ils peuvent avoir une valeur ou une autre.

Une solution serait de commencer par renommer la variable globale v en utilisant différent noms suivant la position d'évaluation. Ainsi il n'y a plus de conflit de nom.

Une variable globale pourrait être constitué d'un nom et d'un numéro d'ordre. Mais on tombe sur le problème du distribute où il y a duplication éventuel de la variable globale avec des ordres différents (par exemple si on fait un recurse contenant un writeGlobal). On ne peut donc pas attribuer les numéros statiquement. Peut-être peut-on les attribuer dynamiquement ou dynamequement replacer le nom de la variable global par la valeur ?
On peut ne remplacer v que quand on l'évalue :

Si on a une vérité f contenant v en fonction, alors on peut remplacer v par sa valeur (pour writeGloballe remplacement ne se fait pas dans les deux premiers arguments).
Mais la notion d'évaluation n'a pas trop de sens car il n'y a pas d'ordre dans les preuves.

Valeur retournée par une déduction d'informatique

Si la déduction utilise la variable globale v, avec comme valeur de départ x et pour calculer y, alors le résultat est exprimé de la forme :
writeGlobal v x y = writeGlobal v z t.

Comment traduire la déduction d'informatique

Puisque l'on utilise une nouvelle déduction et un nouveau type de formule il nous faut définir une extension lazi.

Ce nouveau type de formule (les writeGlobal) peuvent être calculés, c'est pourquoi il nous faut définir une nouvelle déduction pour les calculer. Cette déduction

Étude 1 (abandonnée)

Abandonnée car l'idée d'étendre les formules Lazi me parait maitenant possible.

Le problème de la valeur de l'univers en entrée

La valeur de la variable globale "univers" ne peut être initialisée en interne, car tout l'intérêt est que le calcul soit dépendant de cette valeur. Il faut donc que la déduction de calcul ait un argument supplémentaire qui soit la valeur de "univers".

On ne peut emboîter des calculs à variables globales car une déduction de calcul n'a pas de sous-déduction.

On pourrait qualifier de telles types de déduction d'"informatique", ainsi on aurait une règle de déduction d'informatique. La différence est qu'il y a en argument supplémentaire un univers et l'expression de propriétés sur le source. Les règles de déduction d'informatique ont deux arguments : le source et l'unviers.

Le problème de la valeur de l'univers en sortie

Une déduction d'informatique a forcément pour objet une vérité. On l'exprime par f u1 = $T[ x, u2 ] où u1 est l'univers en entrée et u2 en sortie.

Le source et l'univers

Exemples

print

Imaginons une fonction "writeFile" qui doit retourner une valeur pour indiquer si cela a marché, et qui modifie l'univers U, même en cas d'échec.

Lecture de la valeur de l'univers

La lecture se fait par une variable globale (comme celles définies par des $Def).

Écriture de la valeur de l'univers

L'écriture se fait par un évènement "writeUniserse x". Cela implique que le code source à l'intérieur de $Def ou de la valeur retournée n'est plus une formule mathématique.

Extension des formules

On étend les formules par "writeGlobal v x y" où v est le nom de la variable globale, x est la nouvelle valeur à lui attribuer et y est la valeur que vaut writeGlobal v x y avec y ne contenant pas de "writeGlobal v" mais pouvant contenir v.

Pour qu'un "writeGlobal v x y" soit valide il faut déjà se trouver dans une mathématique où v est déclaré comme une variable globale (différent des $Def). On appellera les noms définit par $Def des constantes globales, donc différentes des variables globales.

Pour une formule f, on dira qu'elle utilise la variable globale v si elle utiliser un writeGlobal v ou directement v.

On définit la fonction de traduction TradGlob v f qui traduit les formules. Voir l'étude sur la définition de TradGlob. comme suit (on utilise des notations laxistes pour simplifier):
Si f ne contient par de "writeGlobal v x y" :

TradGlob v f = $F v → $T[v,f]

Si f = "writeGlobal v x y" :

TradGlob v f = $F v → $T[x,y]

Si f = if c x y où c n'utilise pas v :

TradGlob v f = if c $[TradGlob v x] $[TradGlob v y]

Si f = if c x y où c utilise v :

TradGlob v f = $F v → $Let $T[v2,c2] = $[TradGlob v c] v; if c2 ($[TradGlob v x] v2) ($[TradGlob v y] v2)

Si f = distribute x y z :

TradGlob v f = $F v → $Let $T[vz,z2] = $[TradGlob v z]; distribute x y à finir

Si f = g x :

TradGlob v f =

Preuve produite par une déduction d'informatique

On peut faire de deux manières :

  • Traduire le source pour qu'il n'y ait plus d'utilisation de la variable Universe, puis utiliser une déduction de calcul pour produire la preuve.
  • Produire une preuve directement : p
our chaque writeUniverse et pour le départ on utilise un évènement qui permet de définir la valeur "Universe". Cet évènement filtre les vérités contenant la variable globale "Universe".

Traduire le source

On suppose que le source contient déjà les extensions pour les fonctions ($F) et les définitions ($Def). Traduire le source me paraît nécessaire pour pouvoir spécifier les propriétés mathématiques sur des formules lazi (ce ne sont plus des valeurs mathématiques quand le source contient des "writeUniverse x").

Si le source est constitué d'une liste de "writeUniverse f1" ... "writeUniverse fn", puis d'une formule g. Supposons que le nom global pour représenter l'univers est "U".
On remplace le source par : $F U → ($F U → $T[U,g]) \ ($F U → fn) \ ($FU → fn-1) \ ... \ ($F U → f1) U

Réponse

@todo