Nooby stumped by effect of repeated rule

Steven M. Haflich wrote:

> Prolog = is not implemented
> as a functor; rather, the compiler `inlines' it when doing a Prolog
> compile.

Yes, that's exactly where I suggested the fix should go. The inlining
compile-time unifier is the function "compile-unify-variable". The fix has
to precede the call to "find-anywhere" in that function.

> Norvig's bug is that the compile-time and run-time
> unifications don't keep track of each other properly.

The compile-time unification mistakenly fails (due to find-anywhere) if the
variables are one in the same. The inliner thinks that it has a case "11"
on its hands, ie. ?x against f(?x), without first weeding out the ?x eq ?x
case - and compiles this into an immediate failure.

pt

Paul Tarvydas wrote:
> Steven M. Haflich wrote:
>
>> Prolog = is not implemented
>> as a functor; rather, the compiler `inlines' it when doing a Prolog
>> compile.
>
> Yes, that's exactly where I suggested the fix should go. The inlining
> compile-time unifier is the function "compile-unify-variable". The fix has
> to precede the call to "find-anywhere" in that function.
>
>> Norvig's bug is that the compile-time and run-time
>> unifications don't keep track of each other properly.
>
> The compile-time unification mistakenly fails (due to find-anywhere) if the
> variables are one in the same. The inliner thinks that it has a case "11"
> on its hands, ie. ?x against f(?x), without first weeding out the ?x eq ?x
> case - and compiles this into an immediate failure.

I think your analysis is going in the right direction, but i caution
that the bug may be a little more pervasive than you think. The first
indication I have about this bug was a few months ago when a customer
reported a case that reduced to this:

cl-user(16): (?- (= (a ?x c) (a (d) ?x)))
?x = c

I'm not sure this case is subsumed by your analysis, but this kind of
thing is very hard to think about. Actually, it's easy to think about,
but it is hard to think about while maintaining any confidence in the
thought process... That's why, despite this egregious bug, I really
respect Norvig's thought process.

If you devise any fix for the Norvig code befor I have time to do so,
I'd appreciate hearing about it. But make sure it corrects the above
example as well.

