Projet de Langage Fonctionnel

à rendre le 14 janvier 1994

Un interpréteur λ-calcul pur en Caml-Light

On veut un petit langage que l’on appellera PLC dans lequel on puisse définir des λ-termes purs, les exécuter en pas à pas et calculer leur forme normale (si elle existe). Les combinateurs les plus courants devront être prédéfinis et une facilité pour écrire les entiers de Chuch devra être fournie.

Le λ-calcul pur avec constantes

Le langage considéré est le λ-calcul pur avec constantes. On appelle λ-termes les objets de ce langage.

Définition: Un λ-terme est soit

• un nom de constante

• un nom de variable

• l’application d’un λ-terme à un autre λ-terme

• l’abstraction d’un nom de variable

On définit les déclarations de constante et les environnements.

Définition: Une déclaration de constante est un couple constitué d’un nom de constante c et d’un λ-terme t. Le λ-terme t est appelé valeur associée à la constante de nom c.

Définition: Un environnement est une suite finie de déclarations de constantes telle qu’aucun nom ne soit déclaré dans plus d’une déclaration.

Définition: On dit qu’un λ-terme t est clos par rapport à ses variables s’il n’a pas de variables libres.

Définition: On dit qu’un λ-terme t est clos dans un environnement E s’il est clos par rapport à ses variables et si les constantes dont il dépend sont dans E.

Dans la suite, on se place dans un certain environnement E et on suppose que les λ-termes considérés sont clos dans E.

Définition: On appelle δ-redex tout sous-terme d’un terme qui est un nom de constante.

Définition: On appelle δ-réduction le fait de remplacer un nom de constante dans un λ-terme par sa valeur dans E.

Définition: On appelle β-redex tout sous-terme d’un terme qui consiste en l’application d’une abstraction à un autre sous-terme.

Définition: Si t est un λ-terme, a priori dépendant d’une variable x et u est un autre λ-terme, alors l’application à u de t pour lequel la variable x a été abstraite constitue donc un β-redex. Le λ-terme t dans lequel x a été systématiquement remplacé par le λ-terme u s’appelle contractum du redex de départ.

Définition: On appelle β-réduction le fait de remplacer un β-rédex dans un λ-terme par son contractum.

Définition: On appelle redex tout sous-terme qui est soit un δ-redex, soit un β-redex.

Conception et utilisation

PLC devra pouvoir être lancé à partir de la boucle interactive d’Unix. Il devra maintenir à jour un environnement E qui au départ sera initialisé avec les déclarations des combinateurs T, F, If, Zero, Succ, Nil et Cons (cf plus loin). PLC se présentera comme une boucle invitant l’utilisateur à entrer une commande. L’invite devra être PLC ? . On donne ci-après la syntaxe concrète des objets avec lesquelles PLC dialoguera avec l’utilisateur et pour certains de ces objets, la syntaxe interne conseillé. On trouvera ensuite la liste des commandes que l’interpréteur devra reconnaître et exécuter.

Représentation concrète des différents objets considérés

On donne ici la syntaxe concrète de chacun des objets intervenant dans le dialogue avec l’utilisateur.

Définition préliminaire: On appelle identificateur toute chaine constituée de caractères alphanumériques ou du caractère “_” et commençant par une lettre.

Les noms de constante seront représentés de manière concrète par des identificateurs commençant par une lettre majuscule.

Dans la suite, “<nom de constante>” désigne une telle chaine de caractères représentant un nom de constantes.

Les noms de variables seront, eux, représentés de manière concrète par des identificateurs commençant par une lettre minuscule.

Dans la suite, “<nom de variable>” désigne une telle chaine de caractères représentant un nom de variables.

On aura besoin d’une syntaxe concrète pour les entiers positifs (ce sera une suite consécutive de caractères numériques). On notera “<entier>” pour une telle chaine de caractères représentant un entier positif.

Quant aux λ-termes, la définition de leur syntaxe concrète est inductive. Notant “<terme>” la représentation concrète d’un λ-terme, on a que “<terme>”, c’est

• soit “<nom de variable>”

• soit “<nom de constante>”

• soit le caractère “\” immédiatement suivi d’un “<nom de constante>”, immédiatement suivi du caractère “.”, immédiatement suivi d’un “<terme>”

• soit le caractère “(” suivi de “<terme>”, suivi d’au moins un espace suivi d’un “<terme>”, suivi du caractère “)”

• soit “<entier>”, qu’il faudra comprendre comme l’entier de Church associé

Liste des commandes

On donne ici la liste des commandes que PLC devra interpréter. On donne simultanément leur syntaxe concrète et leur action (= leur sémantique). Dans une première ètape, PLC devra analyser la chaine de caractères fournie par l’utilisateur et vérifier la correction de la syntaxe. Une entrée syntaxiquement incorrecte devra être sanctionnée par un message d’erreur approprié. A la fin de l’exécution de chaque commande (excepté la commande Salut), PLC devra se mettre en attente d’une nouvelle commande.

<nom de constante> (respectivement <terme>, <entier>) désigne les représentations concrètes des noms de constante (respectivement λ-termes, entiers positifs).

• Def <nom de constante>=<terme>

