# [mercury-users] Doubt about determinism checking

Wed Jul 20 01:30:38 AEST 2011

```Hi, Alexsandro

Here is how you can make it work:

:- module defs.
:- interface.
:- import_module io.

:- pred main(io::di, io::uo) is det.

:- implementation.
:- import_module string.
:- import_module solutions, list.

:- type formula
--->    and(formula, formula)
;       or(formula, formula)
;       not(formula)
;       literal(string).

:- type query
--->    equiv(formula, formula)
;       formula(formula).

:- pred definition(query::out) is multi.

definition(equiv(literal("A"), and(literal("B"),  not(literal("C"))))).
definition(equiv(literal("C"), or(literal("D"), literal("E")))).
definition(equiv(literal("G"), or(literal("H"), literal("J")))).

:- pred definition_by_literal(string::in, formula::out) is semidet.
definition_by_literal(LitName, Formula) :-
solutions.solutions(pred(F::out) is nondet :-
definition(equiv(literal(LitName), F)), [Formula|_]).

:- func expand(formula) = formula.

expand(F) = ExF :-
( F = and(A,B),    ExF = and(expand(A), expand(B))
; F = or(A,B),       ExF = or(expand(A), expand(B))
; F = not(A),         ExF = not(expand(A))
; F = literal(X),
( if definition_by_literal(X,X1)
then X1 = X2, ExF = expand(X2)
else ExF = literal(X)
)
).

main(!IO) :-
X = and(literal("A"), literal("G")),
io.print(expand(X),!IO),
io.nl(!IO).

>defs
(literal("B") and (not literal("D") or literal("E"))) and (literal("H") or
literal("J"))

Could someone propose better way doing this?

On Tue, Jul 19, 2011 at 6:23 PM, 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. Similarly, the predicate
> "expand" can only provide exactly one expansion for each formula.
>
> But when I try to compile the module defs.m (defined at end of this
> message) I get the following errors:
> \$ mmc --make defs
> Making Mercury/int3s/defs.int3
> Making Mercury/ints/defs.int
> Making Mercury/cs/defs.c
> defs.m:021: In `definition'(out):
> defs.m:021:   error: determinism declaration not satisfied.
> defs.m:021:   Declared `semidet', inferred `multi'.
> defs.m:023:   Disjunction has multiple clauses with solutions.
> ** Error making `Mercury/cs/defs.c'.
>
> What am I doing wrong?
>
> ------------------------- defs.m -----------------------------------
> :- module defs.
> :- interface.
> :- import_module io.
>
> :- pred main(io::di, io::uo) is det.
>
> :- implementation.
> :- import_module string.
>
> :- type formula
>     --->    and(formula, formula)
>     ;       or(formula, formula)
>     ;       not(formula)
>     ;       literal(string).
>
>
> :- type query
>     --->    equiv(formula, formula)
>     ;       formula(formula).
>
> :- pred definition(query::out) is semidet.
>
> definition(equiv(literal("A"), and(literal("B"),  not(literal("C"))))).
> definition(equiv(literal("C"), or(literal("D"), literal("E")))).
> definition(equiv(literal("G"), or(literal("H"), literal("J")))).
>
>
> :- func expand(formula) = formula.
>
> expand(F) = ExF :-
>    ( F = and(A,B),    ExF = and(expand(A), expand(B))
>    ; F = or(A,B),       ExF = or(expand(A), expand(B))
>    ; F = not(A),         ExF = not(expand(A))
>    ; F = literal(X),
>      ( if definition(equiv(literal(X),X1))
>        then X1 = X2, ExF = expand(X2)
>        else ExF = literal(X)
>      )
>    ).
>
> main(!IO) :-
>    X = and(literal("A"), literal("G")),
>    io.print(expand(X),!IO),
>    io.nl(!IO).
>
>
> -----------------------------------------------------------------------
>