Alternative to SSU

General
1

If I understand correctly, SSU syntax is borrowed from another language, and not (easily?) portable across Prologs.

And let’s consider this example for a moment:

ab_status(A,B,Status) :- 
	A, B, Status = both(A,B).

ab_status(A,B,Status) :- 
	A, \+B, Status = just_a(A).

ab_status(A,B,Status) :-
	\+A, B, Status = just_b(B).

ab_status(A,B,Status) :-
	\+A, \+B, Status = neither.

Rewriting the above using SSU wouldn’t omit the cost or repeated evaluations of A and B.

On the other hand, if we adhere to a consistent style of guards, we could refactor the above with a sort of “ssu indicator”
:- ssu(ab_status ...)

This would refactor ab_status to something like:

ab_status(A,B,S) :-
(A -> true; NotA = true), ...,
(A, B, S=both) ;
(A, NotB, S=just_a) ;
(NotA, B, S=just_b(B)) ;
(NotA, \+NotB, S=neither)

This would be some (portable) rewriting for optimization. But it relies on convention and silently fails to optimize if the convention is not adhered to. Could one defend against creating an incorrect rewrite?

Does this seem at all fruitful or totally misguided?

2

Sounds like we could just use:

goal_t(Goal, T) :-
    (   call(Goal)
    ->  T = true
    ;   T = false
    ).
    
ab_status(A, B, Status) :-
    goal_t(A, AT),
    goal_t(B, BT),
    atom_concat(AT, BT, ABT),
    ab_status_(ABT, A, B, Status).
    
ab_status_(truetrue, A, B, both(A, B)).
ab_status_(truefalse, A, _B, just_a(A)).
ab_status_(falsetrue, _A, B, just_b(B)).
ab_status_(falsefalse, _A, _B, neither).

This avoids choicepoints with e.g.:

?- ab_status(true, true, S).
S = both(true, true).

?- ab_status(true, false, S).
S = just_a(true).

?- ab_status(false, false, S).
S = neither.

?- ab_status(false, true, S).
S = just_b(true).
4

The semantics of => are a bit strange if unification happens in a guard in the head. For example, in the following, p/1, q/1, and r/1 should all mean the same:

p(X), eq(X,1) => true.
p(_) => fail.

q(X), X=1 => true.
q(_) => fail.

r(1) => true.
r(_) => fail.

eq(X, Y) :- X=Y.  % or: eq(X, X).

However, p(X) succeeds (with X=1) but q(X) and r(X) quietly fail.
(The definition of p/1 using eq/2 breaks the SSU semantics that no unification occurs in the head.)

So, any conversion from SSU to non-SSU neds to change unification to subsumes_term/2 or similar.

1 Like
5

It is not terribly hard to port to any Prolog system that provides term_expansion/2. It means you must modify arguments holding non-variables in the head into a variable and use ==/2 and similar to verify the shape of the argument without binding it. Also multiple occurrences of the same variable in the head must use subsumes_term/2. Next you add the guards, a !/0 call and the body. Finally you add a catch all clause that raises an exception if no rules reached the body.

It is less complicated in the VM. That basically adds code to verify no trailing happened in the current implementation. The alternative would be to have specializations of the unify instructions that fail rather than trail or have some mode to prevent trailing during the head unification. Not sure that is worth the trouble.

2 Likes