[Prev][Next][Index]
Re: Partial Functions and Logics
In article <4109ub$kja@newsflash.concordia.ca>, chalin@cs.concordia.ca (CHALIN patrice) writes:
> [Original posting by Jones was sent to comp.specificatin.larch; I'm
> cross-posting to the Z news group since the discussion may be of
> interest to the Z people :-)]
>
> > I recently published a short note on this topic in Information
> > Processing Letters. It would be interesting to know what Larch folk
> > think about my comments. (Please e-mail - I'mm about to be away from
> > News for 10 days)
> >
> > cliff
> >
> > @article{Jones95e,
> > author = "C.B. Jones",
> > title = "Partial functions and logics: A warning",
> > journal = ipl,
> > volume = 54,
> > number = 2,
> > pages = "65--67",
> > year = 1995
> > }
>
> [Since someone also wanted the replies to be posted to
> comp.specification.larch, here is mine. A (reference to a) PostScript
> version---which is much more readable---of this message can be found in the
> WWW page http://www.cs.concordia.ca/~faculty/chalin/pfl.ps]
I have not read the Jones paper yet, so I cannot comment on that
aspect of the posting.
[..]
> Z
>
> 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
>
> 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,]. But
> nothing can be proven about the value of f.
I don't think that you can prove this. You can prove that forall i f(i) has
type Unit, but as you already said, this does not imply anything for the
values of f(i). In my understanding of [Sp88] not every well typed term
also has a value. Thus, one cannot deduce from f(i) : Unit that f(i) is
defined and has value u. If you knew that f is total, the situation would be
different.
> In Z, functions are modeled as
> sets of ordered pairs. 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. 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.
As I understand [Sp88] (pp. 69,70-71,91) the equality in Z is to be
interpreted as strict equality. Two terms are strictly equal in an
interpretation iff they are _both_ defined and evalutate to the same
value. Thus an equation of the form g(0) = 0 implies that in any
interpretation satisfying this equation g(0) (and 0) have to be
defined. Therefore g has to include at least the pair (0,0).
>
> 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
No, according to [Sp89, p. 43] the proper form would be
axdef
f: ZZ -+> Unit
where
dom f = {- 1, 0, 1}
forall i : {-1, 0, 1} @ f i = if i = 0 then u else f (i - 1)
end
This difference is important as it states that the equation f(i) = .. is
not required to hold for values other than {-1, 0, 1}. If this restriction
is not made the equation can also be applied to values of i not in {-1, 0,
1}, eg. i = 2. Because of strict equality we can then show that f(2) = 0 and
thus 2 is in the domain of f (eg. 2 \in dom f) which contradicts the
statement dom f = {-1, 0, 1}.
However, another contradiction yields the inclusion of -1 into dom f. If -1
is in the domain of f then f(-1) has to be defined. Applying the above
equation yields f(-1) = f(-2). Because of strict equality and the assumption
that f(-1) is defined f(-2) is defined and therefore an element of dom(f)
which is a contradiction of the restriction of dom(f) to {-1,0,1}.
Thus the Z specification restricting the defintion of f to {0,1} should read
axdef
f: ZZ -+> Unit
where
dom f = {0, 1}
forall i : {0, 1} @ f i = if i = 0 then u else f (i - 1)
end
>
> In which case there is a unique solution f = {(-1,u),(0,u),(1,u)}.
>
> 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)}.
I would be very surprised to see the application of F to -1
terminate. The least fixpoint is {(i,0) | i >= 0}.
> 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. 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.
As in the example of g, (0,0) is an element of f. Consider the right
side of the equation below and i = 0 and assume that the
interpretation of if-then-else is as usual _not_ strict. Then the
right side of the equation evaluates in any interpretation of f to 0.
This means that for any interpretation satisfying the equation the
application of f to 0 has to be defined (using again strict
equality). And for that matter all interpretations satisfying the
equation
f(x) = if x = 0 then 0 else f(x-1)
have to have the set {(i,0) | i >= 0} as subset of the interpretation
of f. You can verify this by taking a sound deduction system and try
to prove eg. f(3) = 0 using the above equation (eg. equality
reasoning). This means (as the deduction system is sound) all
interpretations satisfying the above equation have to have the pair
(3,0) included into their interpretation of f. However, you cannot
prove f(-1) = 0. If the deduction system is complete this implies
that there exists an interpretation not including the pair (-1,0) in
their interpretation of f.
[..]
> Jon95
> C.B. Jones. Partial functions and logics: A warning. Information
> Processing Letters, 54(2):65--67, 1995.
>
> Spi88
> J.M. Spivey. Understanding Z: A Specification Language and its
> Formal Semantics, volume 3 of Cambridge Tracts in Theoretical
> Computer Science. Cambridge University Press, January 1988.
[..]
Hubert
--
Hubert Baumeister
MPI Informatik, Im Stadtwald,
D-66123 Saarbr"ucken, Germany
Phone: (x49-681)302-5432 Fax: -5401
e-mail: hubert@mpi-sb.mpg.de WWW: http://www.mpi-sb.mpg.de/~hubert/
Follow-Up(s):
Reference(s):