[mercury-users] if-then-else transformation

[Chris King]

Hi all, some food for thought:

Mercury's if/then/else is currently limited in that all variables in
the condition *must* be bound somewhere in the condition or outside
the if/then/else, even if said variables are bound within the then and
else.  This precludes "reversal" of certain functions, viz.:

:- pred make_even(int, int).
:- mode make_even(in, out) is det.

make_even(X, Y) :-
    if odd(X) then Y = X + 1 else Y = X.

This predicate transforms any integer into an even integer by possibly
adding one.  Conceptually, we could reverse this operation by possibly
subtracting one from even integers and failing on odd integers:

:- mode make_even(out, in) is nondet.

but this mode won't compile, because X is unbound due to Mercury's
scoping rules.

Now we could transform the if/then/else into its semantically
equivalent disjunction:

make_even(X, Y) :-
    (odd(X), Y = X + 1;
     not(odd(X)), Y = X).

but, as recently discussed, Mercury cannot deduce that these disjuncts
are mutually exclusive, and thus cannot conclude that make_even(in,
out) = det.

However a solution exists.  We can use an if/then/else to decide
odd(X) and bind a boolean variable indicating success.  A disjunct can
then switch on this variable:

make_even(X, Y) :-
    (if odd(X) then Odd = yes else Odd = no),
    (Odd = yes, Y = X + 1; Odd = no, Y = X).

This operationally equivalent code will compile in both modes with the
expected determinism.  It is my belief that such a transformation is
valid for all if/then/else goals which do not contain an explicit
toplevel existential quantification (since these range over the then
goal also). (Perhaps such a goal could still be transformed in this
manner, so long as any subgoals referencing the quantified variable
are left within the if/then/else.)

Thoughts?

- Chris
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------