Best viewed in 24pt and full-screen

L

type liste_fliste (list A) -> ((list A)->(list A)) -> o .
liste_fliste L FL :- pi liste( conc L liste (FL liste) ) .
ou
liste_fliste [] zz .
liste_fliste [E|L] z[E|(FL z)] :- liste_fliste L FL .
ou
liste_fliste L FL :- iter_liste zz erz[e|(r z)] L FL .

Correspondance entre listes standard et listes fonctionnelles. Version avec quantification universelle, version récursive, et version avec itérateur*. Les trois sont réversibles*.

. Variante de Prolog qui restreint le domaine des termes plus fortement que ne le fait le typage simple, et pour laquelle le problème d'unification est décidable* et unitaire* [Miller 91b], même quand le -calcul n'est pas typé ( unification des termes de *). L'idée de est de substituer à l'axiome de -équivalence* l'axiome de -équivalence* qui est moins puissant.

Par définition, le domaine de est le plus grand sous-ensemble des -termes pour lequel la relation de -équivalence est égale à la relation de -équivalence. Ce domaine peut aussi être caractérisé syntaxiquement en restreignant la formation des applications : une variable logique ne peut être appliquée qu'à des variables essentiellement universelles distinctes et quantifiées dans la portée de la quantification de la variable logique.

Par exemple, appartient à car la variable logique  est appliquée à des -variables distinctes. Au contraire, , et n'appartiennent pas à car la variable logique  est appliquée soit à une autre variable logique, ou à deux -variables identiques, ou à un terme qui n'est pas essentiellement universel. Plus subtilement, appartient à dans , mais pas dans , car n'est pas quantifié dans la portée de . On sait maintenant étendre cette restriction à tous les systèmes du cube de Barendregt* [Pfenning 91].

L'usage de la restriction  ne s'est pas généralisé, malgré ses qualités algorithmiques, car beaucoup de définitions utiles sont exclues de . Par exemple, la définition de sigma* n'est pas dans  à cause du terme (B _). Plus généralement, la programmation à l'ordre supérieur (où des fonctions sont appliquées à des termes quelconques et pas seulement à des variables universelles) est exclue aussi : voir les prédicats jointure* et beta_conv*.

En revanche, la programmation par induction* sur la structure des termes conduit souvent à des programmes . De plus, la restriction  peut être utilisée pendant l'exécution comme critère heuristique pour éviter d'utiliser la procédure d'unification générale mais coûteuse [Brisset et Ridoux 92b, Brisset et Ridoux 92a].

(unification des termes de). n.f. (rel. *) Problème de vérifier si il existe une substitution qui peut rendre égaux modulo la -équivalence* deux -termes* du domaine , et de produire une telle substitution quand elle existe (un unificateur). Le problème est unitaire* et décidable* [Miller 91b]. Miller propose un algorithme original pour résoudre ce problème, mais on peut aussi se convaincre qu'il est unitaire est décidable en examinant le comportement du semi-algorithme de Huet* lorsqu'il est appliqué à des termes de ce domaine [Brisset et Ridoux 92b].

Dans le semi-algorithme de Huet, la simplification* ramène tous les problèmes à des problèmes flexible-rigide* ou à des problèmes flexible-flexible*. Les premiers sont ensuite traités par l´imitation* et la projection*, alors que les derniers sont suspendus. Rappelons aussi que les termes du domaine ont la propriété que les seuls termes flexibles ont des arguments qui sont des variables essentiellement universelles distinctes et quantifiées dans la portée de la quantification de la variable logique. En d'autres termes, ces arguments ne sont pas des constantes.

Deux observations permettent d'adapter le semi-algorithme de Huet au cas des termes de . La première est que si l'imitation peut être appliquée alors la projection ne peut pas l'être, et vice-versa. En effet, de par sa définition, l'imitation ne peut substituer à l'inconnue de la tête flexible qu'un terme dont la tête est une constante. Au contraire, de par la définition des termes de , la projection d'un argument d'un terme de ne peut que substituer à l'inconnue de la tête flexible un terme dont la tête n'est pas une constante. De plus, comme les arguments d'un termes flexibles de sont tous distincts, il y a toujours une seule des projections possibles qui peut produire une solution. Donc, le semi-algorithme de Huet ne calcule pas plus d'un préunificateur par problème d'unification. Ce semi-algorithme étant complet pour tout le -calcul simplement typé*, il n'y a pas d'autres préunificateurs. Il faut noter que le choix de la projection ne se fait plus sur un argument de typage mais sur le nom de l'argument à projeter. Les types ne sont donc plus nécessaires à l'exécution.

