Machines, Interprètes

Jean Goubault-Larrecq

Abstract: Ceci est la version 2 de la troisième partie du cours de lambda-calcul, datant du 28 janvier 2011. La première version datait du 15 avril 2002. Merci à Hang Zhou et à Arthur Milchior.
Aucune machine réelle n'exécute directement la relation de β-réduction du λ-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 λ-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 λ-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 λ-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.