Reifying groundness in Prolog with Attributed Variables

Question

I'm working on my own implementation of when/2.

Internally, when/2 needs to be able to—for a lack of a better word—"reify" ground/1. Doing this using attributed variables (in the style of SICStus-Prolog) is what this question is all about.

My implementation should work like the following "reference" implementation:

ground_t(Term,T) :-
   when(ground(Term), T=true).

In a fit of curiosity, I wrote the following little solver:

:- module(ground_t,[ground_t/2]).

:- use_module(library(atts)).
:- attribute ground_t/1.

ground_t(Term,T) :-
    (  ground(Term)
    -> T = true
    ;  term_variables(Term,Vs),
       create_mutable(Vs,MVs),
       attach_to_new_vars(Vs,MVs,T)
    ).

attach_to_new_vars([],_,_).
attach_to_new_vars([V|Vs],MVs,T) :-
    (  get_atts(V,+ground_t(Cs0))
    -> Cs = Cs0
    ;  Cs = []
    ),
    put_atts(V,+ground_t([MVs-T|Cs])),
    attach_to_new_vars(Vs,MVs,T).

% simple case: unify w/ground term
cliques_var_goals__ground([],_,[]).
cliques_var_goals__ground([MVs-T|Cs],Var,Goals) :-
    get_mutable(Vs0,MVs),
    list_eq_removed_atmost_once(Vs0,Var,Vs1),
    update_mutable(Vs1,MVs),
    (  Vs1 = []
    -> Goals = [T=true|Goals0]
    ;  Goals = Goals0
    ),
    cliques_var_goals__ground(Cs,Var,Goals0).

list_eq_removed_atmost_once([],_,[]).
list_eq_removed_atmost_once([X|Xs],E,Ys) :-
    (  X == E
    -> Ys = Xs         % remove item. do it at most once and stop
    ;  Ys = [X|Ys0],
       list_eq_removed_atmost_once(Xs,E,Ys0)
    ).

% general case: unify w/non-ground term
cliques_var_other__nonvar([],_,_).
cliques_var_other__nonvar([MVs-T|Cs],Var,Other) :-
    get_mutable(Vs0,MVs),
    term_variables(Vs0+Other,Vs1),
    term_variables(Other,New0),
    list_eq_removed_atmost_once(New0,Var,New),
    list_eq_removed_atmost_once(Vs1,Var,Vs2),
    attach_to_new_vars(New,MVs,T),
    update_mutable(Vs2,MVs),
    cliques_var_other__nonvar(Cs,Var,Other).

sort_all([]).
sort_all([MVs-_T|Xs]) :-
    get_mutable(Vs0,MVs),
    term_variables(Vs0,Vs),
    update_mutable(Vs,MVs),
    sort_all(Xs).

merge_cliques_post_unify(Cs0,Cs1,Other) :-
    append(Cs0,Cs1,Cs01),
    sort_all(Cs01),
    put_atts(Other,+ground_t(Cs01)).

verify_attributes(Var,Other,Goals) :-
    (  get_atts(Var,+ground_t(Cs0))
    -> (  ground(Other)
       -> cliques_var_goals__ground(Cs0,Var,Goals)
       ;  nonvar(Other)
       -> cliques_var_other__nonvar(Cs0,Var,Other),
          Goals = []
       ;  get_atts(Other,+ground_t(Cs1))
       -> Goals = [merge_cliques_post_unify(Cs0,Cs1,Other)]
       ;  put_atts(Other,+ground_t(Cs0)),
          Goals = []
       )
    ;  Goals = []
    ).

cliques_to_goal([]) --> [].
cliques_to_goal([MVs-T|Cs]) -->
    { get_mutable(Vs,MVs) },
    (  { Vs = []  } -> []
    ;  { Vs = [V] } -> [ground_t(V ,T)]
    ;                  [ground_t(Vs,T)]
    ),
    cliques_to_goal(Cs).

list_to_commalist([],true).
list_to_commalist([X],Y) :-
    !,
    X = Y.
