Je présente ici le type d'évaluation que j'ai moi-même adopté.
1. Termes
2. Application
3. Référence
Etant donné un environnement : env-loc et les définitions :
(def a (def b
env-a = env-loc env-b = ()
rep-a = (apply x ()) rep-b = (apply x env-loc))
a et b s'interprètent identiquement dans un même environnement, soit :
Irep[env-0 a] = Irep[env-0 b]
On calcule :
(1) | |
dans env-a*:env-0 :l'environnement local d'utilisation est vide : env-loc-a* = ()on est donc placé dans l'environnement : env* = ():(env-a*:env-0) = env-a*:env-0= Irep[env* x] | |
(2) | |
dans env-b*:env-0 = ():env-0 = env-0 :on évalue l'environnement local d'utilisation : env-locenv-loc-b* = Ienv[env-loc-b*:env-0 env-loc]on est donc placé dans l'environnement : env'* = env-loc-b*:(():env-0) = env-loc-b*:env-0On a env-a* = env-loc-b* donc env'* = env*on trouve donc le même symbole x.= Irep[env* x]
Note : on décrète que |