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

[Mark Brown]

On 14-Aug-2006, Peter Schachte <schachte at csse.unimelb.edu.au> wrote:
> On Mon, Aug 14, 2006 at 05:20:53PM +1000, Mark Brown wrote:
> > On 21-Jul-2006, Peter Moulder <Peter.Moulder at infotech.monash.edu.au> wrote:
> 
> > > This problem arises with function applications that fail: f \= f is
> > > converted to not(f = f), which becomes not(f = Tmp1, f = Tmp2, Tmp1 =
> > > Tmp2), where the `f = Tmp' calls are treated like predicate calls:
> > > failure of the call means success of the `not' goal, i.e. success of
> > > f \= f.
> > 
> > The explanation for this behaviour is that Mercury follows a simple rule
> > for partial (semidet) functions: any atomic formula containing an undefined
> > term -- a function application that fails -- is false.  The crucial part is
> > that this only applies to _atomic_ formulas.  The goal `f \= f' is not
> > atomic, as it is just syntactic sugar for the compound formula `not (f = f)';
> > in this case it is the atomic goal `f = f' that is false, and thus fails.
> 
> It'd be a shame to give up partial functions.

I'm inclined to agree.  But I also think that partial functions are trickier,
semantically, than people tend to realise (or maybe it is just me :-S).

> Do they have problems
> other than with negation?

I think the real problem is that `X = X' doesn't hold, but people would
naturally expect it to.

> If it's just negation, negation could be
> redefined to specify that function calls are executed *outside* the
> negation.  Ie, a negated goal would be defined to mean that all the
> contained function calls are well-defind (succeed) and the negated
> goal fails.
> 
> Eg, this example would be implemented as
> 
> 	f = Tmp1, f = Tmp2, not(Tmp1 = Tmp2)

This definitely wouldn't be referentially transparent!  In particular,
the meaning of `not Goal' would no longer depend only on the meaning of
`not' and the meaning of `Goal'.  Unless we dispense with classical logic
altogether, that is.

Cheers,
Mark.

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