L'évaluation retardées : « Moi aussi »

Je présente ici le type d'évaluation que j'ai moi-même adopté.

1. Termes

2. Application

3. Référence

4. Symétrie d'évaluation

2. Application

Puisqu'il n'y a pas de λ-expression, la fonction apply sur un symbole s'identifie à la simple utilisation de ce symbole.

Irep[env-0 (apply x)] = Irep[env-0 x]

Pour représenter le passage de paramètres, on introduit alors la notion d'environnement local d'utilisation :

(apply x env-loc)

qui s'interprète :

Irep[env-0 (apply x env-loc)]
     env-loc* = Ienv[env-loc*:env-0 env-loc]
= Irep[env-loc*:env-0 x]

c'est-à-dire qu'on place, en priorité dans l'environnement d'évaluation, l'environnement local évalué en parallèle.

Ceci traduit bien une forme de passage de paramètres. Par exemple :

env-loc = ((def a 1))
Irep[env-0 (apply x env-loc)]
= Irep[(a:→1):env-0 x]

donc ici x est "vu" comme paramétré par le symbole a. La différence importante avec les λ-expressions est que le symbole qui représente le paramètre formel d'une λ-expression n'est plus anonyme dans le cas présent, puisqu'il est défini par l'utilisateur.