[m-dev.] functions whose forward mode fails (was Re: Suggestion for a new "where" operator
Peter Moulder
pmoulder at mail.csse.monash.edu.au
Sat Aug 9 15:26:38 AEST 2003
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.
Attempting to divide by a string or a bool gives a compile-time error,
which is better still. Sometimes we can use modes to get compile-time
errors.
Given that we do have such experience with e.g. division not being
defined for all arguments "of its input type", I find it surprising that
I don't know the mathematically correct interpretation of statements
involving quantification and partial functions. Let's start with
nullary "functions" / constants (e.g. `:- mode f = out is failure'). In
mathematics, what is the truth of p(f), where p is a predicate defined
as all[X] p(X) ? Is it true, undefined, or false as in mercury? What
about `f = f' ? (False in mercury.)
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)' ?
foldoc: "To be unambiguous, the set to which the values of the variable
belong should be specified, though this is often omitted when it is
clear from the context".
When scribbling on paper, I find it convenient to write, say, `all[i]
x_i = 0', and have it understood that i should range over the domain of
the subscript operator (natural numbers less than n).
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". One might (optimistically...) hope that the
inferred "type" for X would take into consideration the domains of
functions in which X is an argument. ("Optimistically": one couldn't in
general expect a compiler to calculate the domain of a function, though
one might hope to be allowed to specify a domain just as we allow
specification of simple types (int etc.).) Such a hope does of course
depend on a certain understanding of what "type" means.
One interesting aspect of the `f = f' case is interesting in that it
demonstrates a difference between F and apply(F). (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. E.g. propositions 58 and 34 in
http://mizar.uwb.edu.pl/JFM/Vol1/partfun1.html.)
Introspection (type_of etc.) is presumably another way in which nullary
higher-order terms are differentiable from the result of applying those
terms.
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. 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. 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.
AFAICT, neither MathML nor OpenMath describe the meaning of quantifiers
(let alone partial functions) in any great detail.
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', and that `not(p(f))' can differ from `not_p(f)' where
`not_p(X):- not(p(X))', and similarly `not(p(f))' can differ from
`some[V1] (V1 = f, not(p(V1)))'.
One possible response might be `functions that fail in their forward
mode are bad, so take steps to reduce (or eliminate) their use in
Mercury code'. A response towards the opposite direction might be
`given that we allow this surprising behaviour ---i.e. given that
reasoning about mercury code in general requires transforming function
calls to predicate calls--- it mightn't be so bad to allow other
surprising behaviour, perhaps even nondet expressions'.
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. Perhaps a good place might be near where we say that
functions' forward mode cannot be multi/nondet (currently node
Determinism categories). Doing so fosters understanding of the issues
and perhaps better decision-making regarding any of the more radical
responses, or when adding more semidet functions and function-like
expressions to the standard library or language or
independently-developed libraries.
pjm.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------
More information about the developers
mailing list