Replies: 2 comments
-
|
@mizlan: I think you initiated the thread I mentioned here? Thank you too! And just to repeat: It is impressive to see such insights, I now saw that this was even the very first post in the forum for this profile! I hope you find the predicates I mentioned above useful for your work, they are all part of the pure monotonic core of Prolog and automatically prevent an important class of mistakes while at the same time yielding very general programs. Note that ?- include(#>(3), [K], []). instantiation_error. Clearly, it is preferable to give more interesting answers instead, as we see with ?- tfilter(\X^(clpz_t(3#>X)), Ks, []). Ks = [] ; Ks = [_A], clpz:(_A in 3..sup), ... ; Ks = [_A,_C], clpz:(_A in 3..sup), ... ; Ks = [_A,_C,_E], clpz:(_A in 3..sup), ... ; Ks = [_A,_C,_E,_G], clpz:(_A in 3..sup), ... ; ... . The key point is to, so to say, "move along correctness": We start with pure monotonic predicates that work correctly in all usage modes, and then make them as efficient as we can, and we think about which additional predicates would be useful and fitting so that we can express even more programs with them, such as the mentioned In this way, we automatically avoid the misconceptions mentioned in the thread. For instance, the internal implementation of constraint solvers has no relevance to application programmers. Various different implementation strategies are possible: Constraints can be built into the Prolog engine, or made available to Prolog libraries via attributed variables or meta-structures etc. None of this has any influence in how these predicates are used in Prolog programs. What matters are the logical properties that these predicates preserve, because these properties make logical reasoning about programs and queries possible. |
Beta Was this translation helpful? Give feedback.
-
|
It is heartening to hear that my suggestion has been well-received :) |
Beta Was this translation helpful? Give feedback.
-
Dear all,
in continuation of
tpartition/4discussed in #2136, I would like to express my appreciation for the new constructclpz_t/2which was suggested with an accompanying implementation by @librarianmage in #2225 and is filed for inclusion inlibrary(clpz)via #2319.As a motivating example, let's take a thread I came across today: https://swi-prolog.discourse.group/t/conditional-doesnt-backtrack-for-solution/7221. The originator of the discussion attentively noticed the following logical discrepancy:
This answer means: There is no solution. Not for any K!
This answer means: There is a solution.
K = 4is a solution!Are there any other solutions? How can we find them? And how can we be certain about the existence or lack of other solutions? Unfortunately, it is clear from this example alone already that we cannot rely on the most basic logical laws we expect to hold when reasoning about solutions in this situation, and therefore it is hard to use the Prolog system's answers to find out more about the situation. We may be lucky and find another solution by trial and error. But what if we don't? What if we only get further "false" answers? Should we give up at one point (when?) and say that there are "maybe" no further solutions?
Note that this is a correctness issue: The system tells us that there are no solutions, but in fact there are solutions. There is no way to spin this in any other way. It is not a matter of opinion or personal preference. The two answers we get above are logically incompatible, because either there is a solution or there is no solution, so they cannot both be correct. The ability to generalize and specialize queries with the expected logical properties is a prerequisite for declarative debugging and systematic testing of Prolog programs, different execution strategies, automatic reordering of goals etc.
tfilter/3fromlibrary(reif)yields correct answers in such situations. Its first argument is a partial goal that is called with two additional arguments, the second of which is the truth value of the goal. So, for the example above, we would need a CLP(ℤ) constraint(#>)/3, which is like(#>)/2with an additional argument for the truth value. It is possible, though a bit impractical, to add such reified versions for each arithmetic relation over integers. Currently,library(clpz)only supports(#=)/3and(#<)/3.With the new predicate
clpz_t/2, all reifiable arithmetic relations become available for use intfilter/3and other predicates fromlibrary(reif)such asif_/3etc.For instance, if we want to retain the occurrence of
#>from the example above, then we can use a lambda expression and write:This answer is correct!
Kis a solution ifKis smaller than 4.Speaking of
library(clpz)and other interesting constructs of Scryer Prolog, @aarroyoc has recently posted a great illustration of Hilbert curves:https://blog.adrianistan.eu/curva-hilbert-prolog
It uses the monotonic execution mode of
library(clpz)and the(#)/1wrapper for integer variables, it is amazing to see this used in actual application code! The example above can indeed be classified as breaking a logical property called monotonicity: A generalization of a query fails, even though a more specific instantiation succeeds. The important point is to recognize this as a correctness issue, and it is interesting that the original poster correctly recognized it as such from the beginning.And this is one of the most striking phenomena I have experienced over and over: How deeply and quickly complete newcomers are able to grasp essential aspects of Prolog and contribute in the most impressive ways to its development! This construct
clpz_t/2spawned by @librarianmage is a good example of this, and we are lucky to have already seen many other such cases during the develompent of Scryer Prolog, with most impressive contributions and keen observations from @notoria, @bakaq, @haijinSk, @flexoron and many others. I am very grateful to be able to see and participate in these developments, please keep up the great work!Thank you a lot,
Markus
Beta Was this translation helpful? Give feedback.
All reactions