Lazi

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""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