Ceci est une ancienne révision du document !
Ce projet a pour objectif de construire un moteur d'unification typée pour des termes de logique du premier ordre dans le langage CHR au dessus de Prolog.
Il est à rendre pour le 28 février par mail à emmanuel.coquery@univ-lyon1.fr.
On rappelle qu'il est possible d'utiliser l'interpréteur CHR en ligne disponible ici, ressources disponibles ici.
Les termes de logique, ainsi que les types, seront représentés par des termes Prolog manipulés en CHR.
Un terme sera représenté comme suit (selon sa sorte):
var(nom)
où nom
sera le nom de la variable;const(nom)
où nom sera le nom de la constante;fonct(symb,liste)
où liste
= [t1, … ,tn]
est la liste Prolog des termes passés en arguments au symbole de fonction symb
.Un type sera;
t(nom)
(types de primitifs de base, où nom
peut être e.g. int, string, float, …);fleche(liste,res)
où liste
est une liste Prolog de types et res
est un type.
Les types primitifs seront ceux des variables, des constantes et des termes, alors que les types flèche seront ceux des symboles de fonction (liste
est la liste des types des arguments et res
est le type résultat)
<note important>Attention à ne pas confondre la notion de terme et de variable en Prolog (e.g. X
est une variable en Prolog) avec les termes et les variables définis ci-dessus où la variable de logique x est représentée par var('x')
</note>
On commencera par implémenter l'algorithme de Martelli et Montanari expliqué en cours.
On pourra utiliser les contraintes CHR suivantes:
unif/2
représentera une équation entre deux termes.unif_list/2
représentera deux listes de termes à unifier. On générera une contrainte unif/2
pour chaque paire de termes à unifier. Par exemple unif_list([t1,t2,t3],[t4,t5,t6]) se simplifiera en 3 contraintes unif(t1,t4)
, unif(t2,t5)
et unif(t3,t6)
.eliminate/2
représentera une substitution à appliquer sur les équations courantes. Remarque: cette contrainte est utilisée pour le codage de la règle eliminate de l'algorithme. La substitution ne doit pas s'appliquer sur l'équation d'où elle provient (dans la règle, la substitution est appliquée sur G et pas sur x=t)Voici, à titre d'exemple, le codage de deux règles: swap et delete
% delete % supprime une équation si elle demande d'unifier les mêmes termes logiques unif(T,T) <=> true. % swap % T est un terme, var(Y) est une variable % la garde T \= var(Z) impose que T ne soit pas unifiable en Prolog avec var(Z), % ce qui impose que T ne soit pas une variable logique unif(T,var(Y)) <=> T \= var(Z) | unif(var(Y),T).
<note tip> Exemple
La contrainte suivante:
unif(funct (plus , [ var(x), funct(plus, [var(x), const(b)]) ] ), funct(plus, [ funct(plus, [const(a), var(y)]), var(z) ] ) )
doit se transformer en:
unif(var(x), funct(plus, [const(a), var(y)]) ), unif(var(z), funct(plus, [funct(plus, [const(a), var(y)]), const(b) ] ) )
</note>
Pour procéder au typage des termes, on se donne les contraintes CHR suivantes:
type_constante/2
: associe un type à une constante. On supposera que le type associé à une constante est un type primitif.type_symb_fonction/2
: associe un type (fleche) à un symbole de fonction.type/2
: associe un type primitif à un terme.type_check/1
: demande à trouver et vérifier le type du terme logique passé en argumentDéfinir des règles CHR pour le typage en vous appuyant sur les remarques suivantes:
type_constante
f
à des arguments t1, … , tn
, son type peut être déduit du type de f
. De même, les types de t1, … , tn
sont imposés par le type de f
<note tip> Exemple Les contraintes suivantes:
type_constante(a, t(int)), type_constante(b, t(int)), type_symb_fonction(plus, fleche([t(int),t(int)],t(int))), check( fonct(plus, [ fonct(plus, [ const(a), const(b) ] ), const(b) ]) )
Doivent se transformer en
% contraintes inchangées type_constante(a, t(int)), type_constante(b, t(int)), type_symb_fonction(plus, fleche([t(int),t(int)],t(int))), % nouvelles contraintes type(fonct(plus, [ fonct(plus, [ const(a), const(b) ] ), const(b) ]), t(int)), type(fonct(plus, [ const(a), const(b) ] ), t(int)), type(const(a), t(int)), type(const(b), t(int))
</note>
<note tip> Exemple Les contraintes suivantes:
type_constante(a, t(string)), type_constante(b, t(int)), type_symb_fonction(plus, fleche([t(int),t(int)],t(int))), check( fonct(plus, [ const(a), const(b) ] ) )
Doivent se transformer en false
</note>
<note tip> Exemple Les contraintes suivantes:
type_constante(a, t(int)), type_symb_fonction(plus, fleche([t(int),t(int)],t(int))), check( fonct(plus, [ fonct(plus, [ const(a), var(b) ] ), var(b) ]) )
Doivent se transformer en
% contraintes inchangées type_constante(a, t(int)), type_symb_fonction(plus, fleche([t(int),t(int)],t(int))), % nouvelles contraintes type(fonct(plus, [ fonct(plus, [ const(a), const(b) ] ), const(b) ]), t(int)), type(fonct(plus, [ const(a), const(b) ] ), t(int)), type(const(a), t(int)), type(var(b), t(int))
</note>
<note tip> Exemple Les contraintes suivantes:
type_symb_fonction(concat, fleche([t(string),t(string)],t(string))), type_symb_fonction(i2s, fleche([t(int)],t(string))), check( fonct(concat, [ var(x), fonct(i2s, [var(x)]) ] ) )
Doivent se transformer en false
</note>
Combiner les deux solveurs précédents pour qu'une unification qui rend égaux deux termes de types différents échoue.