Programming Language Design Paradigms: Logic Programming: Part 2 - Semantics

Programming Language Design Paradigms
Logic Programming: Part 2 - Semantics
Maribel Fernandez and Elliot Fairweather
Department of Informatics
Kings College London
Spring 2017
Introduction
I Use formulae to express knowledge and describe problems

I Use inference to compute with knowledge and solve problems
I Theory: unification and SLD-resolution

I Practice: implementation in Prolog
History of unification
I A unification algorithm was first sketched by Jacques

Herbrand in his thesis in the 1930s.
I In 1965, Alan Robinson introduced the Principle of Resolution
and gave a unification algorithm.
I Finally, around 1974, Robert Kowalski, Alain Colmerauer and
Philippe Roussel defined and implemented the logic
programming language Prolog based on these ideas.
I The version of the unification algorithm that we present is
based on the work of Martelli and Montanari from 1982.
Unification
I A unification problem U is a set of equations between terms

containing variables.
{s1 = t1 , . . . , sn = tn }
I A solution to U, also called a unifier, is a substitution , such

that when when applied to every term in U, for each equation
si = ti , the terms si and ti are syntactically identical
I The most general unifier (mgu) of U is a unifier such that
any other unifier is an instance of
Unification algorithm
I The unification algorithm finds the mgu for a unification

problem if a solution exists, or otherwise fails, indicating that
there are no solutions
I To find the mgu the algorithm simplifies the set of equations
using a set of transformation rules
I At each step, either a new set of equations is produced or a
failure case arises
I The algorithm terminates and outputs the mgu when no rule
may be applied
Unification algorithm: rules
I Input: a finite set of term equations, {s1 = t1 , . . . , sn = tn }
I Output: the mgu of those equations or failure.
(1) f (s1 , . . . , sn ) = f (t1 , . . . , tn ), E s1 = t1 , . . . , sn = tn , E
(2) f (s1 , . . . , sn ) = g (t1 , . . . , tm ), E failure
(3) X = X,E E
(4) t = X,E X = t, E
if t is not a variable
(5) X = t, E X = t, E {X 7 t}
if X not in t and X in E
(6) X = t, E failure
if X in t and X 6= t
More on the unification algorithm
I The unification algorithm applies the rules in a

non-deterministic way until no rule can be applied or a failure
case arises.
I In the case of success, by changing each = in the final set of
equations to 7 we obtain the mgu of the initial set of terms.
I Note that we are working with sets of equations, therefore
their order in the problem is unimportant
I The test in case (6) is called an occur-check. For example,
X = f (X ) is a failure case. This test is time consuming, and
for this reason in some systems it is not implemented.
I Cases (1) and (2) apply also to constants: in the first case the
equation is eliminated and in the second failure arises.
Examples of unification
Example
{ f(a, a) = f(X, a) }
I using rule (1) with the first equation:
{a = X , a = a}
{X = a, a = a}
I using rule (1) with the second equation:
{X = a}
{X 7 a}
More examples of unification
Example
{[X | L] = [0], Y = [1, 2], [X | Z] = U}
{X = 0, L = [], Y = [1, 2], [X | Z] = U}
{X = 0, L = [], Y = [1, 2], [0 | Z] = U}
I using rule (4) with the last equation:
{X = 0, L = [], Y = [1, 2], U = [0 | Z]}
{X 7 0, L 7 [], Y 7 [1, 2], U 7 [0 | Z]}
Exercise
Solve the following unification problem:
{f (g (a), b) = f (X , b), X = g (Z ), f (a, Y ) = f (Z , Y )}

Solution
{f (g (a), b) = f (X , b), X = g (Z ), f (a, Y ) = f (Z , Y )}

I Rule (1), 1: {g (a) = X , b = b, X = g (Z ), f (a, Y ) = f (Z , Y )}
I Rule (4), 1: {X = g (a), b = b, X = g (Z ), f (a, Y ) = f (Z , Y )}
I Rule (5), 1: {X = g (a), b = b, g (a) = g (Z ), f (a, Y ) = f (Z , Y )}
I Rule (1), 2: {X = g (a), g (a) = g (Z ), f (a, Y ) = f (Z , Y )}
I Rule (1), 2: {X = g (a), a = Z , f (a, Y ) = f (Z , Y )}
I Rule (4), 2: {X = g (a), Z = a, f (a, Y ) = f (Z , Y )}
I Rule (5), 2: {X = g (a), Z = a, f (a, Y ) = f (a, Y )}
I Rule (1), 3: {X = g (a), Z = a, f (a, Y ) = f (a, Y )}
I Rule (1), 3: {X = g (a), Z = a, a = a, Y = Y }
I Rule (1), 3: {X = g (a), Z = a, Y = Y }
I Rule (3), 3: {X = g (a), Z = a}
{X 7 g (a), Z 7 a}
The Principle of Resolution
I In order to prove a goal B1 , . . . , Bn with respect to a set P of

