Je présente ici le type d'évaluation que j'ai moi-même adopté.
1. Termes
2. Application
3. Référence
Définition
On commence par le plus simple, à savoir les définitions.
Ienv[env-0 (def x env rep)]
= ( x :→ Iλ[env-0 λ.rep] )
c'est-à-dire qu'une définition est "vue" comme une λ-expression quotée sans argument (en particulier l'environnement de définition env est ignoré).
Symbole
L'utilisation d'un symbole force son évaluation :
Irep[env-0 x]
env-0: x :→ Iλ[env-lex λ.(env-x rep-x)]
env-x* = Ienv[env-x*:env-0 env-x]
rep-x* = Irep[env-x*::env-0 rep-x]
= rep-x*
(ici aussi l'évaluation parallèle est imparfaitement réalisée ; la difficulté est cependant d'un autre ordre, puisque les définitions ne sont pas évaluées – cf. ref).
On remarquera en particulier que l'environnement d'appel est utilisé à l'évaluation du symbole et que l'environnement de définition est ignoré (inconnu) : la recherche des identificateurs est dynamique.
λ-expression
De même qu'un symbole est vu comme une λ-expression quotée, une λ-expression est vue comme un symbole ; c'est-à-dire qu'il n'y a pas à proprement parler de λ-expression : la notion est implicite.