[m-rev.] for post-commit review: clarify the documentation of committed choice

[Peter Wang]

On Thu, 29 Jul 2021 19:54:58 +1000 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> For review by anyone.
> 
> Zoltan.

> diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
> index c4fadc448..b4490cc5f 100644
> --- a/doc/reference_manual.texi
> +++ b/doc/reference_manual.texi
...
> +
> +The commit to the first solution means that
> +a piece of @code{cc_nondet} or @code{cc_multi} code
> +can never be asked to generate a second solution.
> +If e.g. a @code{cc_nondet} call is in a conjunction,
> +then no call to its right (after mode reordering) may fail,

Replace "then no call to its right" with
"then no subsequent goal in the conjunction"?

> +because that would ask the committed choice goal for a second solution.
> +The compiler enforces this rule.
> +
> +In the declarative semantics,
> +which solution will be the first is unpredicatable,

unpredictable

> +but in the operational semantics,
> +you @emph{can} predict which solution will be the first,
> +since Mercury does depth-first search
> +with left-to-right execution of clause bodies,
> +though that is not on the source code form of each clause body,
> +but on its form @emph{after} mode analysis reordering
> +to put the producer of each variable before all its consumers.
> +
> +The @samp{committed choice nondeterminism} of a predicate
> +has to be propagated up the call tree,
> +making its callers, its callers' callers, and so on,
> +also @code{cc_nondet} or @code{cc_multi},
> +until either you get to @code{main/2} at the top of the call tree,
> +or you get to a location where you don't have to propagate
> +the committed choice context upward anymore.
> +

> +While @code{main/2} is usually declared to have determinism @code{det},
> +it may also be declared @code{cc_multi}.
> +In the latter case,
> +while the program's declarative semantics may admit more than one solution,
> +the implementation will stop after the first,
> +so alternative solutions to @code{main/2}
> +(and hence also to @code{cc_nondet} or @code{cc_multi} predicates
>  called directly or indirectly from @samp{main/2})
>  are implicitly pruned away.
> -This is one way to achieve ``don't care'' style nondeterminism in Mercury.
> -
> -The other situation in which you may want pruning
> -and committed choice style nondeterminism
> -is when you know that all the solutions returned will be equivalent.
> +This is similar to the ``don't care'' nondeterminism
> +of committed choice logic programming languages such as GHC.

> +
> +One way to stop propagating committed choice nondeterminism
> +is the one mentioned above: if a goal has no non-local output variables
> +(i.e.@ none of the goal's outputs are visible from outside the goal),
> +then the goal's solutions are indistinguishable from the outside,
> +and the implementation will only attempt to satisfy the goal once,
> +whether or not the goal is committed choice.
> +Therefore if a @code{cc_multi} goal has all its output ignored,

outputs

> +then the compiler considers it to be a @code{det} goal,
> +while if a @code{cc_nondet} goal has all its output ignored,

outputs


That's fine otherwise.

Peter