[mercury-users] infinite recursion

[Fergus Henderson]

On 06-Sep-2000, Michael Day <mcda at students.cs.mu.oz.au> wrote:
> 
> :- pred a.
> :- mode a is semidet.
> 
> a :- a.
> 
> Operationally, this is an infinite loop, which the compiler is kind enough
> to warn about. Logically, should a/0 fail?

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.

> Would it be possible for the
> compiler to make a/0 fail, or does that border on termination analysis in
> the general case?

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.

However, as the documentation says, the support for `pragma
minimal_model' in the current implementation is still unfinished --
for some examples, it gives the wrong answer.  So we don't recommend
using it.

-- 
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
--------------------------------------------------------------------------