[m-dev.] Tabling [1/3]

[Fergus Henderson]

On 11-Mar-1998, Oliver Hutchison <ohutch at students.cs.mu.oz.au> wrote:
> On Tue, 10 Mar 1998, Fergus Henderson wrote:
> 
> > > > I don't think so.  I think that a recursive call with the same input
> > > > arguments will still always lead to infinite recursion, even with
> > > > memoing.  Isn't that correct?
> > > 
> > > No. Memoing will suspend the recursive call and then feed answers back to
> > > it through the resumption mechanism until there are no answers pending.
> > 
> > Does suspension suspend just a call, or does it suspend a whole disjunct?
> 
> Memoing suspends just the call.

Are you sure??

How do you implement that?
The variables in the following call might not have the correct insts.

The behaviour you describe below sounds much more like
suspending a whole disjunct.
(Note I said "disjunct", not "disjunction".)

> > If it suspends just a call, then later goals in this disjunct might fail,
> > leading to termination.  But if it suspends the whole disjunct,
> > I don't see how you can ever get to the situation where there are
> > no answers pending -- surely you'd still have some pending answers for the
> > predicate, namely the ones waiting for the answers for the recursive call.
> > 
> > What's the semantics of memoing?  I thought memoing wasn't supposed to
> > affect the predicate's declarative semantics.  I thought that `minimal_model'
> > was the only one that affects the semantics.  
> 
> The semantics of memoing as I have implemented it matched that of SLG-d as
> described in Kostis Sagonas' PhD theses.

Do you have a URL for that?

The SLG-d semantics is an operational semantics, I'm pretty sure.
What's the declarative semantics of memoed predicates?

The declarative semantics which SLG-d implements can't be
the completion semantics, since the behaviour you describe below
is not sound with respect to the completion semantics. 

I think there should be some way of saying that you want
memoized execution without changing the declaration semantics.
I think `pragma memo' should be that way.

If there is some other useful semantics, e.g. minimal
model or well-founded model semantics,
then there should be different pragmas to ask for them.
For example, that's what `pragma minimal_model' is for.

If I recall correctly (a big if! ;-), SLG resolution implements
the well-founded model semantics, which (again if I recall correctly)
is an extension of minimal model semantics to programs with negation.
I thought we decided to use `pragma minimal_model' simply because
that was a slightly less frightening term than `pragma well_founded_model'.

> First we get the answer 2 from the first disjunct, then on backtracking we
> detect the recursive call and suspend it. We then attempt to backtrack
> again but find no more disjuncts. At this point we return the answer 2
> through the suspended call and get the answer 3. We then return the
> answer 3 through the suspended call but the call e(3, A) fails. We are
> now in a situation where all the available answers to the subgoal p(1, A)
> have been returned to all suspended calls to this subgoal, we can then say
> that the subgoal is completely evaluated and therefore has no more answers.

The "... and therefore has no more answers" conclusion
is valid in the minimal model or well-founded model semantics,
but it's not valid according to the completion semantics.

Could you give a similar description of what happens for that example
program with `pragma minimal_model' instead of `pragma memo'?

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.