Next: Foreign language interface, Previous: Exception handling, Up: Top [Contents]

A legal Mercury program is one that complies with the syntax, type, mode, determinism, and module system rules specified in earlier chapters. If a program does not comply with those rules, the compiler must report an error.

For each legal Mercury program, there is an associated predicate calculus theory whose language is specified by the type declarations in the program and whose axioms are the completion of the clauses for all predicates in the program, plus the usual equality axioms extended with the completion of the equations for all functions in the program, plus axioms corresponding to the mode-determinism assertions (see Determinism), plus axioms specifying the semantics of library predicates and functions. The declarative semantics of a legal Mercury program is specified by this theory.

Mercury implementations must be sound: the answers they compute must be true in every model of the theory. Mercury implementations are not required to be complete: they may fail to compute an answer in finite time, or they may exhaust the resource limitations of the execution environment, even though an answer is provable in the theory. However, there are certain minimum requirements that they must satisfy with respect to completeness.

There is an operational semantics of Mercury programs called the
*strict sequential* operational semantics. In this semantics,
the program is executed top-down, starting from ‘`main/2`’
preceded by any module initialisation goals
(as per Module initialisation), followed by any module finalisation
goals (as per Module finalisation),
and function calls within a goal, conjunctions and disjunctions are all
executed in depth-first left-to-right order.
Conjunctions and function calls are “minimally” reordered as required
by the modes:
the order is determined by selecting the first mode-correct sub-goal
(conjunct or function call),
executing that, then selecting the first of the remaining sub-goals
which is now mode-correct, executing that, and so on.
(There is no interleaving of different individual conjuncts or function calls,
however; the sub-goals are reordered, not split and interleaved.)
Function application is strict, not lazy.

Mercury implementations are required to provide a method of processing Mercury programs which is equivalent to the strict sequential operational semantics.

There is another operational semantics of Mercury programs called
the *strict commutative* operational semantics. This semantics
is equivalent to the strict sequential operational semantics except
that there is no requirement that function calls, conjunctions and disjunctions
be executed left-to-right; they may be executed in any order, and may
even be interleaved. Furthermore, the order may even be different each
time a particular goal is entered.

As well as providing the strict sequential operational semantics, Mercury implementations may optionally provide additional implementation-defined operational semantics, provided that any such implementation-defined operational semantics are at least as complete as the strict commutative operational semantics. An implementation-defined semantics is “at least as complete” as the strict commutative semantics if and only if the implementation-defined semantics guarantees to compute an answer in finite time for any program for which an answer would be computed in finite time for all possible executions under the strict commutative semantics (i.e. for all possible orderings of conjunctions and disjunctions).

Thus, to summarize, there are in fact a variety of different operational semantics for Mercury. In one of them, the strict sequential semantics, there is no nondeterminism — the behaviour is always specified exactly. Programs are executed top-down using SLDNF (or something equivalent), mode analysis does “minimal” reordering (in a precisely defined sense), function calls, conjunctions and disjunctions are executed depth-first left-to-right, and function evaluation is strict. All implementations are required to support the strict sequential semantics, so that a program which works on one implementation using this semantics will be guaranteed to work on any other implementation. However, implementations are also allowed to support other operational semantics, which may have non-determinism, so long as they are sound with respect to the declarative semantics, and so long as they meet a minimum level of completeness (they must be at least as complete as the strict commutative semantics, in the sense that every program which terminates for all possible orderings must also terminate in any implementation-defined operational semantics).

This compromise allows Mercury to be used in several different ways.
Programmers who care more about ease of programming and portability
than about efficiency can use the strict sequential semantics, and
can then be guaranteed that if their program works on one correct
implementation, it will work on all correct implementations. Compiler
implementors who want to write optimizing implementations that do lots
of clever code reorderings and other high-level transformations or that
want to offer parallelizing implementations which take maximum
advantage of parallelism can define different semantic models.
Programmers who care about efficiency more than portability can write
code for these implementation-defined semantic models. Programmers who
care about efficiency *and* portability can achieve this by writing
code for the strict commutative semantics.
Of course, this is not
quite as easy as using the strict sequential semantics, since it is
in general not sufficient to test your programs on just one
implementation if you are to be sure that it will be able to use the
maximally efficient operational semantics on any implementation.
However, if you do write code which works for all possible executions
under the strict commutative semantics (i.e. for all possible orderings of
conjunctions and disjunctions), then you can be guaranteed that it
will work correctly on every implementation, under every possible
implementation-defined semantics.

The University of Melbourne Mercury implementation offers eight
different semantics, which can be selected with different
combinations of the ‘`--no-reorder-conj`’, ‘`--no-reorder-disj`’,
and ‘`--no-fully-strict`’ options.
(The ‘`--no-fully-strict`’ option allows the compiler to improve
completeness by optimizing away infinite loops and goals with determinism
`erroneous`

.)
The default semantics are the strict commutative semantics.
Enabling ‘`--no-reorder-conj`’ and ‘`--no-reorder-disj`’ gives the
strict sequential semantics.

Future implementations of Mercury may wish to offer other operational semantics. For example, they may wish to provide semantics in which function evaluation is lazy, rather than strict; semantics with a guaranteed fair search rule; and so forth.

Next: Foreign language interface, Previous: Exception handling, Up: Top [Contents]