Tutorial 11

Exercise 1

Program

(1.) nat(s(X)) :- nat(X).
(2.) nat(0).

1. SLD-resolution tree for query :- nat(Y).:

digraph {
	node [shape=none]
	"nat(Y)." -> "nat(X1)." [label = "(1)\nY -> s(X1),\nX -> X1"]
	"nat(Y)." -> a [label = "(2)\nY -> 0"]
	"nat(X1)." -> "nat(X2)." [label = "(1)\nX1 -> s(X2),\nX -> X2"]
	"nat(X1)." -> b [label = "(2)\nX1 -> 0"]
	"nat(X2)." -> ".."
	a, b [label = "nat(0)."]
}

2. Prolog will search through the tree depth-first so will infinitely recur on the first rule.

Exercise 2

Program

(1.) member(X | [X | L]).
(2.) member(X | [Y | L]) :- X \= Y, member(X, L).

1. SLD-resolution tree for :- member(1, [2,1,3]).:

digraph {
	node [shape = none]
	"member(1, [2,1,3])" -> "1 \\= 2, member(1, [1,3])" [label = "(2)\n{X -> 1,\nY -> 2,\nL -> [1,3]}"]
	"1 \\= 2, member(1, [1,3])" -> "member(1, [1,3])"
	"member(1, [1,3])" -> "[]" [label = "(1)\n{X -> 1,\nL -> [3]}"]
	"member(1, [1,3])" -> "1 \\= 1, member(1, [3])" [label = "(2)\n{X -> 1,\nY -> 1,\nL -> [3]}"]
	"1 \\= 1, member(1, [3])" -> "failure"
}

2. SLD-resolution tree for :- member(1, []).

digraph {
	node [shape = none]
	"member(1, [])" -> "failure"
}

There is no unification between the query and the program. All of the rules require at least one item in the array, so we cannot match the empty list against any of the rules.

3. SLD-resolution tree for :- member(1, [2,3,4]).

digraph {
	node [shape = none]
	"member(1, [2,3,4])" -> "1 \\= 2, member(1, [3,4])" [label = "(2)\n{X -> 1,\nY -> 2,\nL -> [3,4]}"]
	"1 \\= 2, member(1, [3,4])" -> "member(1, [3,4])"
	"member(1, [3,4])" -> "1 \\= 3, member(1, [4])" [label = "(2)\n{X -> 1,\nY -> 3,\nL -> [4]}"]
	"1 \\= 3, member(1, [4])" -> "member(1, [4])"
	"member(1, [4])" -> "1 \\= 4, member(1, [])" [label = "(2)\n{X -> 1,\nY -> 2,\nL = []}"]
	"1 \\= 4, member(1, [])" -> "member(1, [])"
	"member(1, [])" -> "failure"
}

Exercise 3

1. No, variable cannot unify with predicate.
2. No, list cannot unify with predicate.
3. No, somepred is not unary (they have different arity).
4. No, somepred is not unary (they have different arity).
5. Yes, the unification is $\{X\mapsto X,a(b,c)\mapsto a(b,c),g(W,[H|T])\mapsto g(W,[H|T])\}$
6. No, as some and somepred are not the same predicate.
7. Yes, the unification is $\{X\mapsto r(b,c,a),b\mapsto G,c\mapsto H,W\mapsto \text{wer},H\mapsto GG,T\mapsto []\}$
8. No, as we cannot unify the predicates a and fb.
9. No, as we cannot unify [] with [H|T].