Machines, Interprètes
Jean Goubault-Larrecq
Aucune machine réelle n'exécute directement la relation de
b-réduction du l-calcul, ou même d'un langage
fonctionnel plus pratique comme Caml ou Haskell. Il est donc
nécessaire de passer par un interprète ou un compilateur. Il
existe de nombreuses techniques pour réaliser un interprète du
l-calcul, ou en général d'un langage fonctionnel. Nous
commencerons par présenter les machines à réduction par nom,
et en particulier la version due à Jean-Louis Krivine et les
machines à réduction de graphes, fondées sur la logique
combinatoire, en section 1. Nous verrons que la logique
combinatoire a quelques défauts théoriques, que nous tenterons
de réparer à l'aide des calculs à substitutions explicites, en
section 2. Ces techniques ont l'avantage d'avoir une
belle théorie, et de permettre la réalisation correcte de
machines à réduction pour le l-calcul complet. Ceci est
notamment utile dans la réalisation d'environnements logiques
d'ordre supérieur, comme Coq, où une composante de calcul est
présente dans les formules elles-mêmes (cf. partie 2,
arithmétique de Peano, logique et arithmétique d'ordres
supérieurs).
En revanche, ces calculs ont jusqu'ici été d'une utilité
moindre dans la réalisation d'interprètes et de compilateurs
pour des langages fonctionnels réalistes, où seule une
stratégie incomplète --- réduction faible par valeur en Caml
par exemple --- est souhaitée. On présentera des interprètes
et des compilateurs pour un petit langage fonctionnel au-dessus du
l-calcul en section 3. Les problèmes
particuliers posés par la gestion d'exceptions et les effets de
bord nous feront examiner des stratégies de compilation fondées
sur la passage de continuations en section 4. Ceci
culminera sur la technique de compilation de Baker, qui
généralise la notion de trampolines.
This document was translated from LATEX by
HEVEA and HACHA.