Extension assignation variable locale
Objet
Cette extension ajoute la notion d'assignation d'une valeur à une variable locale.
Elle définie une nouvelle syntaxe : "setL x" où "setL x nx r" signifie, dans le corps d'une fonction de variable x : "attribue la valeur nx à x et retourne r.
nx ne doit pas contenir des setL x libres, mais peut contenir des variables libres de nom x.
Extension du type des formules
On ajoute les formules setL u dans les fonctions où u est le nom de la variable locale à modifier.
Nouvelles règles de déduction
Règle "calcul d'un setL"
Si
nu ne contient pas de setL u libre
alors
($F u → setL u nu r) a = ($F u → r) \ ($F u → nu) a
Règle "extension d'un setL"
Si
nu ne contient pas de setL u libre
alors
$F u → setL u nu r x = $F u → setL u nu (r x)
Remarque : par récurrence on a : $F u → setL u nu r x1 ... xn = $F u → setL u nu (r x1 ... xn). Pour cela on utilise la règle de calcul dans les fonctions.
Règle "calcul d'une condition"
Si
nu ne contient pas de setL u libre
alors
$F u → if (setL u nu r) = $F u → setL u nu (if r)
Traduction des preuves
Validité de l'extension
@extension