problem with recursion in axiom

[ko56]

Please look at this example:

(in-package :shop-user)

(defdomain simple
  (
    (:- (route ?x ?y)
      direct
      (or (road ?x ?y) (road ?y ?x))
      indirect
      ; Cumbersome! ∃u.f(u) written as ~∀u.~f(u).
      ; ~(∀u ~(((road x u) ∨ (road u x)) ∧ (route u y)))
      (not (forall (?u) ()
	     (not (and (or (road ?x ?u) (road ?u ?x)) (route ?u ?y)))))
      )

    (:method (travel ?x ?y)
      (route ?x ?y)
      ()
      )
    )
  )

(defproblem p1 simple
  ((road a b) (road b c))
  ((travel a c))  ; fine
  ; ((travel a d))  ; exhausts control stack
  )

(find-plans 'p1)

I don't know how to fix the axiom. I tried adding (loc a) (loc b) (loc c) to the problem, and replacing the
empty expression in the forall by (loc ?u), thinking that this would prevent application to 'd', but that didn't work.
Am I missing something here? With 'u' unrestricted, it's not surprising that the recursion is infinite.

[rpgoldman]

Sorry I lost track of this and didn't answer...

Here's a working solution:

(defdomain simple
  (
    (:- (route ?x ?y)
      direct
      ((direct-connection ?x ?y))
      indirect
      ((direct-connection ?x ?z)
       (indirect-connection ?z ?y (?x))))

   ;; Is there a path from ?start to ?end that does not pass
   ;; through any of the nodes in ?disallowed
   (:- (indirect-connection ?start ?end ?disallowed)
       ((direct-connection ?start ?end))
       ((direct-connection ?start ?mid)
        (not (= ?mid ?end))
        (not
         (call member (quote ?mid) ?disallowed))
        (assign ?new-disallowed (cons '?mid ?disallowed))
        (indirect-connection ?mid ?end ?new-disallowed)))

   (:- (direct-connection ?x ?y)
       ((road ?x ?y))
       ((road ?y ?x)))

   (:- (= ?x ?x)
	   ())

    (:method (travel ?x ?y)
      (route ?x ?y)
      ()
      )
    )
  )

This changes your axiom to avoid having cycles in a path. I think I have gotten it right. I also pulled it apart into multiple different axioms which is less efficient, but makes the domain easier to understand.

A better solution would be to add a special-purpose lisp function that would run some efficient algorithm (transitive closure) and respond to queries like (call graph-reachable-p (quote ?start) (quote ?end))

[ko56]

Thanks for the reply. If I were writing an algorithm in Lisp to find
undirected paths in a graph I would probably end up with something
like what you wrote (to handle cycles).

After thinking about it for a while, the real issue in my mind is my
understanding, or lack thereof, of axioms in SHOP3. So I have some
questions:

1. The (recursive) axiom evaluation. It seems that an axiom can
   involve arbitrary (Lisp) functions, as long as they return booleans.
   How is an axiom evaluated in a state (sec. 10 of manual)? Is the
   theorem prover used? Or just Lisp, somehow? If it's the theorem
   prover, it seems to me that I should be able to write a recursive
   axiom like my original one, and the theorem prover should not get into
   an infinite recursion. In any case, some clarification is needed
   here, and it would be good to include it in the manual.

2. How can I write a "headless" axiom? E.g. to express
   ∀x,y r(x,y) ⇒ r(y,x)?
   Apparently the parser accepts such a construct, see item 3.

3. By tracing the axioms in this modified example (see below), it
   appears that the "road symmetry" axiom is never used. Apart from the
   violation of the syntax, I don't understand why that is. It does not
   accord with sec. 10.1.2 of the manual, which seems to say that axioms
   are invoked automatically, so to speak.

4. Doesn't an axiom a(...) hold iff (E1 ∨ ... ∨ En)?

5. This has to do with quantifiers. Given the substitution/satisfier
   framework presented in sec. 10.1, it would seem that existential
   quantification in logical expressions is not needed? Is this correct?
   If so, a note should be added to the manual in sec. 4.5.5.
   The situtation is even more confusing for someone who knows PDDL, where
   there are existential quantifiers.

Apart from the above, I've taken the latest master copy of the manual
and made some more edits, as I read through various parts more
carefully. (In particular, see if you agree with the comments I added
in sec. 4.1 and 4.3 on predicates and functions.) Here is
manual.patch.gz

And the modified example:

(in-package :shop-user)

(defdomain simple
  (

    ; the 'road' relation is symmetric:
    ; The following violates the syntax, but is accepted
    (:-
      (forall (?x ?y) (implies (road ?x ?y) (road ?y ?x)))
      )

    ; defn. of routes/paths:
    (:- (route ?x ?y)
      dir-rt
      (road ?x ?y)
      ind-rt
      (and (road ?x ?u) (route ?u ?y))
      )

    (:op (!goto ?l)
      :add ((at ?l))
      )

    (:method (travel ?x ?y)
      doit
      (route ?x ?y)
      ((!goto ?y))
      )
    )
  )

(defproblem p1 simple
  (
    (at a)
    (road a b) (road c b) (road c d)
    )
    ((travel a c))
  )


(find-plans 'p1 :verbose :long-plans)

[rpgoldman]

1. The (recursive) axiom evaluation.  It seems that an axiom can
   involve arbitrary (Lisp) functions, as long as they return booleans.
   How is an axiom evaluated in a state (sec. 10 of manual)?  Is the
   theorem prover used?  Or just Lisp, somehow?  If it's the theorem
   prover, it seems to me that I should be able to write a recursive
   axiom like my original one, and the theorem prover should not get into
   an infinite recursion.  In any case, some clarification is needed
   here, and it would be good to include it in the manual.

An axiom may invoke arbitrary lisp functions, but only through the eval, call, and assign family of pseudo-predicates. Note that these functions do not have access to the current state except by using the special variable shop::*current-state*.

Other predicates are addressed through the theorem-prover. The theorem prover knows about SHOP's state and queries will be evaluated in the context of the current state.

By default, the theorem prover will search for all solutions to a query (you can use the :just-one flag to avoid this), and recursive queries will cause the theorem-prover to go away forever.

For a theorem-prover to avoid such infinite recursions requires very expensive checking for visiting repeated nodes in search, and SHOP does not make any such checks.

2. How can I write a "headless" axiom?  E.g. to express
   ∀x,y r(x,y) ⇒ r(y,x)?
   Apparently the parser accepts such a construct, see item 3.

You cannot. The SHOP syntax is Prolog-like Horn clauses, and Horn clauses always have heads (this oversimplifies a little). A Horn clause (:- (P ?x) (Q ?x)) for example means

Forall x Q(x) implies P(x)

(note the inverse direction)

If you want to say r is symmetric, as above, you would say:

(:- (r ?x ?y) ((r ?y ?x)))

but this will cause infinite recursion. A common trick is to break the recursion by defining the predicate r in terms of an auxiliary predicate that means something like "r is in the data base":

(:- (r ?x ?y) 
    ((explicit-r ?x ?y))
    ((explicit-r ?y ?x)))

The database will only have facts about explicit-r and there will be no rules with explicit-r in their head, and so no recursion.

3. By tracing the axioms in this modified example (see below), it
   appears that the "road symmetry" axiom is never used.  Apart from the
   violation of the syntax, I don't understand why that is.  It does not
   accord with sec. 10.1.2 of the manual, which seems to say that axioms
   are invoked automatically, so to speak.

The SHOP axiom tracer is not guaranteed -- I have never really checked it for correctness (it comes from the original SHOP2 code). It's possible it only prints after processing an axiom is done, in which case you would never see anything printed in the case of the infinite recursion. Try tracing a "Normal" non-recursive axiom and see what happens. If it does not work properly, please post an issue.

4. Doesn't an axiom a(...) hold iff (E1 ∨ ... ∨ En)?

More exactly, it's

(E1 v (~E1 ^ E2) v (~E1 ^ ~E2 ^ E3) ... v (~E1 ^ ~E2 ^ ~E3 ... ^ ~En-1 ^ En)

5. This has to do with quantifiers.  Given the substitution/satisfier
   framework presented in sec. 10.1, it would seem that existential
   quantification in logical expressions is not needed?  Is this correct?
   If so, a note should be added to the manual in sec. 4.5.5.
   The situation is even more confusing for someone who knows PDDL, where
   there are existential quantifiers.

That is correct. Formally, what is going on here (I'm a little rusty, but I think I have the terminology correct) is resolution refutation. So the way you answer a query like (P ?x) is to try to refute (contradict it). So you try to disprove (P ?x). Unbound variables here are implicitly universally quantified, so the theorem prover will try to disprove

Forall ?x ~P(?x)

Now, to disprove that you have to prove

Exists ?x P(?x)

and that is what SHOP's theorem-prover is doing. It is trying to find all bindings of ?x (or only one if you use :just-one) that make

P(?x)

true.

What SHOP is doing with its axioms is not PDDL-like -- it is Prolog-like. PDDL axioms are much more limited than SHOP axioms, and SHOP's language is actually older than PDDL.

[ko56]

Thanks very much for the explanations. While I'm digesting them,
an additional clarification on #4:

x ∨ (¬x ∧ y) ∨ (¬x ∧ ¬y ∧ z) ... is equivalent to (x ∨ y ∨ z ...)

So I don't understand why a more complicated explanation of the
semantics of an axiom is needed than just saying

e1 ∨ ... ∨ en ⇒ a(t1 ... tm)

In view of all this disussion, I find the matter of axioms worthy of
more explanation for the non-expert. Are you amenable to me
augmenting sec. 4.7 of the manual with some of the things you wrote,
and the notes on p. 48 on axioms? Or creating an appendix with all of
this?

[rpgoldman]

x ∨ (¬x ∧ y) ∨ (¬x ∧ ¬y ∧ z) ... is equivalent to (x ∨ y ∨ z ...)

So I don't understand why a more complicated explanation of the
semantics of an axiom is needed than just saying

Logically, they are the same, but procedurally they are not. (For more details, see a discussion of Prolog's "cut" operation)). If x is true, the search for solutions terminates. Or, if x is false and y is true, then the search terminates, etc.

The logic doesn't fully capture the procedural semantics. The procedural semantics are "if-then-else" not "or."

I don't object to adding a discussion, but we should take into account the conceptual framework it is built upon.

[ko56]

OK, I see. I thought something like that might be be the reason. The cut is somewhat similar to short-circuit evaluation.

Let me know how you want to proceed with the new material.