1.1 Évaluateur de λ-calcul

Le schéma d'évaluation d'un λ-terme est le suivant :

env	terme	pile	env	terme	pile
e	c	S	e	c	S
e	MN	S	e	M	(N.e::S)
e_ρ	λ x.M	s::S	(e,s)_ρ,x	M	S
(e,(M.e2))_ρ,x	x	S	e2_ρ	M	S
(e,a)_ρ,y	x	S	e_ρ	x	S

où l'environnement contient des couples (termes,environnement), c'est-à-dire des valeurs calculables.

Solution :

Ce λ-calcul est étendu aux déclarations locales.

env	terme	pile	env	terme	pile
e_ρ	let x=N in M	S	(e,N.e)_ρ,x	M	S
e_ρ	let rec x=N in M	S	f=(e,N.f)_ρ,x	M	S

1.2 Instructions de la machine

Grab : met le sommet de pile dans l'environnement
Push label : met le label et l'environnement dans la pile
Acces n : accès à la n-ième variable de l'environnement
Label label : étiquetage

Solution :

Let label : met la fermeture (label, environnement) dans l'environnement
Rec label : met la fermeture (label, nouvel environnement) dans l'environnement qui vaut le nouvel environnement

1.3 Schéma de compilation

On note [M]_ρ la compilation du terme M dans l'environnement ρ.

[MN]_ρ = Push l; [M]_ρ; Label l; [N]_ρ
[λ x.M]_ρ = Grab; [M]_ρ,x
[x]_ρ = Acces n (où n est la position de x dans ρ)

Solution :

[let x = N in M]_ρ = Let l; [M]_ρ,x; Label l; [N]_ρ
[let rec x = N in M]_ρ = Rec l; [M]_ρ,x; Label l; [N]_ρ,x

1.4 Schéma d'évaluation

Une fois les λ-termes traduits en instructions machine, il est nécessaire d'avoir un interprète de cette machine virtuelle. Voici le schéma d'évaluation des instructions de cette machine :

env	code	pile	env	code	pile
e	Push l;C	S	e	C	(l.e)::S
e	Grab; C	s::S	(e,s)	C	S
e	(*)Grab;C	()	arrêt	sur	(e,*)
(e,(l.e2))	Acc 0;C;Label l; C2	S	e2	C2	S

Solution :

env	code	pile	env	code	pile
e	Let l;C	S	(e,(l.e))	C	S
e	Rec l;C	S	ne=(e,(l.ne))	C	S

Ce document a été traduit de L^AT_EX par H^EV^EA