Next: , Previous: Exception handling, Up: Top   [Contents]


15 Formal semantics

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 semantics. In this semantics, the program is executed top-down using SLDNF resolution (or something equivalent), starting from ‘main/2’ preceded by any module initialisation goals (as per Module initialisation), and followed by any module finalisation goals (as per Module finalisation). Function calls, 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: the sub-goals are reordered, not split and interleaved. Function application is strict, not lazy. Predicate calls are strict in the sense that goals will be executed irrespective of any mode-determinism assertions, even if they loop, are ‘erroneous’, or are ‘det’ and contain no outputs.

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

There is another operational semantics of Mercury programs called the strict commutative semantics. This semantics is equivalent to the strict sequential 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 differ each time a particular goal is entered.

As well as providing the strict sequential semantics, Mercury implementations may provide one or more implementation-defined operational semantics, as long as any such implementation-defined operational semantics is at least as complete as the strict commutative semantics. An implementation-defined operational semantics is “at least as complete” as the strict commutative semantics if and only if the implementation-defined operational 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 function calls, conjunctions and disjunctions).

Thus, to summarize, there are in fact a variety of different operational semantics for Mercury. One of them, the strict sequential semantics, is deterministic—the behaviour is always specified exactly. Programs are executed top-down, mode analysis does “minimal” reordering (in a precisely defined sense), function calls, conjunctions and disjunctions are executed depth-first left-to-right, and function and predicate 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 be non-deterministic) as long as they are sound with respect to the declarative semantics, and meet a minimum level of completeness.

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. In some ways this is not 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. On the other hand, if you do write code which works for all possible executions under the strict commutative semantics, then you can be guaranteed that it will work correctly on every implementation, under every possible implementation-defined operational semantics.

The Melbourne Mercury implementation offers eight different operational semantics, which can be selected with different combinations of the following options:

--no-reorder-conj

Only do minimal reordering of conjunctions.

--no-reorder-disj

Do not reorder disjunctions.

--no-fully-strict

Predicate calls are not strict (function application is always strict in the current implementation). This option allows the compiler to improve completeness by optimizing away infinite loops, goals with determinism erroneous, and goals with determinism det and no outputs.

The default semantics is the strict commutative semantics. The strict sequential semantics can be selected with the ‘--no-reorder-conj’ and ‘--no-reorder-disj’ options.

Future implementations of Mercury may wish to offer other implementation-defined 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: , Previous: Exception handling, Up: Top   [Contents]