list_to_commalist([X|Xs],(X,Y)) :-
    list_to_commalist(Xs,Y).

attribute_goals(Var) -->
    { get_atts(Var,+ground_t(Cs)) },
    cliques_to_goal(Cs).

attribute_goal(Var,Goal) :-
    phrase(attribute_goals(Var),Goals),
    list_to_commalist(Goals,Goal).

That was the easy part; now comes the hard part...

How do I go about testing if the behavior of the two solvers are equivalent—when performing multiple steps of variable aliasing and instantiation in a forest of shared terms?

---

Here are some simple manual tests that I did:

| ?- ground_t(X+Y,T1).
| ?- ground_t(X+Y,T1),X=f(U).
| ?- ground_t(X+Y,T1),X=f(U),U=Y.
| ?- ground_t(X+Y,T1),X=f(U),U=Y,Y=y.

| ?- ground_t(X+Y,T1),ground_t(X+Z,T2).
| ?- ground_t(X+Y,T1),ground_t(X+Z,T2),X = -U,Z = +V.
| ?- ground_t(X+Y,T1),ground_t(X+Z,T2),X = -U,Z = +U.
| ?- ground_t(X+Y,T1),ground_t(X+Z,T2),X = -U,Z = +U,U=u.
| ?- ground_t(X+Y,T1),ground_t(X+Z,T2),X = -U,Z = +U,U=u,Y=U.

Maybe you have a good idea for some nice corner cases... please share!

Answer 1

The really hard part is first of all understanding what ground_t/2 is actually about. It is not reifying anything, for there is no false.

It seems to be some internal auxiliary predicate you need to implement when/2. If it is an internal predicate, it does not need to fulfill all the expectations we have about a real constraint. Most notably, your implementation (as well as your reference implementation using the built-in when/2) does not constrain all involved variables:

SICStus 4.8.0beta3 (x86_64-linux-glibc2.17): Mon Oct 17 20:11:03 UTC 2022
...
| ?- when(ground(A-B),T=true),copy_term(A,Ac,Ac_0),copy_term(B,Bc,Bc_0).
Ac_0 = prolog:trig_ground(Ac,[_A],[Ac,_A],_B,_B),
Bc_0 = true,
prolog:trig_ground(A,[B],[A,B],_C,_C),
prolog:when(_C,ground(A-B),user:(T=true)) ? ;
no
| ?- ground_t(A-B,T),copy_term(A,Ac,Ac_0),copy_term(B,Bc,Bc_0).
Ac_0 = ground_t:(ground_t([Ac,_A],_B),true),
Bc_0 = ground_t:true ? ;
no
| ?- ground_t(A-B,T).
ground_t([A,B],T) ? ;
no
| ?- 

So both do not really constrain B, although the ground_t:true kind of gives us a hint. Also, it seems that the goal ground_t([A,B],T) is only displayed when no copy_term/3 has been used.

Given such lax requirements, freeze/2 is all you need. No need to delve into atvs at all.

myground_t(Term, T) :-
    term_variables(Term, Vs),
    myvars_t(Vs, T).

myvars_t([], true).
myvars_t([V|Vs], T) :-
    freeze(V, myground_t([V|Vs], T)).

| ?- myground_t(A-B,T),copy_term(A,Ac,Ac_0),copy_term(B,Bc,Bc_0).
Ac_0 = prolog:freeze(Ac,user:myground_t([Ac,_A],_B)),
Bc_0 = true,
prolog:freeze(A,user:myground_t([A,B],T)) ? ;
no

(A good implementation of term_variables/2 could avoid recreating identical list suffixes. No, there is currently none I know of.) What is missing in this implementation?

Now to your actual question about testing. Testing coroutines and constraints requires quite a lot of compute. So one may ask in advance whether or not the implementation to be tested has been written in such a manner to avoid certain errors a priori. I did not read your code any further than term_variables_set/2 whose second argument depends on the very age of variables which means that it might work for one age and does not work for another one. It would not be the first. So testing gets here even more complex. Why this at all?