[mercury-users] infinite recursion

[Fergus Henderson]

On 06-Sep-2000, Ralph Becket <rbeck at microsoft.com> wrote:
> > From: Michael Day [mailto:mcda at students.cs.mu.oz.au]
> > 
> > :- 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: translating the above clause into FOL we have a <= a, and
> (a <= a)  <=>  (~a \/ a)  <=>  true

OK so far...  You forgot to take the completion
(it should be `a <=> a' rather than `a <= a'),
but it doesn't make any difference to the end result,
which is still just the vacuous statement `true'.

> So a/0 should be det and true.

No, that's not correct.  The program is equivalent to `true',
but the statement `true' is just expression a vacuous tautology;
it says nothing about the truth or falsity of `a'.
Nor does it say anything about the truth or falsity of `b', `c', etc.

If the simplified program was `a', you could conclude that a/0 is true.
But from the simplified program `true' you can't conclude anything
that you didn't know already.

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