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 2015 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.

Tutoriel Prolog

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):

• une variable: var(nom) où nom sera le nom de la variable;
• une constante const(nom) où nom sera le nom de la constante;
• un symbole de fonction appliqué à des termes 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;

• soit t(nom) (types de primitifs de base, où nom peut être e.g. int, string, float, …);
• soit 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 argument

Définir des règles CHR pour le typage en vous appuyant sur les remarques suivantes:

• un même terme logique ne peut pas avoir deux types différents
• si un terme est une constante, son type est donné par la contrainte CHR type_constante
• si un terme est une application d'un symbole de fonction 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
• si un terme est une variable, son type est imposé par son utilisation

<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.