-
Notifications
You must be signed in to change notification settings - Fork 54
Predicates and functions
Let's take a closer look at predicates and functions.
Nearly every logic programming tutorial starts with a genealogy example, and this one is (unfortunately) no different. The examples on this page will make use of this type that names some people.
:- type person
---> ada
; bob
; dan
; ema
; fay
; joe.Predicates and functions are defined with clauses with the forms:
predicate_name(ARG1, ..., ARGN) :- BODY.
function_name(ARG1, ..., ARGN) = RESULT :- BODY.Predicates with the same name but numbers of arguments are considered
different predicates, and similarly for functions. We often refer to
predicates or functions as name/arity, e.g. foo/3, meaning
the predicate or function foo with 3 arguments.
The stuff to the left of the :- symbol is the clause head.
The arguments in the clause head are terms, not limited to variables.
If there are no arguments then the parentheses must be left out.
When a predicate or function is called, the arguments of the call are
unified with the corresponding terms in the clause head.
A clause without a body is a fact. The :- symbol is also left out.
Examples:
female(ada).
female(ema).
female(fay).
male(bob).
male(dan).
male(joe).
parent(ada, dan).
parent(bob, dan).
parent(dan, fay).
parent(ema, fay).
parent(dan, joe).
parent(ema, joe).We see that a predicate or function can be defined with multiple clauses. So we have facts stating that:
- "Ada is female", "Ema is female", "Fay is female"
- "Bob is male", etc.
- "Ada is a parent of Dan", etc.
A clause with a body is a rule which states that the head of the rule is
true provided that the body of the rule is true.
The :- symbol is supposed to resemble the reversed implication operator ←.
The body is a goal, such as the call or conjunction goals that we have seen.
father(P, C) :-
parent(P, C),
male(P).
mother(P, C) :-
parent(P, C),
female(P).
grandparent(PP, C) :-
parent(PP, P),
parent(P, C).Therefore, we have rules stating these relations:
- For all P and C, P is a father of C if P is a parent of C and P is male.
- For all P and C, P is a mother of C if P is a parent of C and P is female.
- For all PP and C, PP is a grandparent of C if PP is a parent of P, and P is a parent of C.
A fact is equivalent to a rule in which the body is always true.
Functions can also be defined with multiple clauses and function rules. Examples:
mass_kg(ada) = 55.0.
mass_kg(bob) = 72.0.
% etc.
height_m(ada) = 1.65.
height_m(bob) = 1.80.
% etc.
bmi(Person) = Mass / (Height * Height) :-
Mass = mass_kg(Person),
Height = height_m(Person).So a Mercury program consists of a set of clauses. How does it work? The following is a brief example. (It would be useful to have a look at the formal basis of logic programming later.)
At any time, the program has a goal that it is trying to solve (prove).
If the goal is mother(M, fay) then the objective is to find a
substitution for M that makes the goal true.
There is a single rule for mother/2:
mother(P, C) :- parent(P, C), female(P).We can unify mother(M, fay) with the head of the clause.
The body of the rule gives us a new goal to solve,
parent(M, fay), female(M).
Logically, the order of operands in a conjunction does not matter,
but we'll attempt the goals left-to-right.
There are multiple clauses for parent/2 and two of them can match
parent(M, fay). This introduces the need to search for a solution.
In Mercury the search strategy is to try one alternative at a time and
backtrack as necessary.
One solution of parent(M, fay) is parent(dan, fay). If we substitute
dan for M, we just need to prove female(dan).
There is no clause that would allow us to make that conclusion,
so we cannot prove that mother(dan, fay).
There was potentially another solution to parent(M, fay) to consider,
so let's backtrack to that point. The next solution is parent(ema, fay).
Substituting ema for M, we are left to prove female(ema).
There is a fact stating exactly that, so now we have a solution
mother(ema, fay) to the original goal mother(M, fay).
Previously, we saw an example of a predicate declaration:
:- pred main(io::di, io::uo) is det.That is a pred-mode declaration, a common shorthand for two separate declarations:
:- pred main(io, io).
:- mode main(di, uo) is det.A :- pred declaration gives the type of the predicate, including its
arguments.
A :- mode declaration gives a single mode of the predicate and its
associated determinism category.
We can declare the types of our example predicates, without the mode information, as:
:- pred female(person).
:- pred male(person).
:- pred parent(person, person).
:- pred father(person, person).
:- pred mother(person, person).
:- pred grandparent(person, person).Look again at one of the calls from before, parent(M, fay). The second
argument is an input, and we are looking for an output in the first
argument position. Does that mean we can call any predicate with any
combination of input and output arguments we like? Unfortunately not!
In practice, most predicates can only work in one direction.
A mode declaration declares an assignment of input and output arguments to a predicate or function (this is a simplification, but goes a long way). The compiler will analyse each mode of a predicate or function separately to ensure that it can be compiled, or otherwise reject it. Each mode of a predicate or function is also called a "procedure".
We can declare multiple modes for the parent/2 predicate.
:- mode parent(in, in).
:- mode parent(in, out).
:- mode parent(out, in).
:- mode parent(out, out).So in fact, all four combinations of in and out arguments are
possible. What a surprise.
We can call the parent(in, in) mode to check if a given person is a
parent of another given person. An example of a call to this mode is
parent(ada, dan).
We can call the parent(in, out) mode to find the children of a known
person, if any. An example of a call to this mode is parent(ema, X),
which succeeds with X = fay or X = joe.
We can call the parent(out, in) mode to find the parents of a known
child, if known. An example of a call to this mode is parent(X, joe),
which succeeds with X = dan or X = ema.
Finally, we can call the parent(out, out) mode to enumerate all known
parent-child relationships in the program.
Note that a predicate cannot be declared with a combined pred-mode declaration as well as separate mode declarations, and similarly for functions.
It is possible to call a procedure with an argument that is more bound
than required by the argument mode. If there is only a p(out) mode,
you can call p(X) with X already bound to a value, as if there was
an additional p(in) mode. The compiler will insert an additional
unification, transforming the code to p(Y), X = Y with a fresh
variable Y.
There is a step in compilation of a Mercury program called mode analysis. It checks one mode of a predicate or function at a time, keeping track of the instantiation state of each variable as it progresses, that is, whether a variable is bound or not. At a call, it needs to select a mode of the predicate or function to call, based on the instantiatedness of the arguments.
Imagine the mode analysis has reached this goal, a conjunction of two calls, and the variable X is free (not bound):
p(X), q(X)Say the predicate p/1 has a single mode p(in). Since X is free,
the call to the p(in) mode cannot go ahead. However, mode analysis
can defer the call, and try the call q(X) first. If q/1 has a mode
q(out), then that mode can be selected for the q(X) goal. After the
call returns X will be bound, so mode analysis can attempt to schedule
the call p(X) afterwards.
That might give you an idea of how a single definition of a predicate may be called in different modes.
For every mode of a predicate or function, there is an associated determinism category according to the number of solutions it may produce, and whether it may fail without producing any solution.
If all possible calls to a mode of a predicate or function which return to the caller
-
have exactly one solution, then that mode is det
-
either have no solutions or have one solution, then that mode is semidet
-
have one or more solutions, then that mode is multi
-
have zero or more solutions, then that mode is nondet
-
fail without producing a solution, then that mode has determinism failure
If no possible calls to a mode of a predicate or function can return to the caller (e.g. because it throws an exception), then that mode has determinism erroneous.
Now that we know all that, we can declare the modes of the parent/2
predicate with their determinisms as well:
:- mode parent(in, in) is semidet.
:- mode parent(in, out) is nondet.
:- mode parent(out, in) is nondet.
:- mode parent(out, out) is multi.nondet is more general than the other determinism categories, so why bother declaring tighter determinisms? They allow the compiler to generate more efficient code; supporting backtracking has a cost. If the compiler infers a different determinism from what you declared, that's often a good sign that there is a mistake somewhere. Determinism declarations are good documentation for human readers, too, like other declarations.
There are two more, "committed choice" determinism categories. cc_multi and cc_nondet are like multi and nondet, respectively, but will arbitrarily commit to a single solution, and prevent backtracking to find further solutions. Sometimes one solution is as good as any other.
Only det and cc_multi predicates can perform I/O as backtracking over I/O is not allowed.
Function type and mode declarations are similar to those of predicates. They look like this:
:- func min(int, int) = int.
:- mode min(in, in) = out is det.You can combine the two declarations together as well:
:- func min(int::in, int::in) = (int::out) is det.If there is no mode declaration for a function then the compiler will
assume a default mode in which all arguments have mode in and the
result has mode out, and the determinism is det.
Multiple modes of a function are possible, though rare. An example is
the addition function in the int module.
(Remember that uo means "unique output".)
:- func int + int = int.
:- mode in + in = uo is det.
:- mode uo + in = in is det.
:- mode in + uo = in is det.Forward modes of a function (i.e. all arguments are fully input, result is output) can only have determinisms det, semidet, erroneous, or failure. Nondeterministic forward modes would break referential transparency.
Furthermore, functions with determinism semidet and failure are
discouraged even though the language allows them.
Consider that the goal f = f can fail if f can fail.
Phew! That was a lot to cover, and we went over it all very briefly so as not to get bogged down. Hopefully once you see more code it will start to make sense.
Some points to take away:
-
predicates and functions are defined by one or more clauses
-
predicates and functions are declared with type and mode declarations
-
a mode declaration assigns inputs and output arguments to a predicate or function
-
a determinism declaration indicates the number of solutions that a mode of a predicate or function may produce
-
backtracking is employed to explore multiple solutions
Here is the code of the family tree example for your copy-pasting pleasure.
:- module family.
:- interface.
:- import_module io.
:- pred main(io::di, io::uo) is det.
:- implementation.
:- import_module list.
:- import_module solutions.
:- type person
---> ada
; bob
; dan
; ema
; fay
; joe.
:- pred female(person).
:- mode female(in) is semidet.
:- mode female(out) is multi.
female(ada).
female(ema).
female(fay).
:- pred male(person).
:- mode male(in) is semidet.
:- mode male(out) is multi.
male(bob).
male(dan).
male(joe).
:- pred parent(person, person).
:- mode parent(in, in) is semidet.
:- mode parent(in, out) is nondet.
:- mode parent(out, in) is nondet.
:- mode parent(out, out) is multi.
parent(ada, dan).
parent(bob, dan).
parent(dan, fay).
parent(ema, fay).
parent(dan, joe).
parent(ema, joe).
:- pred father(person, person).
:- mode father(in, in) is semidet.
:- mode father(in, out) is nondet.
:- mode father(out, in) is nondet.
:- mode father(out, out) is nondet.
father(P, C) :-
parent(P, C),
male(P).
:- pred mother(person, person).
:- mode mother(in, in) is semidet.
:- mode mother(in, out) is nondet.
:- mode mother(out, in) is nondet.
:- mode mother(out, out) is nondet.
mother(P, C) :-
parent(P, C),
female(P).
:- pred grandparent(person, person).
:- mode grandparent(in, in) is semidet.
:- mode grandparent(in, out) is nondet.
:- mode grandparent(out, in) is nondet.
:- mode grandparent(out, out) is nondet.
grandparent(PP, C) :-
parent(PP, P),
parent(P, C).
main(!IO) :-
% The first argument to solutions is a closure.
% solutions/2 returns all the solutions produced by the closure
% as a list.
solutions(
(pred(PP::out) is nondet :-
grandparent(PP, fay)
),
PPs),
(
PPs = [],
write_string("fay has no known grandparents\n", !IO)
;
PPs = [_ | _],
write_string("fay has these known grandparents: ", !IO),
write(PPs, !IO),
nl(!IO)
).