Je présente ici le type d'évaluation que j'ai moi-même adopté.
1. Termes
2. Application
3. Référence
Pour structurer les utilisations, on introduit un autre symbole "spécial" : ref.
Irep[env-0 (ref x)]
env-0: x :→ Iλ[env-lex λ.(env-x rep-x)]
env-x* = Ienv[env-x*:env-0 env-x]
= env-x*
qui signifie qu'on ne garde du symbole x que sa valeur d'environnement.
C'est ici qu'intervient la difficulté algorithmique liée à l'évaluation parallèle des environnements : en effet si une définition n'est pas évaluée en revanche on évalue une référence.
De la même façon que pour une utilisation, on peut définir un environnement local de référence :
Ienv[env-0 (ref x env-loc)]
env-loc* = Ienv[env-loc*:env-0 env-loc]
= Ienv[env-loc*:env-0 (ref x)]