Ken Tilton wrote:
>
>
> Mark Tarver wrote:
>
>> I would say you have a bug in ACL Prolog. Btw what is the role of
>> Prolog in your app (just curious)?
>
>
> Suppose you want to help a student with a problem by solving for them
> one that has all the salient characteristics of their problem. The
> functional requirement is "make a new problem just like this problem
> only different". If we randomly choose new numbers, we will likely not
> get a similar problem. Consider:
>
> 5/12 * 18/5
>
> Now, having solved that problem thus:
>
> 5*6*3 / 6*2*5 ; merge and factor out gcf
>
> 3/2 ; cancel like factors
>
> ...and having all the details of the solution available (transformations
> and results and operands of each) we can try building a new problem that
> is the same. My current approach is to define methods dispatched on each
> transformation ID, eg (eql 'mrg-n-factor), and have anyone who cares
> offer constraints, such as any original numerator/denominator pair being
> co-prime (or they could just simplify that before multiplying, which
> would be a fine problem but a different kind of problem, which would be
> not fine).
>
> Long experience tells me this is a devilish problem to get right, and
> the downside is truly horrific random problems. I may yet have to role
> my own unifier, but with Prolog just sitting there...

We almost effortlessly get better problems then I ever managed before:

(generating ?x1 (with-random-gen 1 10))
(= ?x1 ?x8)
(generating ?x2 (with-random-gen 2 10))
(> ?x8 1) ;; ah, a bug, this could be one clause earlier
(= ?x2 ?x5)
(generating ?x3 (with-random-gen 2 10))
(*int ?x2 ?x3 ?x4)
(co-prime ?x4 ?x8)
(> ?x5 1)
(generating ?x6 (with-random-gen 2 10))
(*int ?x5 ?x6 ?x7)
(co-prime ?x1 ?x7)
(co-prime ?x3 ?x6)

That will rpoduce things like 5/12 * 18/5, where

x1 = x8 = 5
x2 = x5 = 6, the common factor (hmmm, maybe the transformation can use
the same variable for the gcf)
x3 = 2, and with x2 will produse the 12
x6 = 3 and with x5 will produce the 18

or...

x1/x2*x3 * x5*x6/x8

Those rules were a distillation of an awful raw set of rules obtained by
asking each different transformation in the solution to just spout
whatever constraints that transformation could think of:

(generating ?x1 (with-random-gen 1 10))
(generating ?x2 (with-random-gen 2 10))
(generating ?x3 (with-random-gen 2 10))
(*int ?x2 ?x3 ?x4)
(generating ?x5 (with-random-gen 2 10))
(generating ?x6 (with-random-gen 2 10))
(*int ?x5 ?x6 ?x7)
(generating ?x8 (with-random-gen 1 10))
(generating ?x1 (with-random-gen 1 10))
(generating ?x7 (with-random-gen 2 20))
(co-prime ?x1 ?x7)
(generating ?x4 (with-random-gen 1 10))
(generating ?x8 (with-random-gen 2 20))
(co-prime ?x4 ?x8)
(> ?x8 1)
(= ?x1 ?x8)
(generating ?x3 (with-random-gen 1 10))
(generating ?x6 (with-random-gen 2 20))
(co-prime ?x3 ?x6)
(> ?x5 1)
(= ?x2 ?x5)

First problem is redundancy. In the last line we simply copy x2 to x5,
so there is no need to be generating x5 in step 5.

Second problem is excessive backtracking due to constraints appearing
too late, and especially after generators that do not affect the
constraint. eg, (> x5 1) could be right after the generating of x5
(which is doomed to be replaced by an even higher (= x2 x5) anyway). So
we can get a bad x5 of 1 but then try 10x10x10x20x20 other bindings
before deciding against x5 as 1. ouch.

So I wrote some meta-prolog to parse the raw prolog and look for ways to
patch it up. The nice thing here is that the meta-prolog can cheat, cuz
I only ever have to parse the prolog I create and the patcher-upper can
be hard-coded for the created prolog (which can itself be created in
ways to make the patcher's life easier.

Naturally I also de-dup the thing in honor of the thread subject.

Hopefully this will continue to work for problems with longer solutions,
cuz as I said before, programmatic generation of /good/ random problems
is a total PITA, hard to get right and no fun.

This is fun.

kt

--
http://www.theoryyalgebra.com/

"In the morning, hear the Way;
in the evening, die content!"
-- Confucius

On Jan 19, 4:51 am, "Steven M. Haflich" <s...@alum.mit.edu> wrote:

> cl-user(16): (?- (= (a ?x c) (a (d) ?x)))
> ?x = c
>
> I'm not sure this case is subsumed by your analysis, but this kind of

Yes, a quick test shows that my suggested fix does not address the
above problem.

At the moment, I think that these are two separate bugs (Kenny's
problem vs. the above snippet) - but, we'll see...

> thing is very hard to think about. Actually, it's easy to think about,

After seeing the above example, I now understand your earlier
comments.

> but it is hard to think about while maintaining any confidence in the
> thought process... That's why, despite this egregious bug, I really
> respect Norvig's thought process.

This is simply "compiler optimization" thinking. 99.99% of the
optimization cases are "obvious". The other 0.0001% of cases show up
some time later.

> If you devise any fix for the Norvig code before I have time to do so,
> I'd appreciate hearing about it. But make sure it corrects the above
> example as well.

OK.

pt

I believe that these were two separate bugs and, I propose fixes for both
(see lines below marked with "pt").

The first bug (from my perspective :-) was Kenny's

(?- (= ?x ?y) (= ?x ?y))

and is solved by adding case 1a - checking for ?x eq ?x.

The second bug devolves to:

(?- (= (?x c) ((d) ?x)))

and is caused by an error in the optimization table of section 12.4 (page
402 in my copy of paip).

Case #10 involves unification of two (or more) variables, yet the "bindings"
column shows only one new binding. The table should show bindings of
(?x . ?x) and (?y . ?y). Case #10 deals with the unbound variable ?x, as
opposed to case #7 which deals with an already-bound variable (?arg1).

The compiler compiles (?- (?x c) ((d) ?x) by first unifying the two heads ?x
and (d), which is case #10. It is at this point that the original
table/code "forgets" to mark ?x as "bound" (i.e. by adding (?x . ?x) to the
bindings). When the tail is unified - c and ?x - the compiler sees that ?x
is "still unbound" and merrily compiles new binding code for it.

The proposed fix consists of breaking case 10 from case 7 and adding
(?x . ?x) to the bindings in case 10 (by calling bind-variables-in for ?x).

And, then, we notice that Norvig left an optimization on the table. In this
example, "(d)" is a constant (contains no variables), but Norvig's code
misses this case because the code checks for (consp y1) without also
checking whether y1 is manifestly constant. His code marks the last clause
of the cond as being case #9 but fails to note that it is only a sub-case
of case #9.

So, the proposed fix adds a check for manifest constant lists in the same
place as case 7&10 are weeded out. I've marked this check as case #9a.

Thankfully, the function "compile-unify-variable" has a fairly strong
precondition - X is always a variable (bound or unbound) - and, so it is
possible to think about each of the cases without getting too wooly.

Please do let me know if you agree. I know from experience that fixing
someone else's optimization code can cause new bugs to appear...

pt

(defun compile-unify-variable (x y bindings)
"X is a variable, and Y may be."
(let* ((xb (follow-binding x bindings))
(x1 (if xb (cdr xb) x))
(yb (if (variable-p y) (follow-binding y bindings)))
(y1 (if yb (cdr yb) y)))
(cond ; Case:
((or (eq x '?) (eq y '?)) (values t bindings)) ; 12
((eq x y) (values t bindings)) ; 1a same
variable - pt
((not (and (equal x x1) (equal y y1))) ; deref
(compile-unify x1 y1 bindings))
((find-anywhere x1 y1) (values nil bindings)) ; 11
((consp y1) ; 7,10,9a
(if (and (null xb) ; x unbound - pt
(not (has-variable-p y1))) ; y is a constant
list - pt
(values 't (extend-bindings x1 y1 bindings)) ; 9a - pt
(values `(unify! ,x1 ,(compile-arg y1 bindings))
(bind-variables-in y1
(if (null xb)
(bind-variables-in x1 bindings) ;
10 - pt
bindings))))) ; 7
((not (null xb))
;; i.e. x is an ?arg variable
(if (and (variable-p y1) (null yb))
(values 't (extend-bindings y1 x1 bindings)) ; 4
(values `(unify! ,x1 ,(compile-arg y1 bindings))
(extend-bindings x1 y1 bindings)))) ; 5,6
((not (null yb))
(compile-unify-variable y1 x1 bindings))
(t (values 't (extend-bindings x1 y1 bindings)))))) ; 8,9



test cases:


(?- (= (?x c) ((d) ?x)))

(?- (= ((d) ?x) (?x c)))

(?- (= (?x (d)) ((d) ?x)))

(?- (= ?x 1) (= (?x c) ((d) ?x)))

(?- (= ?x ?y) (= ?x ?y))

(?- (= ((?y) ?x) (?x c)))

(?- (= ((?y) ?x) (?x (c))))