[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 @ ...)

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