Sunday random thoughts: Prolog's asymetry of Goal vs Clause & library(yall) problems

Request For Comments
1

I have been wondering why there is such an asymetry between “specifying a program at database level” and “specifying a program as a term” (as a goal, really). Once you notice it, it’s weird!

Code and unit tests code are here

Consider this program in “Prolog database form”:

foo(a(K)) :-
   debug(foo,"Database form: a(K) with K = ~q",[K]),
   (var(K) -> K= 666 ; true).

foo(b(K)) :-
   debug(foo,"Database form: b(K) with K = ~q",[K]),
   (var(K) -> K= 999 ; true).

The above can be alternatively expressed in “goal form”. Note that the goal form is a conjunction, where what was previously the head is now just an explicit unification at first position. There is no implication (and definitely no ‘->’ control construct) Proving X :- Y is the same as running X,Y.

goalform(X) :-
   G =
      ((X = a(K),
        debug(foo,"Goal form: a(K) with K = ~q",[K]),
        (var(K) -> K=666 ; true));
       (X = b(K),
        debug(foo,"Goal form: b(K) with K = ~q",[K]),
        (var(K) -> K=999 ; true))),
   call(G).

In “database form” the head has more “power” - simultaneous unification of several arguments, efficient lookup etc … why not have Goals which have :- too (they exist more or less in Lambda Prolog but the theoretical underpinning are unclear to me).

Anyway, the above lead to trying out library(yall) on the goalform. And there is a little problem. Consider:

goalform_yall_bad(X) :-
   K = as, % the andromeda strain
   G =
      ({}/[X]>>
         ((X = a(K),
           debug(foo,"Goal form: a(K) with K = ~q",[K]),
           (var(K) -> K=666 ; true));
          (X = b(K),
           debug(foo,"Goal form: b(K) with K = ~q",[K]),
           (var(K) -> K=999 ; true)))),
   call(G,X).

The above works the same way as the database form, as long as K stays fresh. Once K is instantiated, it bleeds into the goalform, wrecking results (see the test cases here). This in spite of explicitly stating via {} that “no free variables inside the lambda-enclosed term are connected to outside”.

Is it possible to fix that?

2

Hm, interestingly, directly passing the yall body to call/2, instead of storing it as a separate term does seem to work (it appears to be because the term expansion replaces the inline lambda goal with a separately-compiled predicate that gets its own fresh variables):

goalform_yall_good(Z) :-
   K = as, % the andromeda strain
   call({}/[X]>>
         ((X = a(K),
           debug(foo,"Goal form: a(K) with K = ~q",[K]),
           (var(K) -> K=666 ; true));
          (X = b(K),
           debug(foo,"Goal form: b(K) with K = ~q",[K]),
           (var(K) -> K=999 ; true))),
       Z).

?- goalform_yall_good(X).
X = a(666) ;
X = b(999).

Looking at the listing/1 of the goals:

goalform_yall_bad(X) :-
    K=(as),
    G={}/[X]>>(X=a(K), debug(foo, "Goal form: a(K) with K = ~q", [K]), (var(K)->K=666;true);X=b(K), debug(foo, "Goal form: b(K) with K = ~q", [K]), (var(K)->K=999;true)),
    call(G, X).

goalform_yall_good(A) :-
    true,
    call('__aux_yall_8b4629c866a4a7c537db486acbf8a0bc4b40280e', A).

'__aux_yall_8b4629c866a4a7c537db486acbf8a0bc4b40280e'(A) :-
    (   A=a(B),
        debug(foo, "Goal form: a(K) with K = ~q", [B]),
        (   var(B)
        ->  B=666
        ;   true
        )
    ;   A=b(B),
        debug(foo, "Goal form: b(K) with K = ~q", [B]),
        (   var(B)
        ->  B=999
        ;   true
        )
    ).
4

Maybe I’m missing something, but isn’t this just a variant on the problem of making “steadfast” predicates?

5

As I understand it, the issue is that one expects variables introduced in a lambda body to be distinct from variables in the surrounding “scope”, unless explicitly included in the capture group. This does happen when it can “ahead-of-time” expand the yall template, but as we see here, when it calls the yall lambda at runtime, it captures all the variable in the surrounding “scope” (since, of course, there isn’t really a scope to begin with).

1 Like
6

So, similar to the problem of “scope” for setof/3 and friends?

1 Like
7

Very much so; I guess the mechanism that calls un-expanded yall bodies should be doing the same sort of variable qualifying that setof/3 et al do.