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

[Fergus Henderson]

On 09-Aug-2003, Peter Moulder <pmoulder at mail.csse.monash.edu.au> wrote:
> On Fri, Aug 08, 2003 at 06:32:52PM +1000, Fergus Henderson wrote:
> > 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.
> 
> All divide operators in mercury throw an exception on division (other
> than unchecked_quotient etc.).  I think this gives less surprising
> behaviour than functions that fail in their forward mode.

There are certainly important practical advantages to this approach.
But the declarative semantics with this approach are surprising.
For example, in Mercury the goal 

	some [X `with_type` integer, Y `with_type` integer]
		((X * Y) / Y \= X)

is true.  The same is the case for the analagous goal in Goedel.
This is because the although the operational semantics says that
0 / 0 will throw an exception, the declarative semantics says that
0 / 0 has some unspecified value.

Haskell has a different approach where these exceptional results
are made part of the denotational semantics, rather than being
just part of the operational semantics.  But this requires adding
error values to every type, which has its own drawbacks.

> Now suppose that f1 is an empty unary function (`:- mode f1(in) = out is
> failure').  What's the truth of `all[X] p(f(X))' given `all[X] p(X)' ?

If f(X) fails for any X then `all[X] p(f(X))' is false.

> One reason I mentioned types above is that universal quantification in
> Mercury is (I believe) implicitly understood to range only over values
> of the appropriate "type".

That's correct.

> One might (optimistically...) hope that the
> inferred "type" for X would take into consideration the domains of
> functions in which X is an argument.

Definitely not!

> One interesting aspect of the `f = f' case is interesting in that it
> demonstrates a difference between F and apply(F).

Certainly `F' and `apply(F)' are different.
If they weren't, there would be no point having apply/1 in the language.

> (Comparison of
> functions/predicates is currently disallowed in Mercury given that the
> question is undecidable in general, but mathematically empty functions
> are considered equal, I believe.

If they are of the same type, then yes.

> E.g. propositions 58 and 34 in
> http://mizar.uwb.edu.pl/JFM/Vol1/partfun1.html.

Proposition 34 holds in Mercury.  Proposition 58 holds in Mercury if
you restrict the functions f1 and f2 to being of the same type, but does
not hold in the case where f1 and f2 have different types.  (The paper
that you cite seems to be using an untyped calculus.)

> Introspection (type_of etc.) is presumably another way in which nullary
> higher-order terms are differentiable from the result of applying those
> terms.

Right.

> I'm not familiar with Mizar, but it looks to me as if proposition 69 on
> the above-referenced page uses quantification involving undefined
> partial function application, considering the case where dom f is the
> empty set.  f is then a function from {x} to Y, from propositions 28,29.  
> And f(x) is undefined.

Mizar defines the notation `f(x)' so that in the case when x is not an
element of dom f, f(x) = the empty set.
(Reference: http://mizar.org/JFM/pdf/funct_1.pdf, definition 4 (ii).)

> I'd guess that Mizar accepts this because of
> the definition of \subseteq would in this case expand to `all[e] (e \in
> \emptyset => ...)' which would be true regardless of whether `...'
> contains undefined function applications.

Right.

> However, in Mercury the above
> `all[X] p(X)' examples show that if `\subseteq' were implemented as a
> Mercury predicate then "empty `subseteq` singleton(f(x))" would be
> considered false, because it would expand to `some[V1] (V1 = f(x),
> subseteq(...))', where that first conjunct is false, so the expression
> as a whole is considered false regardless of the definition of subseteq.

Yes.  Mizar has a different treatment of partial functions than Mercury.
Mizar defines the result of applying a partial function to a value which
is not in the domain of that function to be the empty set.  In Mercury,
such a definition would not be type-correct.

> Although I haven't ascertained what "standard mathematical treatment" of
> partial functions is in predicates, there is evidence that Mercury's
> treatment differs from that of Mizar, and we do have some "surprising"
> properties such as that `f = f' cannot in general be replaced with
> `true',

Mizar's system also has some surprising results, such as the fact that
x / y = z does not imply x = y * z.

> In any case, a reasonable step to do first would be to raise awareness
> of the issues by documenting the surprises explicitly, to make them less
> surprising.

This is a good suggestion; patches welcome!

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