Attributed Variables: A simple test, an unexplained failure

Help!
1

To understand handling of attributed variables better, I have rewritten the example of the reference manual from section 8.1 and added test cases.

This is an application of attributed variables whereby the variable carries a list (actually fulfilling the constraints of an ordset) of allowed values (which are atoms). On unification, the triggered hook procedure then either:

  • intersects the ordset attributes of two variables; or
  • unifies the post-unification variable with the single allowed value if the intersection yields an ordset of size 1; or
  • vetoes the unification.

This generally works, and I actually found a slight hiccup in the original version whereby the hook procedure is triggered from inside the hook procedure itself needlessly when the unification for the case of “there is a single allowed value” is performed.

However, I don’t get the following test case to work, which is actually just about assigning an attribute to a variable (breaking this into two lines because Discourse insist on using a narrow designer lane of text with 20 cm of white on each side of it):

test("assign attribute with single allowed 
      value to unbound variable", true(X == quux)) :-
   enum_domain(X,[quux]).

So, assigning an attribute listing only quux as allowed value to X should force X to be quux. Makes sense.

This doesn’t happen.

The rewritten code is:

enum_domain(X, ED) :-
   nonvar(ED),                   % ED bound? Then set the attribute value of the hole denoted by X   
   !,                            % Unnecessary cut (last clause!) but let's be clear about the commit
   list_to_ord_set(ED, EDOS),    % Sort/uniquify ED to form EDOS
   assertion(maplist(atom,ED)),  % All should be atom
   attr_key(Key),                % Retrieve Key value, which *must* be the name of this module
   put_attr(Y, Key, EDOS),       % Instead of replacing an existing attribute on X, set it on freshvar Y...
                                 % merge the attributes on X and Y via 
                                 % a triggered call to attr_unify_hook(Key, Y)
   X = Y.                        % *** THIS WON'T TRIGGER THE HOOK BUT SHOULD ***

(Btw, is there a way to get the name of the current module? module/1 just sets the current module)

The original code is more direct but essentially the same:

domain(X, List) :-
        list_to_ord_set(List, Domain),
        put_attr(Y, domain, Domain),
        X = Y.

What doesn’t happen is that X = Y triggers the hook procedure. However, it should. The original code is clearly based on that idea. But I don’t see what could block the calling. Unless it is newly not allowed to have the hook triggered from inside the module to which it belongs?

Here are the code and test cases:

enum_domain.pl

enum_domain.plt

2

The issue is you are using == rather than =.
== is more strict than unification, it essentially ask if they are the same and doesnt unify. e.g. X == 1 will fail.

You may ask, well other tests use == and they work. e.g.

test("unify two attributed variables with the allowed values intersection having one value", true(X == foo)) :-
   enum_domain(X,[foo,bar,baz]),
   enum_domain(Y,[foo,quux,zool]),
   X = Y.

However, the X = Y has already caused X to be unified to foo and hence X == foo is true in that particular case.

4

Thanks people.

Let me think about this. Whenever the answers are completely at odds with the question, I have expressed myself badly or there is some extremely large misunderstanding in my head.

No problem for the different semantics between = and ==, that’s clear - actually that’s why the test has X == quux - I expect the call to make X equal to quux by unification, which is what happens if two unbound variables are unified such that a single allowed value is left.

Similarly, in the other test, I expect the calls to enum_domain/2 followed by unification to leave X and Y the same and == to foo.

No surprises here.

Just a minute, I will add some debug statements to explain better.

6

Yes, that’s what I do, but like this:

Like this:

domain(X, Dom) :-
        var(Dom), !,
        get_attr(X, domain, Dom).

domain(X, List) :-
        list_to_ord_set(List, Domain),
        put_attr(Y, domain, Domain),  
        X = Y.  % <---- Here I expect the attr_unify_hook/2 to be called in all cases

I expect attr_unify_hook/2 to be called, which will take care of the special case List = [_], unifiying the attributed variable with the unique value allowed.

This is also what happens in the original code:

domain(X, Dom) :-
        var(Dom), !,
        get_attr(X, domain, Dom).
domain(X, List) :-
        list_to_ord_set(List, Domain),
        put_attr(Y, domain, Domain),
        X = Y.

But it doesn’t work. And why not?

After additional testing, I shall state with some certainty that:

the attributed variables hook is called for the statement X = Y where Y is var but carrries attributes only if X is nonvar.

Is that supposed to happen? It seems to defeat the purpose of attributed variables. X may be var and carry compatible or incompatible attributes, and we have to analyze that.

(And completely unrelated, can you put constraints on the attributes, stacking them? I don’t have enough brain to see when this would be useful but it might)

From the test cases output:

Successful test case

test("assign attribute to bound variable with allowed value", true) :-
   debug(enum_domain_test,"assign attribute to bound variable with allowed value",[]),
   X=foo,
   enum_domain(X,[foo,bar,baz]). % YES IT WORKS! Uses 2nd clause, and hook is called (and succeeds) **************

The printout shows the hook is well called:

% assign attribute to bound variable with allowed value                                                                                                     
% Prior to unification: X attributes are none, Y attributes are att(enum_domain,[bar,baz,foo],[])                                                           
% enum_domain:attr_unify_hook called with ATTV = [bar,baz,foo], PUV = foo, attributes(PUV) = none                                                           
% enum_domain:attr_unify_hook succeeds. PUV is no longer a variable but foo

Test case where the hook is not called

Test case fails because the hook must be called for it to succeed

X is unbound and the hook is not called, thus X is not set to quux

test("assign attribute with single allowed value to unbound variable", true(X == quux)) :-
   debug(enum_domain_test,"assign attribute with single allowed value to unbound variable",[]),
   enum_domain(X,[quux]). % Uses 2nd clause, but hook is not called

The printout shows the hook is not called:

% assign attribute with single allowed value to unbound variable                                                                                            
% Prior to unification: X attributes are none, Y attributes are att(enum_domain,[quux],[])                                                                  
ERROR: /home/calvin/_WORK_ON_PROLOG/github/prolog_notes/swipl_notes/about_attributed_variables/enum_domain.plt:11:
        test assign attribute with single allowed value to unbound variable: wrong answer (compared using ==)
ERROR:     Expected: quux
ERROR:     Got:      A
ERROR:        with: [enum_domain(A,quux)]

Test case succeeds because the hook need not be called for it to succeed

test("assign attribute to unbound variable", true) :-
   debug(enum_domain_test,"assign attribute to unbound variable",[]),
   enum_domain(_X,[foo,bar,baz]). % Uses 2nd clause but hook is not called

% assign attribute to unbound variable                                                                                                                      
% Prior to unification: X attributes are none, Y attributes are att(enum_domain,[bar,baz,foo],[])

Test case succeeds because the hook need not be called for it to succeed

But the check reveals that X = Y correctly took over the attributes present on Y only

test("assign attribute to unbound variable, then verify", true(ATTS == [bar,baz,foo])) :-
   debug(enum_domain_test,"assign attribute to unbound variable, then verify",[]),
   enum_domain(X,[foo,bar,baz]), % Uses 2nd clause but hook is not called
   enum_domain(X,ATTS).          % Uses 1st clause; ATTS is the ordset of [foo,bar,baz]

% assign attribute to unbound variable, then verify                                                                                                         
% Prior to unification: X attributes are none, Y attributes are att(enum_domain,[bar,baz,foo],[])

Or:

test("assign attribute to unbound variable, then verify (using get_attrs/2)", true(ATTS == [bar,baz,foo])) :-
   debug(enum_domain_test,"assign attribute to unbound variable, then verify",[]),
   enum_domain(X,[foo,bar,baz]), % Uses 2nd clause but hook is not called
   get_attrs(X,att(_,ATTS,[])).  % ATTS is the ordset of [foo,bar,baz]

% assign attribute to unbound variable, then verify (using get_attrs/2)                                                                                     
% Prior to unification: X attributes are none, Y attributes are att(enum_domain,[bar,baz,foo],[])

(Why do need to suffer 80 column text in 2020 in Discourse? Because the IBM Punch Card had those practically exactly 100 years ago and tradition is tradition!)

7

From the manual for attr_unify_hook:

It is called after the attributed variable has been unified with a non-var term, possibly another attributed variable.

I interpret this to mean that unification of an attributed var with a “pure” var will not call the unify hook, which I think is correct.

Looking at domain/2, the first clause queries an attributed variable for its domain which I think is clear enough. My interpretation of the second clause
is that the domain defined by List is intersected with X’s current domain. The intersection is implemented by attr_unify_hook. An absent X domain (no attribute) is interpreted as the universal set (all terms?), so the new X domain will be just the set defined by List, first attributed to Y (a local var) and then unified with X. In this case no call to attr_unify_hook is made; what would be the point?

This leaves the problem of what should happen when the domain becomes a singleton set. I think the intent is that the attributed variable should be unified with the singleton. If a domain is narrowed to a singleton via intersection then that can be done in attr_unify_hook. But if that is expected to happen by calling domain/2, then there’s a missing case which should just unify X with the list member. The other missing case is List=[], which I believe should just fail (as should an intersection which produces the empty set). So something like:

domain(X, Dom) :-
        var(Dom), !,
        get_attr(X, domain, Dom).
domain(X, List) :-
        list_to_ord_set(List, Domain),
        set_domain(Domain,X).

set_domain([],X) :- !, fail.  % should be checked
set_domain([X],X) :- !.       % if X attributed, attr_unify_hook will test validity
set_domain(Domain,X) :-
        put_attr(Y, domain, Domain),  % create Y to intersect with current X
        X = Y.

Thanks for doing this; I think the manual could definitely use a bit more rigour in this area, e.g., is attr_unify_hook called if two attributed variables are unified but don’t have a common attribute?

1 Like
9

Thank you for answers.

After lengthily going through the example again and referring to your answers, I got rewritten code that is working as expected.

Diagram because I love diagrams

A little diagram to explain what’s going on in this application of attributed variables, where the attribute values are ordsets and unification means the new attribute value is the intersection of the ordsets (it’s really not complicated):

A matrix showing when the hook is triggered

The different cases are also tested in enum_domain.plt below.

Code

And finally, the example rewritten for more clarity (IMHO) and with lots of more comments, and debug printouts and separate get/set predicates for the attribute in question (… awkwardly shoehorning an imperative get and set into a single predicate domain/2, as done in the example, is just a step too far for me).

Additionally, the hook predicate updates a global variable to indicate that it has been called (and with what arguments), so that test cases can easily verify that it has, indeed, been called, and that only once.

(note that Github won’t correctly syntax-highlight .plt files, it thinks those are gnuplot files)

1 Like
10

Looks correct to me. Not sure I like the term hole for a variable, but I guess it is intuitive enough.

11

Thank you.

I have to say, it took me a looong time to get that the “variables” are the “local names” of “global stuff” (a concept near the mathematical variable) and that the “holes” have an independent existence as a special case of “global stuff” (an idea that is not well communicated with var/1 and nonvar/1 for example).

In Prolog lingo, “variables” is used both to fluidly signify “hole” and “local name”. That’s probably a reef for beginners.

13

Prolog variables are strange things :slight_smile: At least, if you try to compare them to variables of imperative languages. They basically have no name, e.g. functor(Term, x, 10) produces a term with 10 variables that have no name. Only the context of read/1 gives (some) variables a name. There it serves two purposes: ensure variables with the same names are shared and, notably for the toplevel, determine that a variable with name X has been filled (bound) to a term T, making a query true given a set of bindings. I think the idea to consider variables to be named entities is in most cases misleading in Prolog. They should primarily be considered holes.

1 Like
16

It’s about engineering & coding.

Bitter lessons learned taught me that knowing that some tools actually exist can save you many many months of your life - and also open new avenues that you didn’t even know where there.

Also, adding documentation is fun, it helps to straighten out the concepts. And maybe somebody may use them even.

Not sure what I can do with attributed variables yet. We will see. Maybe nothing.

(But there should be something similar for the head’s “capturing variables”: one should be able to specify that the term X captured be a head variable Y must be var(X) or nonvar(X). It would save on guard conditions to be performed immediately after a (potentially undesired) head unification has succeeded. What’s the reason this doesn’t exist?)

17

Can you turn Vidals Quine into a counting algorithm? Currently it says
Yes its a tautology, No its not a tautology (it can also say its an antology).

But how about Vidals Quine which would say:
Hey your formula has so and so many models?