mercury

Are algebraic predicates supported in Mercury?


I'm very new to Mercury and logic programming in general. I haven't found a numeric example like this in the docs or samples...

Take the example predicate:

:- pred diffThirtyFour(float, float).
:- mode diffThirtyFour(in, out) is det.

diffThirtyFour(A,B) :-
    ( B = A + 34.0 ).

With this, A must be ground, and B is free. What if I want A to be free and B to be ground (eg, adding mode diffThirtyFour(out,in) is det.). Can this sort of algebra be performed at compile time? I could easily define another predicate, but that doesn't seem very logical...

Update

So, something like this kind of works:

:- pred diffThirtyFour(float, float).
:- mode diffThirtyFour(in, out) is semidet.
:- mode diffThirtyFour(out, in) is semidet.

diffThirtyFour(A,B) :-
    ( B = A + 34.0, A = B - 34.0 ).

A little wary of the semidet, and the redundancy of the second goal. Is this the only way of doing it?

Update 2

This might be the answer...it issues a warning at compile time about the disjunct never having any solutions. A correct warning, but perhaps unnecessary code-smell? This does what I need, but if there are better solutions out there, feel free to post them...

:- pred diffThirtyFour(float, float).
:- mode diffThirtyFour(in, out) is det.
:- mode diffThirtyFour(out, in) is det.



diffThirtyFour(A,B) :-
    ( A = B - 34.0, 
      B = A + 34.0 
    ; 
     error("The impossible happened...")
    ).

Solution

  • Just discovered the ability to enter different clauses for different modes. This isn't quite an algebraic solver (which I wouldn't have expected anyway), but offers the precise organizational structure I was looking for:

    :- pred diffThirtyFour(float, float).
    :- mode diffThirtyFour(in, out) is det.
    :- mode diffThirtyFour(out, in) is det.
    :- pragma promise_pure(diffThirtyFour/2).
    
    diffThirtyFour(A::out,B::in)  :- A = B - 34.0.
    diffThirtyFour(A::in, B::out) :- B = A + 34.0.
    

    As described in the link, the promise_pure pragma is required because this feature can be used to break semantic consistency. It would also suffice to use the promise_equivalent_clauses pragma, which promises logical consistency without purity. It is still possible to declare clauses with inconsistent semantics with the impure keyword in the pred declaration.

    Interestingly, addition and subtraction in the standard int module are inversible, but not in the float module. Perhaps the choice was made because of possible errors in floating point arithmetic....