17/04/2003
Thierry Joly (IUT de Villetaneuse)
Lambda-définissabilité dans les modèles pleins finis

Deux problèmes du lambda-calcul simplement typé furent considérés dès les années 1970 par G. Huet, B. Lang, G. Plotkin et R. Statman :

DP (Definability Problem) :

Une fonctionnelle (d'un modèle plein fini quelconque) donnée est-elle l'interprétation d'un lambda-terme clos ?

MP (Matching Problem) :

Une équation donnée de la forme PX=Q, (P,Q lambda-termes clos) possède-t-elle une solution ?

Du fait que MP se réduit facilement au problème DP, ce dernier attira plus particulièrement l'attention, du moins jusqu'à ce que R. Loader en établisse l'indécidabilité (1993). On parachève le travail de R. Loader en étudiant la décidabilité de nombreuses restrictions de DP (à un modèle fixé, à un type ou ordre de fonctionnelle fixé...). En particulier, on établit l'indécidabilité de la définissabilité dans le modèle plein à 2 atomes. Enfin, on dresse un bilan définitif des cas particuliers de MP (problème toujours ouvert dans sa généralité) que DP permet de résoudre.