5.1 Environnement d'évaluation
Le l-calcul est véritablement
un calcul grâce à la règle b-réduction qui correspond à
la réduction d'un redex à l'intérieur d'un terme. Cette règle substitue
le paramètre formel d'une fonction dans le corps de la fonction par le
paramètre d'appel :
(l x.M)N ®0 M[N/x]
On peut utiliser cette règle de substitution lors de l'appel d'une fonction sur ces arguments, mais cette technique n'est pas très réaliste
si l'on désire une quelconque efficacité de l'évaluation. Pour cela,
on ne substitue pas une variable par un terme, mais on effectue un lien
entre une variable et
une valeur. On conserve les différentes liaisons d'un calcul dans un environnement. Ainsi l'application de (l x.M)N s'évalue comme l'évaluation de M dans l'environnement où x vaut N. De plus en ML, la
stratégie d'évaluation est stricte, c'est à dire les arguments passés
à une fonction sont évalués. L'environnement peut être vu alors comme
une liste de liaisons : variable - valeur.
Soit E un environnement, e une expression à calculer dans E,
on note l'évaluation de e dans E donnant v de la manière suivante :
E |- e Þ v
qui se lit
"l'expression e a la valeur v dans l'environnement E".
De même on note :
[(Pair)]
E|- e1 Þ v1 E|- e2 Þ v2
E|- (e1,e2) Þ (v1,v2)
la règle Pair indiquant que si e1 s'évalue en v1 dans E et si e2 s'évalue en v2 dans E, alors (e1,e2) s'évalue en (v1,v2) dans E.