Cependant, le semi-algorithme de Huet ne calcule que des préunificateurs et laisse des problèmes flexible-flexible non résolus. La seconde observation est que un terme flexible de représente un terme inconnu dans lequel les seules variables essentiellement universelles qui peuvent avoir une occurrence sont celles qui sont argument du terme flexible ( test d´occurrence*). Le traitement des problèmes flexible-flexible de devient alors assez simple.

Il y a deux cas. Le premier est celui de deux termes flexibles dont les têtes sont différentes. Il faut substituer aux têtes une nouvelle variable logique dont les arguments sont tous ceux que les deux termes flexibles ont en commun. Le second cas est celui de deux termes flexibles dont les têtes sont identiques. Il faut alors substituer aux têtes une nouvelle variable logique dont les arguments sont tous ceux que les deux termes flexibles ont en commun et en même position. Les deux cas sont exclusifs et chacun deux ne produit qu'une solution. Ce résultat et celui portant sur les problèmes flexible-rigide montrent que le problème d'unification de  est unitaire.

On montre que le problème d'unification est décidable en vérifiant que le semi-algorithme de Huet et le traitement des problèmes flexible-flexible par la primitive terminent toujours. Le traitement d'un problème flexible-flexible conduit toujours à son élimination, n'en produit pas d'autres et ne produit pas de nouveaux problèmes flexible-rigide.

Seule la terminaison du semi-algorithme de Huet est délicate. En effet, trouver une mesure du problème qui décroit strictement par l'application de l'imitation ou de la projection n'est pas très simple. Par exemple, ces opérations peuvent augmenter le nombre d'inconnues du problème ou le nombre de problèmes flexible-rigide. Cependant, certaines inconnues n'en sont pas vraiment. Par exemple, celles qui forment la tête flexible d'un problème flexible-rigide ou flexible-flexible sont destinées à disparaitre par substitution et ne figurent dans le problème que parce que l'algorithme n'en traite qu'une à la fois. Nous les appelons des inconnues fictives. En particulier, les introduits par l'imitation ou la projection sont fictives, car elles vont figurer en tête de problème dès après la simplification

On peut montrer que la mesure constituée d'une paire dont le premier composant est la somme des longueurs des chemins qui mènent à des occurrence d'inconnues fictives et le second composant est la taille des problèmes qui ne contiennent pas d'inconnues fictives décroit pour l'ordre lexicographique à chaque application de l'imitation ou de la projection.

Le semi-algorithme de Huet complété par l'application de la primitive à tous les problèmes flexible-flexible résiduels constitue donc un algorithme d'unification pour les termes de . La principale différence avec l'algorithme de Miller est que celui-ci évite de créer les inconnues intermédiaires au prix d'une exploration plus détaillée des termes du problème.

. Notation traditionnelle de la -abstraction*. La notation de Prolog (xE pour ) permet de rester dans le cadre de la syntaxe de Prolog.

Libre. adj. (ant. lié*) ( -abstraction*, quantification* et substitution*)

Lié. adj. (ant. libre*) ( -abstraction*, quantification* et substitution*)

Liste homogène. n.f. La version typée des listes de Prolog impose généralement que tous les éléments ont le même type. On les qualifie d'homogène. On ne saurait pas utiliser les éléments d'une liste non-homogène sans l'aide d'une consultation dynamique du type des termes. Les constructeur du type des listes homogènes sont les suivants :

type nil (list T) .

type '.' T -> (list T) -> (list T) .

Liste en différence. n.f. Représentation des listes par la différence entre deux listes. C'est une représentation très employée en programmation logique* car elle conduit à des programmes efficaces en évitant des concaténations explicites ( prédicat conc*). Cependant, elle recèle quelques difficultés conceptuelles. En effet, deux listes en différence qui dénotent la même liste ne sont pas nécessairement unifiables. Par exemple, [1,2]-[2] et [1,3]-[3] dénotent la liste [1], mais ne sont pas unifiables. Le programmeur qui utilise les listes en différence devrait donc s'assurer qu'elles ne rentrent pas dans des problèmes d'unification trop complexes. C'est en général le cas, car les listes en différence servent le plus souvent de structure de données temporaire pour construire des listes standard. Ce sont ces dernières qui rentrent éventuellement dans des problèmes d'unification complexes. Un autre problème est que le test qu'une liste en différence représente une liste vide nécessite le test d´occurrence* alors que celui-ci fait défaut dans beaucoup de systèmes Prolog. Enfin, la notation M-N n'entraine pas que N est une sous-liste de M. Ainsi, l'exemple suivant montre le prédicat de concaténation de trois listes en différence, et son utilisation naïve pour spécifier la relation de liste à sous-liste.

