[mercury-users] Doubt about determinism checking

[Mark Brown]

Hi Alex,

On 19-Jul-2011, Alexsandro Soares <prof.asoares at gmail.com> wrote:
> Hi,
> 
>    I'm trying to make a predicate that converts a formula with complex
> literals into a formula with primitive literals.  For example, using the
> facts informed in predicate "definition" (in module defs.m), I could convert
> the complex formula
> 
>      and(literal("A"), literal("G"))
> 
> into
> 
>    and(and(literal("B"),
>                  not(or(literal("D"),
>                            literal("E")))),
>           or(literal("H", literal("J"))))
> 
> Each complex literal can only be defined one time, so the predicate
> "definition" can provide, at most, one answer.

You mean, for any fixed literal on the left hand side there is at most one
answer.  If you allow the left hand side to vary, there are three answers -
one for each clause.  Since you declare the entire argument as `out', it's
the latter case that the Mercury compiler is checking.

In theory Mercury can express the constraint that there is at most one
solution once the left hand side is fixed.  E.g.:

    :- inst query_lhs
        --->    equiv(ground, free)
        ;       formula(ground).

    :- pred definitions(query::(query_lhs >> ground)) is semidet.

In practice, however, such "partially instantiated data structures" are not
supported very well, and the usual approach is to factor predicates so
that each argument is either `in' or `out'.  E.g.:

    :- pred definitions(formula::in, formula::out) is semidet.

    :- pred facts(formula::in) is semidet.

> Similarly, the predicate
> "expand" can only provide exactly one expansion for each formula.

In this case, Mercury can see that `literal(X)' is ground in the call to
definition, but without the more precise mode information it can't infer
that X1 is always bound to the same value.  So another solution is to
declare definitions to be `multi' but promise X1 is always the same with

    promise_equivalent_solutions [X1]
        definition(equiv(literal(X), X1))

This lets the compiler commit to the first solution (which is better than
using solutions/2, as suggested by Vladimir, since it stops as soon as the
first solution is found instead of continuing until failure).

Cheers,
Mark.


--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------