program clauses, resolution seeks to show that
P, B1 , . . . , Bn leads to a contradiction
I A contradiction is obtained when a literal and its negation are
stated at the same time, that is, both A and A
I If a contradiction does not arise directly, a new goal is derived
by unifying the current goal with a program clause
I The derived goals are called resolvents
SLD-resolution
I S selection rule: at each resolution step a fixed computation

rule is applied to select which atom from the goal will be next
resolved upon
I L linear: at each resolution step the most recently derived
resolvent is used as the next goal
I D definite: all the program clauses are definite clauses
Properties of SLD-resolution
1. SLD-resolution is refutation-complete: given a program and a

goal, if a contradiction can be derived, then SLD-resolution
will eventually generate it
2. Independence of the selection rule: if there exists a solution to
a goal, SLD-resolution will find it, regardless of the selection
rule employed for choosing which atom is next resolved upon
Computing resolvents with SLD-resolution
I Given a goal clause G1 , G2 , . . . , Gk , we select an atom Gi of

form p(s1 , . . . , sn )
I We select a program clause p(t1 , . . . , tn ) B1 , . . . , Bm such
that p(t1 , . . . , tn ) and p(s1 , . . . , sn ) are unifiable using the
mgu
I We then obtain the resolvent B1 , . . . , Bm , G1 , . . . , Gk
from which Gi has been eliminated
I The idea is to continue deriving new resolvents until an empty
one is found, which indicates that a contradiction has been
found
I When an empty resolvent is generated, the composition of the
substitutions applied at each resolution step, restricted to the
variables of the query, is the solution to the goal
SLD-resolution trees
We represent each resolution step graphically as follows:
goal
mgu
resolvent
I Since there might be several clauses in the program that can

be used to generate a resolvent from a goal, we obtain an
SLD-resolution tree
I Every branch in the SLD-tree that leads to an empty
resolvent, denoted by , yields a solution
I If a goal unifies with no program clause, the branch is a failure
I An SLD-resolution tree may thus have success branches,
failure branches, but also infinite branches
SLD-resolution in Prolog
I Prolog always selects the leftmost literal in the goal

I Prolog uses the clauses in the program in the order they are
written, that is, from top to bottom
I SLD-resolution is complete, but Prologs implementation of
SLD-resolution is not complete because of its search strategy
in the SLD-tree. Prolog uses depth-first search, which is not
complete, but is efficient in respect to the time until a first
solution is found.
Example of SLD-resolution in Prolog
Example
based(prolog, logic).
based(haskell, maths).
likes(max, logic).
likes(claire, maths).
likes(X, P) :- based(P, Y), likes(X, Y).
Example of SLD-resolution in Prolog continued
Example
I :- likes(Z, prolog).
I Using the last clause and the mgu {X 7 Z, P 7 prolog}, we
obtain the resolvent :- based(prolog, Y), likes(Z, Y).
I Now using the first clause and the mgu {Y 7 logic}, we
obtain the new resolvent :- likes(Z, logic).
I Since we can now unify with the fact likes(max, logic).
using the substitution {Z 7 max}, we can obtain an empty
resolvent
I The composition of substitutions generated is
{X 7 max, P 7 prolog, Y 7 logic, Z 7 max}
I And the solution to the initial query is {Z 7 max}
Example of SLD-resolution in Prolog continued
Example
:- likes(Z, prolog).
{X 7 Z, P 7 prolog}
:- based(prolog, Y), likes(Z, Y).
{Y 7 logic}
:- likes(Z, logic).
{Z 7 max} {X 7 Z, P 7 logic}
:- based(logic, Y), likes(Z, Y).

Another example of SLD-resolution
Example
:- likes(Z, painting).
{X 7 Z, P 7 painting}
:- based(painting, Y), likes(Z, Y).

Back-tracking
I When a branch ends Prolog can back-track over the tree to

search alternative branches
I The previous resolution step is taken back and the next
possible resolvent is generated
I Failure branches back-track automatically
I Solution branches can be back-tracked from on request
I Back-tracking can be stopped by using the cut predicate,
written !, which means do not back-track beyond this point
Example of back-tracking
Example
append([], L, L).
append([X | L], Y, [X | Z]) :- append(L, Y, Z).
The goal :- append(X, [1, 2], U). produces the following

