[mercury-users] infinite recursion

[Fergus Henderson]

On 07-Sep-2000, Michael Day <mcda at students.cs.mu.oz.au> wrote:
> 
> > No.  Logically, the meaning of that problem according to the semantics
> > described in the "Semantics" chapter of the Mercury language reference
> > manual is just "a <=> a".  Since all that you have specified is
> > `a<=>a', which is a tautology, the compiler can't soundly infer `not
> > a' from that.  Nor can it soundly infer `a' from that either.
> > The only valid actions that an implementation can take for such code
> > are to loop forever or to throw an exception.
> 
> Oh I see. I had a quite mistaken idea of the semantics (if you can't prove
> it's true, then it's false). Would it make these things easier to debug if
> it did throw an exception rather than looping, or is the compiler
> warning/error good enough?

Well, we can't always detect such situations (classic halting problem),
there is a consistency argument in favour of doing the same thing
in the situations that we can and cannot detect.

If you run the program in the debugger (mdb) and press control-C,
it will stop at the current point, so you can see why the program was
looping.  I think that is sufficient.

> > If you use a minimal model semantics, rather than Mercury's usual
> > completion semantics, then a/0 will be false.  The Melbourne Mercury
> > compiler includes as an extension to standard Mercury a `:- pragma
> > minimal_model' declaration which gives the named predicate minimal
> > model semantics rather than completion semantics.  This is implemented
> > using tabling.  So if you add `:- pragma minimal_model(a/0).' to that
> > code, then a/0 will indeed fail.
> 
> So... minimal model assumes innocent until proven guilty, rather than
> indeterminate until proven innocent or guilty? So to speak? :)

Yes, that's the basic idea.

> Would minimal model semantics permit the writing of left recursive DCG
> parsers?

Yes.

> Is the execution model (using tabling or whatever) more
> complicated or less efficient than the execution model for completion
> semantics?

Lots more complicated, yes.  Often much less efficient (due to the
time and space overhead of maintaining the tables), but sometimes much
more efficient (it avoids recomputing answers that have already been
computed).

-- 
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.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------