Résolution de programmes (Examen Été 2023)

Soit le programme suivant :

a(_).

b(X, Y) :- a(X), c(X, Y).
b(2, 5).

c(X, Y) :- d(X), e(Y).

d(1).
d(2).

e(3).
e(4).

Dans la suite de cette question, vous devrez dessiner des arbre de résolution. Pour cela, il est important :

• d’indiquer les buts à résoudre dans les nœuds de l’arbre
• d’indiquer les assignations aux variables logiques sur les arcs
• d’indiquer true comme feuille pour les requêtes qui réussissent, et false. comme feuille pour les requêtes qui ratent.
• de représenter l’arbre dans son entièreté.
• de dessiner les nœuds de l’arbre dans le bon ordre.

1 . Quelles sont les solutions pour la requête suivante ? S’il n’y a pas de solution, indiquez false.

?- d(X).

Dessinez l’arbre de résolution complet pour cette même requête.

2 . Quelles sont les solutions pour la requête suivante ? S’il n’y a pas de solution, indiquez false.

?- c(U, V).

Dessinez l’arbre de résolution complet pour cette même requête.

3 . Quelles sont les solutions pour la requête suivante ? S’il n’y a pas de solution, indiquez false.

?- b(X, 5).

Dessinez l’arbre de résolution complet pour cette même requête.

Manipulation de listes (Examen Été 2023, Automne 2023)

1 . Définissez une fonction select/3 de façon à avoir le résultat suivant (toutes les assignations possibles sont listées) :

?- select(10,[1,2,3], R).
false.

?- select(2, [1,2,3], R).
R = [1, 3] ;
false.

?- select(2, [1,2,3,2,4], R).
R = [1, 3, 2, 4] ;
R = [1, 2, 3, 4] ;
false.

?- select(2, [1,2,3,2,4,2], R).
R = [1, 3, 2, 4, 2] ;
R = [1, 2, 3, 4, 2] ;
R = [1, 2, 3, 2, 4] ;
false.

2 . Soit la définition suivante :

p([], []).
p(L, [X|Xs]) :-
    select(X, L, R),
    p(R, Xs).

Quels sont les résultats de la requête suivante ?

?- p([1,2], [A,B]).

3 . Donnez un nom plus approprié à la relation p/2.

4 . Écrire une relation sum_list/2 qui est telle que sum_list(L, R) met en relation la liste d’entiers L et l’entier R si la somme des éléments de L est R. Aucune autre relation que sum_list ne doit être utilisée. Par exemple :

• ?- sum_list([], R). doit donner comme réponse R = 0.
• ?- sum_list([1, 6, 4, 6], R). doit donner comme réponse R = 17.

5 . Écrire une relation weakly_increasing/1 qui est telle que weakly_increasing(L) est vraie si la liste d’entiers L est triée dans l’ordre croissant. Aucune autre relation que weakly_increasing ne doit être utilisée. Par exemple :

• ?- weakly_increasing([]). doit donner comme réponse true.
• ?- weakly_increasing([1, 1, 3]). doit donner comme réponse true.
• ?- weakly_increasing([1, 1, 3, 4, 2, 5]). doit donner comme réponse false.

Tri par insertion (Examen Été 2023)

Soit le code OCaml suivant :

let rec insert x = function
| [] -> [x]
| y :: ys ->
  if x < y then
    x :: y :: ys
  else
    y :: (insert x ys)

let rec isort = function
| [] -> []
| x :: xs -> insert x (isort xs)

Donnez une définition équivalente de ces deux fonctions en Prolog.

Listes associatives (Examen Été 2023)

1 . Définissez une relation empty_assoc/1 qui est vraie pour la liste associative vide.

2 . Définissez une relation get_assoc/3 qui récupère la valeur correspondant à un élément dans une liste associative. Par exemple : get_assoc([(1, a), (2, b), (3, c)], 3, X) doit donner X = c.