solutions:
I {X 7 [], U 7 [1, 2]}.
I {X 7 [X1], U 7 [X1, 1, 2]}.
I {X 7 [X1, X2], U 7 [X1, X2, 1, 2]}.
I ...
Example of back-tracking continued
Example
:- append(X, [1, 2], U).
{X 7 [], U 7 [1, 2]} {X 7 [X1 | L1], U 7 [X1 | Z1], Y1 7 [1, 2]}
:- append(L1, [1, 2], Z1).
{L1 7 [], Z1 7 [1, 2]} {L1 7 [X2 | L2], Z 7 [X2 | Z2], Y2 7 [1, 2]}
:- append(L2, [1, 2], Z2).
{L2 7 [], Z2 7 [1, 2]}
.
.
.
Example of non-termination
Since Prolog searches the tree using the program clauses in the
order in which they are written, and in a depth-first manner, it is
important to put base clauses before recursive clauses.
Example
append([X|L],Y,[X|Z]) :- append(L,Y,Z).
append([],L,L).
This program produces no solutions and will result in an error,

because Prolog will attempt to construct an infinite branch by
using the recursive clause in each resolution step.
Example of non-termination continued
Example
:- append(X, [1, 2], U).
{X 7 [X1 | L1], U 7 [X1 | Z1], Y1 7 [1, 2]}
:- append(L1, [1, 2], Z1).
{L1 7 [X2 | L2], Z 7 [X2 | Z2], Y2 7 [1, 2]}
:- append(L2, [1, 2], Z2).
..
.
Exercise
Consider the following program:
length([], 0).
length([H | T], N) :- length(T, M), N is 1 + M.
Give the SLD-resolution tree for the derivation of the goal

:- length([2, 3], X).
Remember that [2, 3] is an abbreviation of [2 | [3 | []]].

Solution
Example
:- length([2 | [3 | []]], X).
{H 7 2, T 7 [3 | []], X 7 N}
:- length([3 | []], M), N is 1 + M.
{H1 7 3, T1 7 [], N1 7 M}
:- length([], M1), M is 1 + M1, N is 1 + M.
{M1 7 0}
:- M is 1 + 0, N is 1 + M.
{M 7 1}
:- N is 1 + 1.
{N 7 2}

Programming Language Design Paradigms: Logic Programming: Part 2 - Semantics

Uploaded by

Copyright:

Available Formats

Programming Language Design Paradigms: Logic Programming: Part 2 - Semantics

Uploaded by

Document Information

Original Description:

Original Title

Copyright

Available Formats

Share this document

Share or Embed Document

Sharing Options

Did you find this document useful?

Is this content inappropriate?

Copyright:

Available Formats

Programming Language Design Paradigms: Logic Programming: Part 2 - Semantics

Uploaded by

Copyright:

Available Formats

Programming Language Design Paradigms

Logic Programming: Part 2 - Semantics

Maribel Fernandez and Elliot Fairweather

I Use formulae to express knowledge and describe problems

I Theory: unification and SLD-resolution

I A unification algorithm was first sketched by Jacques

I A unification problem U is a set of equations between terms

I A solution to U, also called a unifier, is a substitution , such

I The unification algorithm finds the mgu for a unification

(1) f (s1 , . . . , sn ) = f (t1 , . . . , tn ), E s1 = t1 , . . . , sn = tn , E

(2) f (s1 , . . . , sn ) = g (t1 , . . . , tm ), E failure

I The unification algorithm applies the rules in a

Solve the following unification problem:

{f (g (a), b) = f (X , b), X = g (Z ), f (a, Y ) = f (Z , Y )}

{f (g (a), b) = f (X , b), X = g (Z ), f (a, Y ) = f (Z , Y )}

I In order to prove a goal B1 , . . . , Bn with respect to a set P of

I S selection rule: at each resolution step a fixed computation

1. SLD-resolution is refutation-complete: given a program and a

I Given a goal clause G1 , G2 , . . . , Gk , we select an atom Gi of

I Since there might be several clauses in the program that can

I Prolog always selects the leftmost literal in the goal

:- based(prolog, Y), likes(Z, Y).

:- based(logic, Y), likes(Z, Y).

:- based(painting, Y), likes(Z, Y).

I When a branch ends Prolog can back-track over the tree to

The goal :- append(X, [1, 2], U). produces the following

{X 7 [], U 7 [1, 2]} {X 7 [X1 | L1], U 7 [X1 | Z1], Y1 7 [1, 2]}

:- append(L1, [1, 2], Z1).

:- append(L2, [1, 2], Z2).

{L2 7 [], Z2 7 [1, 2]}

This program produces no solutions and will result in an error,

:- append(X, [1, 2], U).

{X 7 [X1 | L1], U 7 [X1 | Z1], Y1 7 [1, 2]}

:- append(L1, [1, 2], Z1).

{L1 7 [X2 | L2], Z 7 [X2 | Z2], Y2 7 [1, 2]}

:- append(L2, [1, 2], Z2).

Consider the following program:

Give the SLD-resolution tree for the derivation of the goal

Remember that [2, 3] is an abbreviation of [2 | [3 | []]].

:- length([3 | []], M), N is 1 + M.

:- length([], M1), M is 1 + M1, N is 1 + M.

You might also like