Previous: Declarative semantics, Up: Introduction to declarative programming [Contents]
Execution in Mercury starts with a goal. This is a proposition that may contain some variables, and the aim of execution is to find a substitution for which the proposition is true. If it does, we refer to this as success, and we refer to the substitution that was found as a solution. If execution determines that there are no such substitutions, we refer to this as failure.
Say, for example,
we start with a goal of ‘N = length([1, 2])’.
Function evaluation is strict,
depth-first, and left-to-right,
so we want to call the length/1
function first.
To do this, we match the argument with
the heads of the clauses that define the function
to find the clause that is applicable.
In this case the second clause matches,
with the substitution of Xs → [2]
(the substitution for ‘_’ is irrelevant,
since any other occurrence of ‘_’
is considered a distinct variable).
Applying this substitution to the body
then replacing it in the goal gives us a new goal,
namely ‘N = 1 + length([2])’.
Repeating this process a second time
gives us the goal ‘N = 1 + 1 + length([])’.
When we call the function the third time
it will match the first clause,
and the new goal will be ‘N = 1 + 1 + 0’.
Now we can evaluate the ‘+/2’ calls
and get a result of ‘N = 2’.
It is trivial to find a substitution that makes this proposition true:
just map N
to the constant 2
.
Now consider the goal ‘append(As, Bs, [1])’.
In this case the first two arguments are free,
meaning that they are variables that
are not mapped to anything in the current substitution,
and the third argument is ground,
meaning that it doesn’t contain any variables
after applying the current substitution.
As before we try to match (or unify) the goal with a clause,
but in this case both clauses match!
We arbitrarily pick the first one,
but we also push a choice point onto a stack,
which will allow us to return to this point later on
and try the other clause if we need to.
Matching with the first clause gives us
the substitution As → [], Bs → [1]
.
Since this clause is a fact,
we succeed with this substitution as our solution.
If a later goal fails,
we pop the previous choice point off the stack
in order to search for a different solution.
This time we want to try unifying our goal with
the head of the second clause.
That is, we want to find a substitution such that
append(As, Bs, [1]) = append([X1 | As1], Bs1, [X1 | Cs1])
.
(The variables from the clause have been given a numerical suffix,
which is to indicate that they came from a different scope
and are not the same variables as those in the goal.)
The substitution we use is
As → [1 | As1], Bs → Bs1, X1 → 1, Cs1 → []
;
you can check that this does indeed unify the two terms.
Note that information is effectively flowing in both directions:
variables from both the goal and the clause
(i.e. the caller and callee) are bound by this substitution.
This is a key difference from pattern matching in many other languages,
in which only variables in the pattern are bound.
Applying this substitution to the body of the selected clause
gives us our new goal,
‘append(As1, Bs1, [])’.
This time only the first clause matches,
with the substitution of As1 → [], Bs1 → []
.
The clause is a fact,
so this is a solution to this call to append.
To find the solution to the parent goal we compose this substitution
with the one from before,
giving As → [1], Bs → []
.
We have now found two solutions for our goal:
one with As
being the empty list and Bs
being [1]
,
and the other with the bindings for As
and Bs
swapped.
These are all of the possible solutions;
if we wanted to search for another
we would find the choice point stack to be empty,
hence we would fail.
One final observation is worth making before we finish this section. We saw earlier that the arguments at the start of the call were either free or ground; in each solution we see that the arguments are all ground. We consider arguments that are ground at the start to be inputs, and arguments that are free at the start and ground at the end to be outputs. The pattern of inputs and outputs for a predicate or function call is known as its mode; we can declare the mode we have used here as follows.
:- mode append(out, out, in) is multi.
More information can be found in later chapters; also, see the Mercury Library Reference Manual for the full set of modes declared for ‘append/3’.
Previous: Declarative semantics, Up: Introduction to declarative programming [Contents]