external-access-hook-query

[ko56]

I want to make sure I understand the function of this hook.
a) It is used at plan generation time, correct?
b) It is, essentially, a convenience, and does not extend SHOP3's plan-generation capabilities.
That is, whatever information is returned could have been put into the problem file to start with.
Correct?

[rpgoldman]

I want to make sure I understand the function of this hook.
a) It is used at plan generation time, correct?

Yes, that is correct.

b) It is, essentially, a convenience, and does not extend SHOP3's plan-generation capabilities.
That is, whatever information is returned could have been put into the problem file to start with.
Correct?

That is not quite correct: one can use the external-access-hook to handle terms with non-finite domains of quantification, such as numerals. At least in theory, the state (which is what I believe you refer to when you talk about the problem file) must be of finite extent (and the bit-vector state representation relies on this).

That said, the external-access-hook seems to me to be redundant with the axiom facility and the ability to invoke arbitrary lisp code in preconditions. As far as I can tell, anything one can do with the external access hook could be done with those facilities.

I am not fully confident in this response because I have never used this facility, and there are no examples of its use in the set of examples distributed with SHOP3. Unfortunately, when the source code was imported into the repository, previous history was lost, and I don't have any history. The only history I have is from SIFT, nothing from U Maryland where this was first implemented:

;;   2003.7.9 (jwm) Revised the external-access-hook mechanism (see
;;   the 2003.4.21 revision, below).  There is a new keyword for the
;;   theorem prover: :external.  Any expression that begins with
;;   :external has the following semantics: If there is an
;;   external-access-hook defined, any attempt to prove (:external A B
;;   C ...)  will return the results of running external-access-hook
;;   on the list '(A B C ...).  If there is no external-access-hook
;;   defined, any attempt to prove (:external A B C ...) will return
;;   nil.  In addition, assertions obtained from calling the
;;   external-access-hook are added to the internal state.

(from the changelog)

@ukuter might know more.

[ko56]

That said, the external-access-hook seems to me to be redundant with the axiom facility and the ability to invoke arbitrary lisp code in preconditions. As far as I can tell, anything one can do with the external access hook could be done with those facilities.

OK, good, I was thinking exactly the same thing. Perhaps this is another possible revision to the manual.
Speaking of that, please look at #76, the diff file I posted a couple of weeks ago.

[ko56]

That is not quite correct: one can use the external-access-hook to handle terms with non-finite domains of quantification, such as numerals. At least in theory, the state (which is what I believe you refer to when you talk about the problem file)

I am talking about the defproblem statement (which I would normally put in its own file), so yes, the initial state.

must be of finite extent (and the bit-vector state representation relies on this).

I'm not quite following this. How can I define an initial state that is not of finite extent, numerals or not?
Any numeral I include will of necessity be finite.

[rpgoldman]

I should have been more clear. What I should have said was that the state-space was non-finite.

Classical AI planning assumes that the state space, while it can be very large, is finite. What this means is that if there are variables in operator schemas, those variables must have finite domains of quantification. So the integers, reals, etc. cannot be used. The proofs of decidability rely on this.

In practice, of course, most uses of non-finite domains of quantification can be made without causing problems for decidability. For example, if you have a finite graph, and you have a predicate that tells you the distance between any two points in the graph, there will be only a finite number of such values, so even though we might use float-valued variables, we aren't necessarily making things undecidable.

In theory, although inefficient, we could write down a full distance table into the initial state (and if you look at some of the International Planning Competition domains, you will see that's exactly what they do).

[ko56]

Yes, understood. You did say

terms with non-finite domains of quantification

but I was distracted by the next statement about the state.