Skip to first unread message
Markus Triska
Mar 30, 2016, 12:40:29 PM3/30/16
to SWI-Prolog
Hi all,
this post addresses 2 insightful comments that were raised in another thread. In short, the question that arose was how determinism and type checking can be combined with our desire to keep our code general and pure.
These questions are both very interesting, with the latter issue in my view being more subtle and insightful a question than the first, and I would like to address these two issues in this thread, independent of the also very interesting challenge that was the primary topic in the other thread.
We start from an obvious CLP(FD) definition of the factorial relation (I assume that you have ":- use_module(library(clpfd))." already in your .swiplrc by now, because using a Prolog system without integer constraints is like... well, there's really nothing else like that):
This will serve as a useful, non-trivial though still quite simple relation to illustrate both topics.
I will first show a few tricks and strategies for finding out more about this program.
Obviously, a logic program defines a relation. What relation? Let us find out! Simply ask the most general query, i.e., the query that has only variables as its arguments for all invoked predicates:
OK! So at this point we know that this logic program actually describes some solutions. How many solutions do we expect from the factorial relation? We know that the factorial function is defined for each integer, and seeing how these concrete integers arise in the answers, we certainly expect no finite bound on the number of solutions! Let us put this into a Prolog query: We expect that the following query never terminates:
What have I done here? I have simply added false/0 at the end of the query, so that the only thing that remains observable is termination, if it occurs. It is a good sign in this case that the query does not terminate! Its termination would mean that we have made a mistake in the implementation of this relation. Go check your definitions of n_factorial/2 with this query! Does this query terminate? If yes, then your definition of the relation is incomplete!
Let's try a few other queries:
All very nice and true. But wouldn't it be nice if we could get rid of the dangling choice points in the last two queries?
This is the first issue I am addressing in this post: Determinism.
Essentially, argument indexing cannot tell in this case that the two clauses are mutually exclusive, and therefore a choice point remains.
To help indexing, we are using the CLP(FD) constraint zcompare/3. This is like compare/3 on integers, except that it is a genuine constraint and remains sound and usable in all directions.
Side-note regarding monotonicity of compare/3:
but adding (!) a constraint yields new solutions:
This of course cannot happen with the CLP(FD) constraint zcompare/3:
Using zcompare/3, the example can be written as:
Here are the above queries and their results:
Aaaaaw yeah! It behaves like before, and the dangling choice points are gone!
But wait, there is more! Let us try two new examples with this definition:
Oh no! Why the discrepancy? Obviously, we would prefer some consistency regarding the type errors, to help automated analyzers and declarative debugging techniques. Luckily, this is also easy to obtain, by changing only the first clause of the auxiliary predicate n_factorial_/3!
Instead of:
we explicitly use the CLP(FD) constraint (#=)/2 to let it perform its type checking which normal unification obviously knows nothing about:
In total, we have:
And now we get:
in addition to the favorable determinism properties discussed above and the intended generality of a true relation.
I regard finding constructs like zcompare/3 as one of the primary challenges in future development of CLP(FD)!
This is only one small step towards obtaining more declarative programs with additional favorable properties. The search space for more such constructs is vast and still almost entirely unexplored! I hope that this and similar constructs will help to eventually resolve the original challenge from which these issues arose.
Using constraints in actual programs is the necessary first step to gradually obtain such constructs after collecting more experience. We cannot solve all arising issues at once, because some are more complex than others and they need to be solved in a certain order. But, in my view, it is high time we at least begin trying!
All the best,
Markus
this post addresses 2 insightful comments that were raised in another thread. In short, the question that arose was how determinism and type checking can be combined with our desire to keep our code general and pure.
These questions are both very interesting, with the latter issue in my view being more subtle and insightful a question than the first, and I would like to address these two issues in this thread, independent of the also very interesting challenge that was the primary topic in the other thread.
We start from an obvious CLP(FD) definition of the factorial relation (I assume that you have ":- use_module(library(clpfd))." already in your .swiplrc by now, because using a Prolog system without integer constraints is like... well, there's really nothing else like that):
n_factorial(0, 1).
n_factorial(N, F) :-
N #> 0,
N1 #= N - 1,
F #= N * F1,
n_factorial(N1, F1).
n_factorial(N, F) :-
N #> 0,
N1 #= N - 1,
F #= N * F1,
n_factorial(N1, F1).
This will serve as a useful, non-trivial though still quite simple relation to illustrate both topics.
I will first show a few tricks and strategies for finding out more about this program.
Obviously, a logic program defines a relation. What relation? Let us find out! Simply ask the most general query, i.e., the query that has only variables as its arguments for all invoked predicates:
?- n_factorial(N, F).
N = 0,
F = 1 ;
N = F, F = 1 ;
N = F, F = 2 .
N = 0,
F = 1 ;
N = F, F = 1 ;
N = F, F = 2 .
OK! So at this point we know that this logic program actually describes some solutions. How many solutions do we expect from the factorial relation? We know that the factorial function is defined for each integer, and seeing how these concrete integers arise in the answers, we certainly expect no finite bound on the number of solutions! Let us put this into a Prolog query: We expect that the following query never terminates:
?- n_factorial(N, F), false.
<wait>
<wait>
What have I done here? I have simply added false/0 at the end of the query, so that the only thing that remains observable is termination, if it occurs. It is a good sign in this case that the query does not terminate! Its termination would mean that we have made a mistake in the implementation of this relation. Go check your definitions of n_factorial/2 with this query! Does this query terminate? If yes, then your definition of the relation is incomplete!
Let's try a few other queries:
?- n_factorial(_, 5).
false.
?- n_factorial(N, 6).
N = 3 ;
false.
?- n_factorial(30, F).
F = 265252859812191058636308480000000 ;
false.
false.
?- n_factorial(N, 6).
N = 3 ;
false.
?- n_factorial(30, F).
F = 265252859812191058636308480000000 ;
false.
All very nice and true. But wouldn't it be nice if we could get rid of the dangling choice points in the last two queries?
This is the first issue I am addressing in this post: Determinism.
Essentially, argument indexing cannot tell in this case that the two clauses are mutually exclusive, and therefore a choice point remains.
To help indexing, we are using the CLP(FD) constraint zcompare/3. This is like compare/3 on integers, except that it is a genuine constraint and remains sound and usable in all directions.
Side-note regarding monotonicity of compare/3:
?- compare(>, A, B).
false.
false.
but adding (!) a constraint yields new solutions:
?- A = 3, compare(>, A, B).
A = 3.
A = 3.
This of course cannot happen with the CLP(FD) constraint zcompare/3:
?- zcompare(>, A, B).
B#=<A+ -1.
?- A = 3, zcompare(>, A, B).
A = 3,
B in inf..2.
B#=<A+ -1.
?- A = 3, zcompare(>, A, B).
A = 3,
B in inf..2.
Using zcompare/3, the example can be written as:
n_factorial(N, F) :-
zcompare(C, N, 0),
n_factorial_(C, N, F).
n_factorial_(=, _, 1).
n_factorial_(>, N, F) :-
N1 #= N - 1,
F #= N*F1,
n_factorial(N1, F1).
zcompare(C, N, 0),
n_factorial_(C, N, F).
n_factorial_(=, _, 1).
n_factorial_(>, N, F) :-
N1 #= N - 1,
F #= N*F1,
n_factorial(N1, F1).
Here are the above queries and their results:
?- n_factorial(N, F).
N = 0,
F = 1 ;
N = F, F = 1 ;
N = F, F = 2 .
?- n_factorial(N, F), false.
<wait>
?- n_factorial(_, 5).
false.
?- n_factorial(N, 6).
N = 3.
?- n_factorial(30, F).
F = 265252859812191058636308480000000.
N = 0,
F = 1 ;
N = F, F = 1 ;
N = F, F = 2 .
?- n_factorial(N, F), false.
<wait>
?- n_factorial(_, 5).
false.
?- n_factorial(N, 6).
N = 3.
?- n_factorial(30, F).
F = 265252859812191058636308480000000.
Aaaaaw yeah! It behaves like before, and the dangling choice points are gone!
But wait, there is more! Let us try two new examples with this definition:
?- n_factorial(3, a).
ERROR: Domain error: `clpfd_expression' expected, found `a'
?- n_factorial(0, a).
false.
ERROR: Domain error: `clpfd_expression' expected, found `a'
?- n_factorial(0, a).
false.
Oh no! Why the discrepancy? Obviously, we would prefer some consistency regarding the type errors, to help automated analyzers and declarative debugging techniques. Luckily, this is also easy to obtain, by changing only the first clause of the auxiliary predicate n_factorial_/3!
Instead of:
n_factorial_(=, _, 1).
we explicitly use the CLP(FD) constraint (#=)/2 to let it perform its type checking which normal unification obviously knows nothing about:
n_factorial_(=, _, F) :- F #= 1.
In total, we have:
n_factorial(N, F) :-
zcompare(C, N, 0),
n_factorial_(C, N, F).
n_factorial_(=, _, F) :- F #= 1.
n_factorial_(>, N, F) :-
N1 #= N - 1,
F #= N*F1,
n_factorial(N1, F1).
zcompare(C, N, 0),
n_factorial_(C, N, F).
n_factorial_(=, _, F) :- F #= 1.
n_factorial_(>, N, F) :-
N1 #= N - 1,
F #= N*F1,
n_factorial(N1, F1).
And now we get:
?- n_factorial(3, a).
ERROR: Domain error: `clpfd_expression' expected, found `a'
?- n_factorial(0, a).
ERROR: Domain error: `clpfd_expression' expected, found `a'
ERROR: Domain error: `clpfd_expression' expected, found `a'
?- n_factorial(0, a).
ERROR: Domain error: `clpfd_expression' expected, found `a'
in addition to the favorable determinism properties discussed above and the intended generality of a true relation.
I regard finding constructs like zcompare/3 as one of the primary challenges in future development of CLP(FD)!
This is only one small step towards obtaining more declarative programs with additional favorable properties. The search space for more such constructs is vast and still almost entirely unexplored! I hope that this and similar constructs will help to eventually resolve the original challenge from which these issues arose.
Using constraints in actual programs is the necessary first step to gradually obtain such constructs after collecting more experience. We cannot solve all arising issues at once, because some are more complex than others and they need to be solved in a certain order. But, in my view, it is high time we at least begin trying!
All the best,
Markus
Paulo Moura
Mar 30, 2016, 1:01:34 PM3/30/16
to Markus Triska, SWI-Prolog
Hi Markus,
Just a quick note. You compare/3 example is misleading. The compare/3 predicate is a standard predicate that compares terms, *including variables*, using standard order. Thus, when adding the A = 3 goal, you're not adding a constraint as you wrote but going from comparing two variables to comparing an integer with a variable (with the results, *in both cases*, being defined by standard order). On the other hand, your zcompare/3 predicate doesn't support comparing variables and instead adds a constraint waiting for the variables to become bound.
Cheers,
Paulo
> --
> You received this message because you are subscribed to the Google Groups "SWI-Prolog" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to swi-prolog+...@googlegroups.com.
> Visit this group at https://groups.google.com/group/swi-prolog.
> For more options, visit https://groups.google.com/d/optout.
-----------------------------------------------------------------
Paulo Moura
Logtalk developer
Email: <mailto:pmo...@logtalk.org>
Web: <http://logtalk.org/>
-----------------------------------------------------------------
Just a quick note. You compare/3 example is misleading. The compare/3 predicate is a standard predicate that compares terms, *including variables*, using standard order. Thus, when adding the A = 3 goal, you're not adding a constraint as you wrote but going from comparing two variables to comparing an integer with a variable (with the results, *in both cases*, being defined by standard order). On the other hand, your zcompare/3 predicate doesn't support comparing variables and instead adds a constraint waiting for the variables to become bound.
Cheers,
Paulo
> You received this message because you are subscribed to the Google Groups "SWI-Prolog" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to swi-prolog+...@googlegroups.com.
> Visit this group at https://groups.google.com/group/swi-prolog.
> For more options, visit https://groups.google.com/d/optout.
-----------------------------------------------------------------
Paulo Moura
Logtalk developer
Email: <mailto:pmo...@logtalk.org>
Web: <http://logtalk.org/>
-----------------------------------------------------------------
Markus Triska
Mar 30, 2016, 1:11:05 PM3/30/16
to SWI-Prolog, tri...@logic.at
Hi Paulo,
Just a quick note. You compare/3 example is misleading. The compare/3 predicate is a standard predicate that compares terms, *including variables*, using standard order. Thus, when adding the A = 3 goal, you're not adding a constraint as you wrote but going from comparing two variables to comparing an integer with a variable (with the results, *in both cases*, being defined by standard order). On the other hand, your zcompare/3 predicate doesn't support comparing variables and instead adds a constraint waiting for the variables to become bound.
Thank you for your interest!
I have given this example precisely to illustrate that whatever compare/3 is doing, it is certainly not a monotonic constraint, so yes, this is a big difference between compare/3 and zcompare/3.
Just a quick note: A = 3 is an example of a constraint in CLP(H), i.e., in constraint logic programming over Herbrand terms.
All the best!
Markus
Jan Burse
Apr 4, 2016, 3:23:03 PM4/4/16
to SWI-Prolog, tri...@logic.at
Dear All,
This is only the beginning, compare/3 and the likes is only one way to address determinism. Here is an example that uses (# \ /)/2 to address determinism. Its a problem posted on stack overflow(*) that diverted into a reification discussion:
Strong Reification Code:
In contrast to weak reification, strong reification not only uses an extra parameter for the truth value but also it tries to generate constraints. More inference power is gained if also invariants of the arguments are formulated:
Providing Invariants:
How much there is an impact of termination and/or feasibility for backward computation, I don't know yet. Its a first try on using an alternate approach for the Fibonacci Lukas problem. Not yet used for the later problem.
Bye
(*) Prolog union for A U B U C
http://stackoverflow.com/a/36410996/502187
This is only the beginning, compare/3 and the likes is only one way to address determinism. Here is an example that uses (# \ /)/2 to address determinism. Its a problem posted on stack overflow(*) that diverted into a reification discussion:
Strong Reification Code:
member(_, [], 0).
member(X, [Y|Z], B) :-
(X #= Y) #\/ C #<==> B,
member(X, Z, C).
union([], X, X).
union([X|Y], Z, T) :-
freeze(B, (B==1 -> T=R; T=[X|R])),
member(X, Z, B),
union(Y, Z, R).In contrast to weak reification, strong reification not only uses an extra parameter for the truth value but also it tries to generate constraints. More inference power is gained if also invariants of the arguments are formulated:
Providing Invariants:
?- all_different([1,X]), all_different([X,3]), union([1,X],[X,3],Y).
Y = [1, X, 3],
X in inf..0\/2\/4..sup,
all_different([X, 3]),
all_different([1, X]).How much there is an impact of termination and/or feasibility for backward computation, I don't know yet. Its a first try on using an alternate approach for the Fibonacci Lukas problem. Not yet used for the later problem.
Bye
(*) Prolog union for A U B U C
http://stackoverflow.com/a/36410996/502187
Markus Triska
Apr 4, 2016, 4:25:05 PM4/4/16
to SWI-Prolog, tri...@logic.at
Hi all,
On Monday, April 4, 2016 at 9:23:03 PM UTC+2, Jan Burse wrote:
This is only the beginning, compare/3 and the likes is only one way to address determinism. Here is an example that uses (# \ /)/2 to address determinism.
We are here witness to a take on CLP(FD) constraints that differs significantly from what we have often heard on this list in the past: Jan propagates here the notion that if we find a CLP(FD) program that does not work as efficiently as we need it to, we are well advised to look for different formulations that may run more efficiently, or even come up with entirely new constructs that may allow the solver to run faster.
All this despite the fact that it has been well established, repeatedly, on this list, that if we find a single example of a slow CLP(FD) program, it is better to throw away constraints altogether.
How may we be able to reconcile these view points? It is now almost as if library(clpfd) were a library that could be further improved and adapted to different use cases, and be made faster for applications that were previously inefficient!
I wish more users would see this just like Jan! Keep up the great work!
All the best,
Markus
Jan Burse
Apr 4, 2016, 5:07:27 PM4/4/16
to SWI-Prolog
Am Montag, 4. April 2016 22:25:05 UTC+2 schrieb Markus Triska:
All this despite the fact that it has been well established, repeatedly, on this list, that if we find a single example of a slow CLP(FD) program, it is better to throw away constraints altogether.
Thanks for playing host to the audience about me. And thanks
for making fun of me. Generally I am able to speak for myself.
Jan Burse
Apr 4, 2016, 5:28:55 PM4/4/16
to SWI-Prolog
Well the core of my challenge is:
What are the limits of this method?
This is no less and no more what is written in my
stack overflow question. I tried to find a picture about
the software engineering pyramid architecture-tools-
methods, but I didn't find it.
The CLP(FD) would be the architecture, the SWI-Prolog
would be the tool, and the method we don't know yet
a lot about it.
But I wouldn't worry. In the past there have been written
books about negation as failure. I it should have been witnessed
that I wrote it might take 1-2 years fo a good SO answer.
So at least I can share Markus Triskas appelation go go
Prologers. Help this poor soul.
Bye
P.S.: I found another pyramid on the web instead, which
allows me as a little retaliation to make fun of the current
state of the art of the method. Where are we currently exactly?
What are the limits of this method?
This is no less and no more what is written in my
stack overflow question. I tried to find a picture about
the software engineering pyramid architecture-tools-
methods, but I didn't find it.
The CLP(FD) would be the architecture, the SWI-Prolog
would be the tool, and the method we don't know yet
a lot about it.
But I wouldn't worry. In the past there have been written
books about negation as failure. I it should have been witnessed
that I wrote it might take 1-2 years fo a good SO answer.
So at least I can share Markus Triskas appelation go go
Prologers. Help this poor soul.
Bye
P.S.: I found another pyramid on the web instead, which
allows me as a little retaliation to make fun of the current
state of the art of the method. Where are we currently exactly?
Markus Triska
Apr 4, 2016, 5:37:37 PM4/4/16
to SWI-Prolog
Hi Jan,
On Monday, April 4, 2016 at 11:07:27 PM UTC+2, Jan Burse wrote:
Thanks for playing host to the audience about me. And thanks
for making fun of me. Generally I am able to speak for myself.
You're welcome! Just one thing that you cannot say yourself:
I would like to thank you for participating on the SWI mailing list!
All the best,
Markus
Jan Burse
Apr 4, 2016, 5:51:38 PM4/4/16
to SWI-Prolog
Quite obsessed with the SWI-Prolog mailing list, right?
I wouldn't worry about the SWI mailing list, since SWI-Prolog is
practically the only alive Prolog system, and since comp.lang.prolog
is anyway dead, the list has a splendid future.
Also I couldn't run the example in Jekejeke, since I have not
yet released a reification module. Today I was strongly thinking
about making reification more general.
Wouldn't it be nice to allow union work for the Herbrand domain?
Look see, we would only need to be able to change (#=)/2:
I wouldn't worry about the SWI mailing list, since SWI-Prolog is
practically the only alive Prolog system, and since comp.lang.prolog
is anyway dead, the list has a splendid future.
Also I couldn't run the example in Jekejeke, since I have not
yet released a reification module. Today I was strongly thinking
about making reification more general.
Wouldn't it be nice to allow union work for the Herbrand domain?
Look see, we would only need to be able to change (#=)/2:
member(_, [], 0).
member(X, [Y|Z], B) :-
(X #= Y) #\/ C #<==> B,
member(X, Z, C).
Into the following:
There is everything around to do that, yes or no? We
have (=)/2 and dif/2. Why does CLP(FD) reification not
cooperate with those two guys CLP(H)?
Or we might really think about a combination of (=)/2
and (#=)/2. Not yet sure about how this could be done
without types.
Lets call this new operator (eq)/2 for the moment, we could
then run member/3 for much bigger range of domains. Picat
could do it I guess, since instead of types they have evaluation
and a LISP like quote operator for Prolog terms.
Bye
P.S.: I am adopting CLP(H) since Paulo Moura used this here.
member(_, [], 0).
member(X, [Y|Z], B) :-
(X = Y) #\/ C #<==> B,
member(X, Z, C).
There is everything around to do that, yes or no? We
have (=)/2 and dif/2. Why does CLP(FD) reification not
cooperate with those two guys CLP(H)?
Or we might really think about a combination of (=)/2
and (#=)/2. Not yet sure about how this could be done
without types.
Lets call this new operator (eq)/2 for the moment, we could
then run member/3 for much bigger range of domains. Picat
could do it I guess, since instead of types they have evaluation
and a LISP like quote operator for Prolog terms.
Bye
P.S.: I am adopting CLP(H) since Paulo Moura used this here.
Markus Triska
Apr 4, 2016, 5:57:06 PM4/4/16
to SWI-Prolog
On Monday, April 4, 2016 at 11:51:38 PM UTC+2, Jan Burse wrote:
Wouldn't it be nice to allow union work for the Herbrand domain?
Look see, we would only need to be able to change (#=)/2:
Nice. Going even further, CLP(FD) could sometimes strongly benefit from the additional propagation that CLP(Q) gives you.
All the best,
Markus
Jan Burse
Apr 4, 2016, 6:14:56 PM4/4/16
to SWI-Prolog
Thats another issue. Its not related to reification but rather
how CLP(Q) deals with equations. Right?
how CLP(Q) deals with equations. Right?
Jan Burse
Apr 4, 2016, 6:17:38 PM4/4/16
to SWI-Prolog
Hi,
As far as I see it, reification always tries to stick with the inferential
capabilities of the original constraint. Doesn't try to give much more
or much less.
Today I made a nice additional observation, the reified constraint
also interacts with the non reified constraint or is negative. This is
seen in the all_different/1 usage.
Bye
As far as I see it, reification always tries to stick with the inferential
capabilities of the original constraint. Doesn't try to give much more
or much less.
Today I made a nice additional observation, the reified constraint
also interacts with the non reified constraint or is negative. This is
seen in the all_different/1 usage.
Bye
Reply all
Reply to author
Forward
0 new messages