functor_spec/3, a generalization of functor/3 that works in all modes

[bakaq]

Recently I made this library to learn how to use attributed variables. It provides a predicate functor_spec/3 that works like functor/3, but delays execution so that it can work in all modes. The goal was to make something like dif/2 is to (\==)/2, and I think I was able to do it (I made a lot of tests).

It also provides a variant functor_spec/4 in which the fourth argument is a list of the arguments of the term, (#=..)/2 which is a generalization of (=..)/2, reified versions of these for use with library(reif) (functor_spec_t/4, functor_spec_t/5 and (#=..)/3), and a predicate functor_match_t/3 for use with library(reif) which unifies it's arguments only if they have the same functor and arity.

Example of usage:

% Works just like functor/2
?- functor_spec(a(1,2), a, 2).
   true.
?- functor_spec(A, a, 2).
   A = a(_A,_B).
?- functor_spec(a(1,2), A, B).
   A = a, B = 2.
% But works in more cases
?- functor_spec(A, B, C).
   functor_spec:functor_spec(A,B,C,_A).
?- functor_spec(A, B, C), B = a, C = 2.
   A = a(_A,_B), B = a, C = 2.

I feel like this could be integrated into a built-in library for Scryer, but I'm not sure if this is useful enough to justify that. In my (not so extensive) experience, using predicates like functor/2 and (=..)/2 usually means that there is a better way to do it with implicit unification in the arguments of predicates (which also can benefit from indexing). But maybe that impression I have is just because they are modal and, because of that, very annoying to use.

[UWN]

It would be nice to give such predicates a good general suffix. Think of the _si-suffix for predicates that expect sufficiently instantiated arguments. So we have dif_si/2 and atom_si/1. The corresponding definition here would be atom_thatsuffix/1.

Apart from bakaq/constrained.pl#1, it is not clear how and what kind of consistency should be maintained. Think of

?- functor_spec(F,F,N).
   functor_spec:functor_spec(F,F,N,_A), functor_spec:put_atts(F,functor_spec_constraint([F])), weak. % maybe unexpected
   N = 0, *** . % expected but not found
?- functor_spec(F,F,F).
   functor_spec:functor_spec(F,F,F,_A), functor_spec:put_atts(F,functor_spec_constraint([F])), weak.
   F = 0.

And it is not clear if this should be the sole responsibility of functor_thatsuffix/3 or if it is rather related to a more general type/constraint system. So that functor_thatsuffix/3 would post rather:

?- functor_thatsuffix(F,N,A).
   atomic_thatsuffix(N), integer_thatsuffix(A), functor_thatsuffix(F,N,A).
?- functor_thatsuffix(F,N,A), F = N.
   F = N, A = 0, atomic_thatsuffix(F).
?- functor_thatsuffix(F,N,A), F = N, F = A.
   F = 0, N = 0, A = 0.

All of this is quite close to CHRs.

But maybe that impression I have is just because they are modal and, because of that, very annoying to use.

Annoying they are only if there is an instantiation_error. But if that error does not occur, their result is correct. Compare this to an incorrect answer. Think of

?- atom(X), X = a.
   false.  % bad
?- X = a, atom(X).
   true. % good
?- atom_si(X).
   instantiation_error. % annoying
?- X = a, atom_si(X).
   X = a. % correct
?- X = 1, atom_si(X),
   false. % also correct

At first it seems that constraints/delayed goals are the answer. But if you look at the development of Prolog systems this is not that evident. One of the first systems in that direction was MU/NU-Prolog with it's wait declarations. Even SICStus adopted them early on as block declarations. They are still in SICStus and apparently they are used (given that there are highly specific bug fixes) but the properties of these declarations is very hard to fathom, in particular with respect to universal termination.
And then if you get an answer back full of floundering goals you will soon get annoyed too. Contrast this to clpz/clpfd. There the answer to such an answer full of constraints would be labeling. It does not work in all cases but in many.

Another approach worth mentioning is Prolog III and even more so Prolog IV. There are some such constraints that are maintained automatically.

[bakaq]

All of this is quite close to CHRs.

What are CHRs?

[UWN]

Constraint Handling Rules. Prolog implementations are for SICStus and SWI. The SWI implementation has certain quirks that limit its applicability.

The atv-interface is in a sense much too low level for most uses. But a higher level than that has not been established. Only some hints towards one.

[bakaq]

I suppose "atv-interface" refers to attributed variables, is that right?

CHR looks like a more general and elegant way to do what I'm doing behind the scenes in the enforce_constraints/4 predicate here.

[UWN]

Just for completeness, labeling (that is labeling/2) is not the only way out of unreadable answers, the other way is the much underappreciated clpz:contracting/1 which (from the viewpoint of a library-user) does no backtracking-search but instead just contracts the domains (of course it uses backtracking behind, but this does not interfere with the user's view).

[bakaq]

It seems that Scryer's library(clpz) doesn't provide contracting/1, but you can use it with a full qualification clpz:contracting(_).

(Just leaving this here if someone reads this discussion and is confused why it doesn't work if you call it like contracting(_))

[bakaq]

It would be nice to give such predicates a good general suffix. Think of the _si-suffix for predicates that expect sufficiently instantiated arguments. So we have dif_si/2 and atom_si/1. The corresponding definition here would be atom_thatsuffix/1.

I agree, I just didn't think of anything good and wanted to implement it before thinking about names. Some things that come to mind:

• _delayed
• _d, for "delayed"
• _de, for "delayed execution"
• _nm, for "non-modal"

[UWN]

delayed means it just delays and does not check for any form of consistency. That is, it is easy to construct cases of inconsistency. Or to put it the other way round, only delay mechanisms are at work, no consistency checking. Also, what about errors? Prolog IV opted for silent failure only (for constraints).

[bakaq]

I don't understand the usefulness of errors in this context if the predicate can be reified (like I did). With reified predicates you can avoid using catch/3 (which, as far as I know, isn't monotonic like if_/3) to deal with the cases where the constraint fails. Can you give an example of how errors could be more useful than just failure + reified alternative?

[bakaq]

Other options I thought about are:

• _nb/_nonblocking, because instead of throwing an instantiation error it continues, but this doesn't encode that consistency is mantained.
• _c/_consistent, because the predicate ensures consistency, but you can argue that predicates like functor/3 already ensure consistency because they only give correct answers or instantiation errors.
• _dc/_delayed_consistent, because the predicate is both delayed (and thus doesn't throw instantiation errors) and ensures consistency.

[bakaq]

And then if you get an answer back full of floundering goals you will soon get annoyed too. Contrast this to clpz/clpfd. There the answer to such an answer full of constraints would be labeling. It does not work in all cases but in many.

I don't know if something like clpz:labeling/2 is possible in this case for the general case, because it would need to generate all the possible functors for this general case:

-? functor_spec(A, F, 1).
   A = a(_A), F = a
;   A = b(_A), F = b
;  ... .

But you can already generate all the aritys with functor_spec/4:

?- use_module(functor_spec), functor_spec(F,a,_,Args), length(Args, _).
   F = a, Args = []
;  F = a(_A), Args = [_A]
;  F = a(_A,_B), Args = [_A,_B]
;  F = a(_A,_B,_C), Args = [_A,_B,_C]
;  ... .

One idea is to maybe implement so that it only works when the set of possible functors is finite, just like clpz:labeling/2 only works if the domains of the variables are finite.

[bakaq]

And it is not clear if this should be the sole responsibility of functor_thatsuffix/3 or if it is rather related to a more general type/constraint system. So that functor_thatsuffix/3 would post rather:

?- functor_thatsuffix(F,N,A).
   atomic_thatsuffix(N), integer_thatsuffix(A), functor_thatsuffix(F,N,A).
?- functor_thatsuffix(F,N,A), F = N.
   F = N, A = 0, atomic_thatsuffix(F).
?- functor_thatsuffix(F,N,A), F = N, F = A.
   F = 0, N = 0, A = 0.

I definitely thought about doing something like I did with functor/3 for all (or at least most) of the relevant ISO Standard (can't do it with var/1 for example), and it would enable the behavior you showed.

[bakaq]

I think the property I would want from _thatsuffix predicates, and what I intended to achieve with functor_spec/3 is the following:

If there are only _thatsuffix predicates in a query, reordering the order of the predicates never gives a wrong answer or introduces an instantiation error. Ideally it always gives the same answer, but I'm not sure if that is achievable. A wrong answer in this context means that the concrete values or constraints of the answer are not consistent with the concrete values or constraints of the other answers. If the answer it gives is more general, it has to contain all the more specific answers. If the answer is more specific, it has to be contained in all of the more general answers.

I think this is strictly stronger than monotonicity. Some predicates that seem to have this property are (=)/2, (,)/2, (;)/2, if_/3 and my functor_spec/3, but I'm not entirely sure.

[UWN]

A wrong answer in this context means that the concrete values or constraints of the answer are not consistent with the concrete values or constraints of the other answers.

Not sure what you mean here by "other answers",

As long as an answer is conditional, so there are some residuals floating around (more precisely floundering around), it might be weak, but not wrong.

If the answer is more specific, it has to be contained in all of the more general answers.

Not sure what you mean here. An (complete) answer, that is more specific is just incomplete.

Also termination or rather non-termination comes here into play.

What about calling it functor_c/3?

And as you mention (;)/2 we should clarify, what we mean by an answer. Is it the complete answer, or is it just one answer the top level loop produces and where upon ; we get further answers. In Prolog we have this ambiguity. Prior to constraints, everything was a solution. That is, everything NSTO, was a solution or in fact often also many solutions. Think of

?- length(L,2).
   L = [_A,_B].

Traditionally this was often called a solution. But these are infinitely many solutions.

In any case, for the purpose of better examples, consider a constraint version of append(Xs,Ys,XsYs).

In Prolog IV there is a related constraint version conc(XsYs,Xs,Ys) which is only true for lists. So Ys = non_list will always fail. Further it propagates only if two of the arguments are lists. It does not fail for Xs = [a|_], XsYs = [b|_] whereas append/3 does so. Do you see the motivation behind?

[bakaq]

It does not fail for Xs = [a|_], XsYs = [b|_] whereas append/3 does so. Do you see the motivation behind?

It seems to be wrong, because if Xs starts with a then it's concatenation with another list will also start with a. Is it because conc/3 doesn't have it's arguments ordered, so that XsYs can be both Xs then Yx or Ys then Xs?

[bakaq]

What about calling it functor_c/3?

The "c" stands for "consistent" as I suggested earlier I suppose. That seems fine.

[UWN]

conc/3 has a different order, because in Prolog IV, there is (~)/2 which is used to describe primarily answers, but in contrast to call/N, it adds as the first argument. For some reason one cannot use that ~as operator in ISO mode, but there is the prolog4 mode where you can:

>> XsYs ~ conc(Xs,Ys).

Ys ~ list,
Xs ~ list,
XsYs ~ list.

Which as answer is too general. In ISO mode only the following works

?- conc(XsYs, Xs,Ys).

Ys ~ list,
Xs ~ list,
XsYs ~ list.

As far as I understant Prolog IV, there was never a mode that showed the constraints.

But leaving that aside, do you see the termination problems?

[UWN]

What about calling it functor_c/3?

The "c" stands for "consistent" as I suggested earlier I suppose. That seems fine.

Or maybe it stands for constraint. Consistency might be achievable for functor_c/3, but it is not (realistically) achievable for append_c/3 nor conc_c/3.

[bakaq]

Not sure what you mean here by "other answers",

Ok, let me specify. Suppose we have the following query:

?- a(X), b(Y), c(X,Y).
    X = 4, Y = 2
;   Y = 2, less_than(X, 3).

(X = 4, Y = 2; Y = 2, less_than(X, 3)), where less_than/2 is an constraint, is what I was referring to as "an answer". It's the "set of all answers found on backtracking" for a given permutation of the goals. No suppose we have this other permutation of the goals:

?- c(X,Y), b(Y), a(X).
    X = 1, Y = 2
;   X = 4, Y = 2.

The "answer" for this permutation is more specific, but it is still consistent with the other "answer". This "set of all answers found on backtracking" is a subset of the other permutation. Now suppose this:

?- b(Y), c(X,Y), a(X).
    between(X, 0, 5), between(Y, 0, 5).

The "answer" for this permutation is more general, but it is still consistent with the other "answer". The "set of all answers found on backtracking" of the other answers are subsets of this one.

I guess there are more complicated cases where the "answers" are not subsets of one another but are still consistent, but I guess this is enough to explain what I meant.

[UWN]

To me, a/1, b/1and c/2are not relations at all!

Your first query describes for X the values 0, 1, 2, 4 (and maybe also all negative numbers).

The second query only describes X with 1, 4 and

The third describes X with 0, 1, 2, 3, 4, 5.

So they are all different.

Could we agree to say complete answer to mean it all?

[bakaq]

Could we agree to say complete answer to mean it all?

Ok, makes sense.

So they are all different.

So you think the complete answers should always be identical (as in representing the same set of possible values for variables, there could be redundant constraints) for such predicates? That would mean that the complete answers in each iteration could be:

?- a(X), b(Y), c(X,Y).
    X = 4, Y = 2
;   Y = 2, less_than(X, 3), greater_than(X, 0).
% Notice that the only possible value for X here in the second alternative is 1.
% Maybe the constraints couldn't be resolved because of implementation details,
% but it still describes the complete answer ( X = 1, Y = 2; X = 4, Y = 2).
?- c(X,Y), b(Y), a(X).
    X = 1, Y = 2
;   X = 4, Y = 2.
?- b(Y), c(X,Y), a(X).
    Y = 2, greater_than(X, 0), less_than(X, 0), not_in_interval(X, 2, 3).
% Similarly, this also describes the complete answer ( X = 1, Y = 2; X = 4, Y = 2).

I'm not sure if this is achievable when constraints interact with one another (like in #1010, but your explanation there does seem to indicate that what's happening doesn't affect the set represented by the complete answer but only redundant or reducible constraints).

[UWN]

So you think the complete answers should always be identical

At least for the finite case. For the infinite case, things get a bit less precise, when you have unfair enumeration and the like.

[bakaq]

I think this is well defined even for infinite answers, but maybe not that useful in practice.

Answer being an answer to a query query means that (Answer, query) terminates and is true. The property I was talking about (in the case of the complete answers always being identical) means that for any permutation of the query (Answer, query_permutation) also terminates and is true. In the finite case this is equivalent to constructing the complete answer CompleteAnswer = (Answer1; Answer2; Answer3; ...) and having (CompleteAnswer, query_permutation) terminate and be true.

[UWN]

Not sure the termination property can be guaranteed all the time. Of course it is desirable.

[triska]

This project seems to be an excellent candidate for a great presentation at the Scryer Prolog meetup in November: https://hsd-pbsa.de/veranstaltung/scryer-prolog-meetup-2023/

If possible, please consider attending the meetup, it would be great to meet you there!

[bakaq]

I would love to attend! Unfortunately I live in Brazil, so I think it would be kinda complicated for me to get there. And also, it's right about the date I have to submit my bachelor's thesis, and knowing myself I will be working on it until the very last hour.

As an update, I've renamed the project to constrained.pl and expanded the scope to include many other common predicates that I think are possible to implement as constraints (like most type checks, and length_c/2 which has already been useful to me in practice). I think this is a great stress test for attributed variables, but also very useful to expand the "pure, monotonic core of Prolog" with predicates that also aren't modal. I intend to submit this as a library for Scryer eventually (at least a subset with the type constraints, functor_c/3 and friends, and length_c/2), but I think it needs a bit more testing.

[triska]

Awesome, then let's focus on this for now! I hope we will be able to enjoy a more elaborate presentation of all these features at a future meetup, maybe already next year!

[UWN]

Regardless of the concrete plans for future constraints, they will always have to interact with dif/2. Did you have a look at #2056? I am not even sure my speculations there are right.