[mercury-users] functions vs predicates (was Re: State variable problem

Peter Schachte schachte at csse.unimelb.edu.au
Tue Aug 15 12:36:14 AEST 2006


On Tue, Aug 15, 2006 at 11:39:56AM +1000, Ralph Becket wrote:
> Peter Schachte, Tuesday, 15 August 2006:

> > I'm not so sure what people's natural expectation is in this case.  If
> > our domain is the natural numbers, would you expect 0-1 = 1-2?  I
> > guess I wouldn't be surprised either way.  How about 1/0 = 2/0?
> 
> Neither of those matches X = X.

I was trying to get at the issue of whether all failures are created
equal.

> I'm pretty sure that extending the axiom "X = X" to "X = X, except if
> evaluating X throws an exception" would not muddy the waters too much.

Agreed.  We already have to put in the proviso that both comparands
terminate; refining it to "X=X whenever X terminates without throwing
an exception" isn't too bad.  But if we get rid of semidet functions,
we can say something stronger:  X = X never fails, and X \= X never
succeeds.

-- 
Peter Schachte              Reality is for those who can't face Science
schachte at cs.mu.OZ.AU        Fiction. 
www.cs.mu.oz.au/~schachte/  
Phone: +61 3 8344 1338      
--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------



More information about the users mailing list