3 . Définissez une relation put_assoc/4 qui ajoute un élément dans une liste associative. Si l’élément est déjà présent, il est remplacé. Par exemple : put_assoc([(1, a), (2, b), (3, c)], 3, d, L) donne L = [(1, a), (2, b), (3, d)].

Unification (Examen Automne 2023)

1 . Donner le résultat de l’unification des termes b(X, c) et b(c, Y). Le résultat doit être donné en spécifiant les valeurs que doivent prendre les variables X et Y pour que l’unification ait lieu. La réponse doit être justifiée.

2 . Donner le résultat de l’unification des termes a(X, b(Y, X), Y) et a(c(Y), Z, c(T)). Le résultat doit être donné en spécifiant les valeurs que doivent prendre les variables X, Y, Z, et T.

Arbre de résolution (Examen Automne 2023)

Dessiner l’arbre de résolution complet de la requête ?- even(4). au sein des règles suivantes :

even(0).
even(N) :-
  N > 0,
  M is N - 2,
  even(M).

Interpréteur

Soit le code source de l’interpréteur interp5.ml.

On vous demande de représenter l’exécution d’expressions au travers d’une trace d’évaluation des appels à eval. Il faut donc lister chaque appel à eval avec les arguments donnés, et la valeur de retour. On commence avec un environnement vide ([]).

Par exemple, l’évaluation de l’expression let x = 5 in x + 1 donne lieu à la trace d’évaluation suivante.

• eval [] (Let ("x", Int 5, Plus (Var "x", Int 1)))
  • appelle eval [] (Int 5)
    • -> renvoie VInt 5
  • appelle ensuite eval [("x", VInt 5)] (Plus (Var "x", Int 1))
    • appelle eval [("x", VInt 5)] (Var "x")
      • -> renvoie VInt 5
    • appelle ensuite eval [("x", VInt 5)] (Int 1)
      • -> renvoie VInt 1
    • -> renvoie VInt 6
  • -> renvoie VInt 6

Faire de même pour les expressions suivantes :

• (1 + 2) * (3 + 4)
• let x = 1 in let y = x + 2 in y + 3
• let x = 1 in let x = 2 in x
• (function x y -> x + y) 1 2
• let rec f x = f x in f 1 (cela donne lieu à une évaluation infinie, ne représenter qu’un préfixe fini de cette évaluation)

Vérification de type

Soit le code source du typeur typing.ml.

De façon similaire à l’exercice précédent, on demande de représenter les appels récursifs à type_of pour différentes expressions.

Par exemple, les appels récursifs pour l’expression let x = 5 in x + 1 sont les suivants :

• type_of [] (Let ("x", Int 5, Plus (Var "x", Int 1)))
  • appelle type_of [] (Int 5)
    • -> renvoie TInt
  • appelle ensuite type_of [("x", TInt)] (Plus (Var "x", Int 1))
    • appelle type_of [("x", TInt)] (Var "x")
      • -> renvoie TInt
    • appelle ensuite type_of [("x", TInt)] (Int 1)
      • -> renvoie TInt
    • -> renvoie TInt
  • -> renvoie TInt

Faire de même pour les expressions suivantes :

• (1 + 2) * (3 + 4)
• let x = 1 in let y = x + 2 in y + 3
• let x = 1 in let x = 2 in x
• (function (x : int) : int -> x + 1) 2
• let rec f (x : int) : int = f x in f 1

Inférence de type

Soit le code de l’inférenceur de type inference.ml

De façon similaire à l’exercice précédent, on demande de représenter les appels récursifs à type_of pour différentes expressions. Il faut maintenant maintenir les contraintes et le compteur de variable de type également.

Le faire pour les expressions suivantes :

• (1 + 2) * (3 + 4)
• let x = 5 in x + 1
• let x = 1 in let y = x + 2 in y + 3
• let x = 1 in let x = 2 in x
• (function x -> x + 1) 2
• let rec f x = f x in f 1