[m-dev.] functions whose forward mode fails (was Re: Suggestion for a new "where" operator

[Fergus Henderson]

On 07-Aug-2003, Peter Moulder <pmoulder at mail.csse.monash.edu.au> wrote:
> On Tue, Aug 05, 2003 at 11:58:50AM +1000, Fergus Henderson wrote:
> 
> > > [EXPR = EXPR can fail when using functions whose forward mode fails]
> 
> > Yes, that's not the reason why Mercury doesn't support multi/nondet functions.
> > The reason is that if functions were allowed to be nondet in their forwards
> > mode, `X = f, p(X, X)' could mean something different than `p(f, f)'.
> 
> Is it a problem that
> 
>    X = f, not p(X)
> 
> means something different than
> 
>    not p(f)
> 
> ?

Actually, yes, partial functions do make reasoning about code a bit
more difficult.

However, we allow this because humanity has had thousands of years of
experience in reasoning about partial functions.  Mathematically speaking,
the division function, which everyone gets exposed to from an early age,
is a partial function because division by zero is undefined.  So people
are supposed to be used to dealing with partial functions.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------