type conc3_dl (dlist A) -> (dlist A) -> (dlist A) -> (dlist A) -> o .

conc3_d A-B B-C C-ZC A-ZC .

type sous_liste_dl (dlist A) -> (dlist A) -> o .

sous_liste_dl SousListe Liste :- conc3_dl _ SousListe _ Liste .

Ici, le prédicat conc3_dl est essentiellement utilisé en mode* (conc3_dl ? ? ? +) alors qu'il ne peut fonctionner qu'en mode (conc3_dl + + + ?).

Liste fonctionnelle. n.f. Représentation des listes par des fonctions. La représentation fonctionnelle FL d'une liste L est une fonction qui quand on l'applique à la représentation classique d'une liste M produit la représentation classique de la liste LM. La liste nil est représentée par , tandis que le constructeur de concaténation est représenté par . En d'autres termes, la liste vide est représentée par la fonction identité, tandis que la concaténation est la composition de fonctions. La correspondance entre la représentation traditionnelle et la représentation fonctionnelle est décrite par le prédicat liste_fliste*, et la représentation de la liste vide et de la concaténation sont des solutions de la spécification d'un monoïde donnée par le prédicat monoïde*.

La représentation fonctionnelle a les avantages notationnels des listes en différence*, sans en avoir les inconvénients [Brisset et Ridoux 91]. Par exemple, le prédicat suivant représente la relation entre une sous-liste et une liste, alors que cela n'est pas possible avec les listes en différence.

type sous_liste ((list A)->(list A)) -> ((list A)->(list A)) -> o .

sous_liste SousListe z(_ (SousListe (_ z))) .

La mise en uvre de la représentation fonctionnelle est cependant plus coûteuse. Cela vient de ce que la concaténation des listes en différence réalise une -réduction* au moindre coût en prenant le risque d'être incorrecte. Avec la représentation fonctionnelle, la -réduction est toujours correctement implémentée, mais en faisant des opérations qui ne sont pas toujours nécessaires.

Littéral. n.m. Formule atomique* éventuellement niée. Les formules et sont des littéraux, mais n'en est pas un.

Logique combinatoire. n.f. Théorie des combinateurs* et de leur propriétés [Curry et al. 68, Hindley et Seldin 86]. Cette théorie a été introduite par Shönfinkel, puis développée par Curry*. Par exemple, est un théorème de la logique combinatoire : pour tout , égale qui égale .

. Première implémentation de Prolog. Elle n'est ni complète ni efficace. Elle a été écrite entre 1986 et 1988 par Dale Miller et Gopalan Nadathur à l'université de Pennsylvanie (UPenn). Il s'agit d'un interpréteur écrit en Prolog.

l_terme. ex.progr. (rel. -terme*) Constructeurs de -termes purs de niveau objet.

kind l_terme type .

type app l_terme -> l_terme -> l_terme .

type abs (l_terme->l_terme) -> l_terme .

Le -terme sera représenté par (abs x(app x x)). Noter que les métatermes de type l_terme représentent des -termes purs, y compris des termes qui ne sont pas simplement typables.

Il n'y a pas besoin d'un constructeur pour les occurrences de variables. En effet, le constructeur abs signale une abstraction. On peut alors appliquer son argument à n'importe quel terme qu'on saura reconnaître. Une variable universelle joue très bien ce rôle. Les occurrences de la variable liée coïncideront avec les occurrences du terme «reconnaissable».

Les différents rédex* de niveau objet peuvent être identifiés de la manière suivante :

type (beta_redex, beta_eta_redex, eta_redex) l_terme -> o .

beta_redex (app (abs E) F) .

eta_redex (abs (app E)) .

beta_eta_redex (app (abs (app E)) F) .

l_terme_st. ex.progr. (rel. -terme simplement typé*) Constructeurs de -termes simplement typés de niveau objet. Les types du niveau objet sont représentés directement par les types du métalangage, Prolog. Si un métaterme est bien typé, alors le terme objet qu'il représente l'est aussi. Il n'y a donc pas besoin d'un prédicat explicite de vérification de type.

kind l_terme_st type -> type .

type app_st (l_terme_st A->B) -> (l_terme_st A) -> (l_terme_st B) .

type abs_st ( (l_terme_st A)->(l_terme_st B) ) -> (l_terme_st A->B) .