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

[Mark Brown]

On 21-Jul-2006, Peter Moulder <Peter.Moulder at infotech.monash.edu.au> wrote:
> On Wed, May 31, 2006 at 11:29:44AM +1000, Ralph Becket wrote:
> 
> > I used to think the same way [that function calls are just an
> > alternative syntax for predicate calls], but I've been convinced
> > otherwise.  The main thing is that with functions it is natural to
> > assume referential transparency.
> 
> That may well be a natural assumption, but it's unfortunately a false
> one in Mercury: that is, the code
> 
>    f \= f
> 
> can succeed (where f is a function application in the usual forward
> direction) even though
> 
>    Z = f,
>    Z \= Z
> 
> always fails.  (Even if the NaN problem were fixed.)

This doesn't demonstrate referential opacity.  That is, you can't get from
one to the other by substituting equals for equals.

However, it is not the referential transparency per se that is important,
but the fact that the reasoning is natural for human beings.  And, in my
view, the reasoning that says the above two goals should be equivalent
is fairly natural.

Even more disturbing to my notion of natural is the fact that a simple
goal such as `f = f' can fail if `f' is a semidet function.  Apparently,
then, the axiom `X = X' does not hold, which belies the statement in the
semantics chapter of the reference manual that the semantics of a Mercury
program includes "the usual equality axioms".

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

---

For modelling problems, partial functions are a useful concept -- more useful
than nondet functions, in my view -- even though the above examples illustrate
the complexity that is added to the language semantics.  The question for
Mercury users is: are partial functions useful enough to justify the
complexity they add to the semantics?

(In any case, the semantics chapter should be fixed so that it explicitly
defines the predicate calculus theory of a Mercury program, rather than
relying on ill-defined statements such as "the usual axioms".  And preferably
the definition should match what the implementation actually does!)

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