Indices de de Bruijn

Le but du projet est d'évaluer des termes du λ-calcul en indices de de Bruijn. Les indications de syntaxe du langage de l'interpréteur sont entre parenthèses.

La base de la syntaxe utilisateur des termes sera L (pour λ), les entiers, les espaces, les parenthèses et le point.

On doit pouvoir dans un premier temps :

• Obtenir un terme atteint après une β-réduction (next),
• Obtenir l'ensemble de tous les termes atteignables avec une β-réduction (all-next),
• Chercher une forme normale pour un terme, d'abord en stratégie normale (normalise).

Dans un deuxième temps on se donnera la possibilité de :

• Préciser la stratégie de réduction : normale, c'est-à-dire gauche extérieure (lo), ou droite intérieure (ri), dans les deux cas avec (all) ou sans réduction (excl) sous les λ,
• Nommer les termes avec une construction de type "let".