PLC devra analyser la chaine de caractères terme, vérifier qu’elle correspond bien à un λ-terme t. Si t est clos dans l’environnement E, il devra y être ajouté sous le nom nom de constante et un message “nom de constante est ajoute a l'environnement” devra s’afficher. Si t n’est pas clos dans l’environnement E, cela voudra dire qu’il y a des noms de constante <nom de constante_{1}>, ..., <nom de constante_{n}> dans t auxquels il n’est pas associé de valeur dans E. Il faudra alors afficher un message “<nom de constante_{1}> n'est pas defini” (respectivement “<nom de constante_{1}>,... <nom de constante_{n}>

ne sont pas definis”).
• Env

PLC devra afficher la liste des déclarations de constantes de l’environnement courant.

• Reduit <terme>

PLC devra analyser la chaine de caractères <terme>, vérifier qu’elle correspond bien à un λ-terme, construire le λ-terme comme un objet de type terme, puis réduire ce λ-terme selon la stratégie de réduction la plus à gauche, en prenant soin de faire des α-conversion quand nécessaire. Si la réduction termine et aboutit à la forme normale dont la représentation comme chaine de caractères est <terme’>, le message “La reduction donne <terme’>” devra s’afficher avant d’attendre une nouvelle commande. Au cours de la réduction, l’interpréteur devra être attentif à l’èventuelle frappe de la touche marqué “S” (“S” comme “stopper”), auquel cas le processus de réduction devra s’interrompre et se mettre en attente d’une nouvelle commande.

• Redex <terme>

l’interpréteur devra analyser la chaine de caractères <terme>, vérifier qu’elle correspond bien à un λ-terme, construire le λ-terme comme un objet de type terme, puis afficher la liste des β− et δ-redex du λ-terme. La syntaxe proposée pour afficher les redex sera du type

1: {\x.\y.\z.(x y z) T F}
2: (\x.\y.\z.(x y z) {T} F)
3: (\x.\y.\z.(x y z) T {F})

c’est-à-dire, un redex par ligne, des accolades à la place des parenthèses pour signaler les β-redex et des accolades aussi autour des noms de constantes pour signaler les δ-redex. Les redex seront numérotés et affichés dans l’ordre de leurs numéros, en commencant par les plus à la gauche (relativement à leur représentation comme chaine de caractères)

Après cela, l’interpréteur devra se mettre en attente d’une nouvelle commande.

• Redn <entier> <terme>

l’interpréteur devra analyser la chaine de caractères <entier> et vérifier qu’elle correspond bien à un entier i, analyser la chaine de caractères <terme> et vérifier qu’elle correspond bien à un λ-terme t, construire t comme un objet de type terme, puis réduire le redex de numéro i (relativement à la numérotation donnée par la commande Redex) de t. Cela fournira un λ-terme t′ dont la représentation en tant que chaine de caractères sera <terme’>. Si i désigne effectivement un redex de t, l’interpréteur devra afficher le message “La reduction donne <terme’>”, sinon, il devra afficher le message “Ce numero de redex n'est pas defini”, et dans tous les cas, se mettre en attente d’une nouvelle commande.

• Affiche <nom de constante>

l’interpréteur devra vérifier que la chaine de caractères <nom de constante> désigne un nom de constante correct, puis afficher “<nom de constante>=<terme>” où <terme> est la représentation en tant que chaine de caractères de la valeur associée à la constante dans l’environnement. Si la constante n’est pas définie, le message “<nom de constante>n'est pas definie” devra s’afficher à la place. Enfin, l’interpréteur devra se mettre en attente d’une nouvelle commande.

• Salut

l’interpréteur devra s’arrêter et rendre la main au programme qui l’avait appelé .

Environnement minimal

Ci-suit l’environnement minimal que PLC devra fournir lors de son appel.

T = \x.\y.x
F = \x.\y.y
If = \x.\y.\z.(x y z)
Zero = \f.\x.x
Succ = \n.\f.\x.(f (n f x))
Nil = \f.\x.x
Cons = \a.\l.\f.\x.(f a (l f x))

Représentations internes conseillées

Les λ-termes seront représentés de manière interne par des objets du type terme suivant :

type terme =
Const of string
| Num of int
| App of terme * terme
| Abs of terme

Les noms de variables et de constantes seront représentés de manière interne par des objets de type string.

Le choix de la représentation interne des constantes et environnement est laissée à la discrétion du programmeur.

Extensions possibles

Toute fonction supplémentaire que le programmeur souhaiterait implémenter sera la bienvenue. En particulier, voici une liste de fonctionnalités supplémentaires que l’on pourra éventuellement implémenter.

• Autoriser la syntaxe (terme_{0} terme_{1} ... terme_{n} ) pour représenter l’application multiple (...(terme_{0} terme_{1} ) ... terme_{n} ).

• Autoriser la syntaxe \nom de variable_{1}, ... ,nom de variable_{n}.terme pour représenter l’abstraction multiple \nom de variable_{1}.\ ... .\nom de variable_{n}.terme.

• Autoriser la syntaxe [terme_{1};...;terme_{n}] pour représenter le codage des listes en λ-calcul.