[Prev][Next][Index]
Re: Partial Functions and Logics
Patrice Chalin writes:
[.. stuff about Larch deleted ...]
Consider a Z version of the first example used in [Jon95]. Actually, because
of the way types are defined I must slightly change the example (reasons
for doing so are given in Note below).
[Unit]
axdef
u: Unit
where
Unit = {u}
end
axdef
f: ZZ -+> Unit
where
f i = if i = 0 then u else f (i - 1)
end
This spec is ill formed, because there is no declaration of the
variable i. But let's suppose that you wrote (forall i : ZZ @ ...)
instead.
From this specification (let us call it SPEC1) we can prove that
forall i: ZZ @ f i = u
This property follows from the fact that the value of a term is
always an element of the carrier set of the type of the term
[Spi88, pp.61--62,].
This isn't so: the value of an expression is a member of the carrier
of its type only if the expression is defined. Expressions can also
be undefined.
In this example, as always, we have to ask what functions f satisfy
your specification. Certainly the (total) constant function from ZZ
to Unit satisfies it; but so may some other functions -- we just can't
tell, because Z does not tell us whether E1 = E2 is true or false in
the case where one or both of them is undefined.
[...]
In Z, functions are modeled as sets of ordered pairs.
Agreed.
SPEC1 does not uniquely determine f: there are many
sets satisfying the definition of f in SPEC1; viz. { },
{(0,u)}, {(1,u), (-1,u)}, etc.
Actually, SPEC1 may or may not determine f, depending on the answers
to questions about equality that we should not ask.
To consider a simpler example,
axdef
g: ZZ -+> ZZ
where
g 0 = 0
end
does not allow us to deduce that (0,0) \in g unless we know that
0 \in \dom g.
True
By the ``customary Z stylistic guidelines'', the SPEC1 definition of f
would be considered incomplete. Spivey writes, ``Partial functions may be
defined by giving their domain and their value for each argument in the
domain''; by doing so we completely determine the partial function being
defined [Spi89, p.43,]. Thus, in general, partial functions can be defined
using recursive equations only if their domains have been fixed (outside of
the recursive equation). Hence, a ``proper'' definition of f would be, e.g.
axdef
f: ZZ -+> Unit
where
dom f = {- 1, 0, 1}
f i = if i = 0 then u else f (i - 1)
end
Again a missing quantifier here -- it should be (forall i: {0, 1} @ ...)
I think.
In which case there is a unique solution f = {(-1,u),(0,u),(1,u)}.
OK.
This brings me to an interesting observation that I made several years ago.
In the semantics of programming languages one tends to require that, e.g., a
function definition, have a single denotation. For example, the denotation
of F in
function F(i:integer):integer
begin
if i = 0 then F := 0
else F := F(i-1)
end;
would be the appropriate least fixed point: {i: @ (i,u)} {i: @
(-i,u)}. In contrast to this approach, it would seem that in the
semantics of specifications languages, we tend to speak of the
structures (or models) that satisfy a given specification. For
example, there are many (nonisomorhpic) models that satisfy SPEC1:
in particular one model will assign { } to f, another will assign
{(0,u)} to f, etc.
Again, we do not know whether these are models or not
Hence we do not seek a single denotation for
components of a specification. With respect to a given
specification, what usually concerns us are those properties that
are logical consequences of that specification: i.e. properties
that hold in all models that satisfy the specification. Thus, the
specification of g does not allow us to deduce that (0,0) \in g
since this statement does not hold in all models that satisfy the
definition of g.
This is a good point, but one that is slightly undermined by Z's
treatment of partial functions.
``... it would seem on closer investigation that `Z' might have some
difficulty in fixing denotations of its recursive functions.'' [Jon95]
In the light of what I stated above, it would not seem necessary
that `Z' fix denotations for its recursively defined functions
since this is not the kind of interpretation that is applied to Z
specifications.
It's true that Z does not necessarily fix on one interpretation of a
recursive definition, but that doesn't make the problem go away. We
want to develop progams that contain recursive functions, and we'll
need to prove that the recursion terminates. All that Z seems to say is
that this is a completely separate problem from defining functions in
mathematics!
Reference(s):