Résumé
Le dernier séminaire a approfondi un point délicat de la mécanisation de langages de programmation : la représentation des variables liées et l’équivalence des termes à renommage près des variables liées (règle d’alpha-conversion). Nous avons passé en revue quatre approches : les indices de de Bruijn, où les variables sont notées par positions au lieu de noms ; la syntaxe abstraite d’ordre supérieur (HOAS, Higher-Order Abstract Syntax), où les fonctions du métalangage représentent les lieurs du langage objet ; les logiques nominales, où les notions de noms de variables, d’invariance par renommage et de quantification sur un nom nouveau sont primitives dans la logique ; et l’approche « sans noms locaux » (locally nameless), qui combine indices de de Bruijn et approches nominales. Comme l’a montré l’étude POPLmark challenge, chacune de ces approches a ses forces et faiblesses, et aucune ne s’est imposée comme solution universelle.
