Size via attributed variables

[philzook58]

I was interested in defining a declarative notion of term size on the road to defining a declarative notion of term ordering based on Knuth Bendix Ordering, but am a bit confused if I'm doing things right.

The thinking was I could attach an attribute to each variable X holding a clpz variable N representing the size that can be refined when the variable X is unified.

:- use_module(library(clpz)).
:- use_module(library(atts)).
:- use_module(library(lists)).

:- attribute term_size/1.


size(T,N) :- N #> 0, (
        var(T) -> 
        (get_atts(T, term_size(M)) -> N = M ; put_atts(T, term_size(N)))
        ; (T =.. [F|TA], maplist(size, TA, NA), sum(NA, #=, M), N #= M + 1)
).

verify_attributes(Var, Value, []) :-
        get_atts(Var, term_size(Size)) ->
        ( var(Value) ->
        (get_atts(Value, term_size(Size2)) -> Size = Size2; put_atts(Value, term_size(Size)))
        ; Value =.. [_F|TA], 
          maplist(size, TA, TAS), sum(TAS, #=, M), Size #= M + 1
        )
        ; true.

It seems like the resulting constraints are roughly right, but they don't prune that this is impossible?

?- size(f(X), Y), size(g(X), Z), Y #\= Z.
   user:put_atts(X,term_size(_A)), clpz:(_A in 1..sup), clpz:(_A+1#=Z), clpz:(_A+1#=Y), clpz:(Z in 2..sup), clpz:(Y#\=Z), clpz:(Y in 2..sup).

I could also perhaps freeze a size predicate until it is ground, but this wouldn't be able to do early pruning for comparison of sizes or even notice that two calls to size must be equal.

Am I missing something?

Thanks,
Phil

[triska]

Definitely an interesting idea, thank you for sharing this!

Currently, nothing is pruned because the clpz constraint Y #\= Z is concerned exclusively with the relation between these two variables, and does not affect variables on which the attribute term_size is attached.

How two different constraint solvers should work together is an open question, we currently have no dedicated formalism for it.

I would therefore recommend, at least for an initial implementation, to express what you need in the module you are currently writing. The important—and currently missing—step is the propagation starting from constraints on the sizes. Maybe this could be a good starting point:

term_sizes_different(Term1, Term2) :- ...

This predicate is also an opportunity to attach an attribute on the involved sizes that pertains to the solver you are writing, and triggers the propagation you want when that size changes.

[UWN]

Maybe look at https://github.com/bakaq/constrained.pl and consider length/2 and its constraint version length_c/2 as a starting point. In particular watch out the degree of consistency.

?- length_c(L, N), N in 0..2.
   constrained:length_c(L,N), constrained:list_c(L), clpz:(N in 0..2), constrained:integer_c(N).
?- length_c(L, N), N in 0..2, L = [a,b,c|_].
   false.
?- length_c(L, N), N in 0..2, length_c(K, M), M #> 2.
   constrained:length_c(L,N), constrained:list_c(L), clpz:(N in 0..2), constrained:integer_c(N),
   constrained:length_c(K,M), constrained:list_c(K), clpz:(M in 3..sup), constrained:integer_c(M).
?- length_c(L, N), N in 0..2, length_c(K, M), M #> 2, L = K.
   L = K, constrained:length_c(L,N), constrained:list_c(L), clpz:(N in 0..2), constrained:integer_c(N),
   clpz:(M in 3..sup), constrained:integer_c(M), weak.