T* introspective rules

16 views
Skip to first unread message

nha...@gmail.com

unread,
Jan 30, 2023, 5:43:22 AM1/30/23
to Shen
So I was adding some debug code to T* to help track down a problem. The name of the currently active sequent rule is added to the context before running it:

(defprolog search-user-datatypes
   P Hyp (- [[Key | Fn] | _]) <-- (call (Fn P [[datatype Key]|Hyp]));
   P Hyp (- [_ | Ds]) <-- (search-user-datatypes P Hyp Ds);)

Which gives you a call stack to help identify why 'P' is being attempted.

But aside from that, it seems like it could be used to prevent expansive rules from feeding back into themselves, by searching the context for their own name. What are the practical implications of having such 'one-shot' rules? Is there any 'logical' interpretation of them, or is it just another extra-logical feature that makes things more complicated to reason about?

Mark Tarver

unread,
Jan 30, 2023, 12:04:52 PM1/30/23
to Shen
This is a part of a general problem in logic programming which is the detection and trapping of infinite loops; that is, infinite branches in search space
which under unbounded depth-first search create non-terminating programs.  In general this problem is not solvable.  It is solvable for a certain class
of infinite loops where the goal repeats.  This is called subsumption testing and it says that if you reave a search path 

g1
 |
 |
 V
 g2
 |
 |
 V
g3

where g1 .. g3 are each a series of Prolog goals each derived form the predecessor by resolution with a program clause
then if g1 subsumes g3 i.e. there is a substition s of the variables in g1 such that s(g1) = g3 
then you can discontinue the search down this path.  Prolog + subsumption allows you to have rules like

brother(X,Y) :- brother(Y,X).

w.o. looping.  AFAIK, if you augment Prolog with subsumption it is complete for Datalog; i.e. function-free Prolog.

However there is another form of looping involving functions which cannot be reliably trapped.

jewish(X) : jewish(mother(X)).

creates a loop which is not trapped by subsumption.

The same holds for Shen derivation rules except the subumption test would be formulated differently.

If you have an expansive rule you can always trap it like this - by raising a flag that signifies the rule is not to be used again.

(datatype jewish

  !; fail;
  ____________________
  (- dont-use-me) >> P;

  dont-use-me >> (jewish (mother X));
  __________________________________
  (jewish X);)

But of course you lose completeness by so doing.

M.
Reply all
Reply to author
Forward
0 new messages