[m-users.] Performance of solutions module

[Zoltan Somogyi]

On Mon, 5 Nov 2018 08:15:15 -0500, Charlie McGee <c4cypher at gmail.com> wrote:
> Thank you for the clarification on this. I am still learning. I'm starting
> to get a decent grasp of how the language works in a single solution
> context, but I'm still learning how the compiler handles nondet code.  One
> of my biggest points of confusion/frustration is how cc_multi and cc_nondet
> work exactly, the semantics of the comitted choice modes.  Do they work in
> terms of a greedy 'first result is good enough if called in a single
> solution context'?  I need to work on my understanding on how det code
> works with nondet code.

There are two kinds of semantics that are relevant here. One is the
declarative semantics: what a piece of code is supposed to mean.
The other is the operational semantics: what the compiled version
of that code actually does. Mercury is a declarative language
because in almost all cases, the compiler is required to ensure
that the operational semantics matches the declarative semantics.

Committed choice code is one of the main exceptions.

Consider a predicate that may have more than one solution in a given
mode according to its declarative semantics. In the usual case of that
mode of the predicate being declared to be nondet or multi,
the compiler is required to generate code that returns every
one of those solutions, one at a time. In this case, the declarative
and operational semantics match.

If that mode of the predicate is instead declared cc_nondet or cc_multi,
then the compiler will generate code that returns at most one solution.
The fact that the rest of the solutions will not be returned is in this case
a deliberate difference between the operational semantics and the usual
declarative semantics.

The one solution that will be returned will be the one that is computed first.
The declarative semantics works in terms of sets of solutions and has
no notion of an order between solutions, but the operational semantics
works in terms of resolution steps, and it *does* know about order.
The order implemented by the Mercury compiler is the standard logic
programming order, with earlier disjuncts being executed before later disjuncts.

There are several kinds of situations in which this difference (and therefore
committed choice determinisms) are useful.

The first is when the piece of code whose determinism we are talking about
may have more than one solution, but we do not care about the differences
between solutions. For example, it is fairly common to have code that
looks like this:

    ( if
        some [Item] (
            list.member(Item, Items),
            item_has_property_x(Item)
        )
    then
        ...
    else
        ...
    )

In this case, all solutions of the code inside the existential quantification
are equivalent, since the code outside the quantification cannot access
the solution; all that this code cares about is the existence or nonexistence
of a solution.

A more subtle version of this is abstract data types with nonstandard
equality theories. Consider a predicate that converts a list of ints
to a binary search tree (BST) containing those ints. Given any nontrivial
list of ints, there will be more than one BST containing those ints.
The standard declarative semantics would require the conversion
predicate to return every one of those forms one at a time.
Mercury allows programmers to use user-defined equality and
committed choice determinisms to tell the compiler that
in the user's intended declarative semantics, all the BSTs whose
in-order traversal yields the original list are equivalent, so having
the conversion predicate returning just one such BST  is fine.
(I mention this only for completeness; most Mercury users
won't use user defined equality.)

Another situation is when the job of the predicate is inherently
operational. The benchmarking predicates in the benchmarking
module of the Mercury standard library invoke the predicate
being benchmarked and return not just its output, but also
a number giving the time taken to execute that predicate.
In the declarative semantics, the benchmarking predicate
has infinite number of solutions, with each solution pairing
the actual result of the predicate under test with all the possible
times. Actually implementing that declarative semantics
would therefore yield an infinite loop, and would also be totally
useless: the user knows the set of possible execution times
is infinite (it can be 0 milliseconds, 1 ms, 2 ms etc), and he/she
calls the benchmarking predicate because he/she wants to know
which is the *actual* execution time of *this* invocation.
(Other invocations may take a different amount of time.)
So the benchmarking predicate is cc_multi; it returns exactly one
of the possible times, the one that this invocation took.
Mercury's rules about what sorts of contexts may contain
committed choice code are intended to prevent such inherently
operational choices affecting the computation of solutions
for non-committed-choice predicates.

Zoltan.