Basic goals

The bodies of predicates and functions are goals. Here are the basic types of goals.

Predicate call

A predicate call has the form:

predicate_name(TERM1, ..., TERM)

There are no function call goals, but function calls occur as terms inside other goals.

Unification

A unification goal has the form:

TERM1 = TERM2

Unifications are used for assignments, constructing and deconstructing compound terms, and testing equality.

Inequality goal

An inequality goal has the form:

TERM1 \= TERM2

It is an abbreviation for not (TERM1 = TERM2). See negation below.

Conjunction

A conjunction is a sequence of goals separated by the comma operator:

GOAL1, GOAL2, ... , GOALn

For example, a sequence of calls:

p(X), q(Y), r(Z)

The declarative semantics is that the conjunction is true if all of the conjuncts are true. Operationally, the goals are executed in some order, not necessarily depth-first left-to-right order. The compiler may reorder conjuncts in order to satisfy mode constraints, or for other reasons.

Disjunction

A disjunction is a sequence of goals separated by the semicolon operator:

GOAL1 ; GOAL2 ; ... ; GOALn

The semicolons are usually written at the start of the line to make disjunctions easy to spot, as in:

(
    p(X)
;
    q(X)
;
    r(X)
)

The declarative semantics is that the disjunction is true if any of the disjuncts is true. Operationally, one of the disjuncts will be executed first to produce a solution. The program may backtrack into that disjunct to find the next solution, and so on, until that disjunct has no more solutions and fails. Then another disjunct would be executed. When there are no more solutions, the disjunction as a whole fails.

If a variable bound within a disjunction is used outside the disjunction, then that variable must be bound in all disjuncts for which it is possible to reach the end of the disjunct.

This is invalid:

(
    Animal = dog,
    Food = dog_food
;
    Animal = cat
    % error: Food not bound here
),
feed(Animal, Food)

But this is valid:

(
    Animal = dog,
    Food = dog_food
;
    Animal = cat,
    fail
),
feed(Animal, Food)

Switch

A switch is a special case of disjunction where each disjunct has, near its start, a unification that tests the same bound variable against a different function symbol. (The reference manual has details of switch detection.)

This is a switch on Animal assuming Animal is input to the disjunction:

(
    Animal = dog,
    pet_doggy(Animal)
;
    Animal = cat,
    pet_kitty(Animal)
)

A switch is complete if it covers all the possible function symbols of the switched-on variable. Otherwise, the switch may fail. If the type of Animal has another constructor in its definition (say, bird) then the switch in the previous example would be incomplete.

We prefer switches over if-then-elses, whenever practical.

true & fail

true is a goal that always succeeds. It is equivalent to the empty conjunction.

fail is a goal that always fails. It is equivalent to the empty disjunction.

false is synonym for fail with a more declarative flavour.

Negation

Negation goals have either of the forms:

not GOAL

\+ GOAL

The \+ operator is supposed to resemble a negated ⊢ symbol.

Both forms are equivalent to if GOAL then fail else true.

You cannot bind a variable in a negated goal, then use that variable outside the negation. This is invalid:

not likes(Person, Food),    % Food bound in negated goal
eat(Person, Food)           % error: Food not bound here

If-then-else

An if-then-else goal has either of the forms:

( if CONDGOAL then THENGOAL else ELSEGOAL )

( CONDGOAL -> THENGOAL ; ELSEGOAL )

The traditional syntax (C -> T ; E) has a slight disadvantage in that the semicolon can be mistaken for a disjunction operator.

A chain of if-then-else goals can be written like this:

( if some_condition then
    ...
else if some_other_condition then
    ...
else
    ...
)

The declarative semantics of an if-then-else is given by ( CONDGOAL, THENGOAL ; not(CONDGOAL), ELSEGOAL) but the operational semantics are different, and it is treated differently for the purposes of determinism inference. Operationally, it executes the CONDGOAL, and if that succeeds, then execution continues with the THENGOAL; otherwise, i.e. if CONDGOAL fails, it executes the ELSEGOAL.

Execution can backtrack into CONDGOAL. Unlike Prolog, Mercury's if-then-else does not commit to the first solution of the condition if the condition succeeds.

It is not allowed to bind a variable in CONDGOAL that is also used outside of the if-then-else goal. However, the CONDGOAL may bind variables used in THENGOAL.

This is invalid:

( if likes(Person, Food) then   % error: condition binds non-local variable
    true
else
    Food = dog_food
),
eat(Person, Food)

The correct way to write it is:

( if likes(Person, Food0) then  % Food0 is local to condition and then-goal
    Food = Food0
else
    Food = dog_food
),
eat(Person, Food)

Similarly to a disjunction, if a variable bound in an if-then-else goal is used outside the goal, then the variable must be bound in both the THENGOAL and the ELSEGOAL (except when the end of either goal is not reachable). This is invalid:

( if likes(Person, Food0) then
    Food = Food0
else
    true    % error: Food must also be bound here
),
eat(Person, Food)

Higher-order call

A higher-order call may be written as:

call(Closure, Arg1, ..., ArgN)

A higher-order call may also be written as:

Var(Arg1, ..., ArgN)

where Var is a variable. (Actually, the compiler accepts a higher-order term in the Var position as well.)

We'll discuss higher-order programming later.

Existential quantification

An existential quantification goal introduces a new scope. It looks like:

some [Var1, ..., VarN] GOAL

The variables listed between the square brackets are local to the goal. A variable with one of the listed names inside the goal is considered distinct from a variable with the same name outside the goal.

some [X] (
    foo(X)
),
bar(X)

The two occurrences of X are considered to be distinct variables. In this case, the compiler will warn about the variables having overlapping scopes.

Mercury's rules for implicit quantification mean that variables are often implicitly existentially quantified (see the reference manual for details). There is usually no need to write existential quantifiers explicitly.

Perhaps the most common reason to use an existential quantification goal is to introduce a new state variable, like this:

some [!X] (
    init(!:X),
    do_one_thing(!X),
    do_another_thing(!X),
    do_third_thing(!X),
    FinalX = !.X
)

Universal quantification

A universal quantification goal looks like:

all [Var1, ..., VarN] GOAL

It is an abbreviation for not (some [Var1, ..., VarN] not GOAL).

The only common use of universal quantification goals is in this pattern:

all [X] ( p(X) => q(X) )

That checks if q(X) holds for every X in which p(X) holds.

Implication and bi-implication

These goals are not commonly used.

• implication

  GOAL1 => GOAL2 is an abbreviation for not (GOAL1, not GOAL2).

• reverse implication

  GOAL1 <= GOAL2 is an abbreviation for not (GOAL2, not GOAL1).

• logical equivalence

  GOAL1 <=> GOAL2 is an abbreviation for (GOAL1 => GOAL2), (GOAL1 <= GOAL2).

Other goals

There are a few more goal types, to be discussed in time.

• purity cast - purity system
• determinism cast - committed-choice determinism
• determinism check - to enhance the robustness of code
• switch completeness check - to enhance the robustness of code
• disable_warnings
• trace goals - debugging or logging
• try goal - exceptions
• parallel conjunction
• event goal