[Prev][Next][Index]
Partial Functions and Logics
[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]
Here is the abstract of [Jon95]
One approach to handling partial functions when specifying and
reasoning about programs is to say that application outside their
domain yields an indeterminate element of their range. This paper
puts forward a counter example which suggests that this approach
might be problematic in a specification language.
I fail to see the problem that the paper is meant to point out (so I hope that
someone can help me out). In response to [Jon95], I make some remarks
concerning Larch and Z [Spi89] below.
Larch
As has already been stated in the postings to
comp.specification.larch, in the logic underlying the Larch
Shared Language (let us refer to this logic as LL), all function are total,
hence [Jon95] does not directly concern LL.
``The originators of Larch [GH93] are prepared to restrict types to
having more than one value.'' [Jon95, p.66,].
It may have been the case that sorts were required to have more than one
element---this was certainly true for LP (prior to version 3.1)
``LP is designed for reasoning about models in which every sort has
at least two elements.'' [GG91, p.16,]
LP3.1 sorts are only required to be nonempty [GH93, p.131,]. If Chapter 2
of the Larch book describes LL, then it is also true that sorts (in LL) are
only required to be nonempty [GH93, p.9,].
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. 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.
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
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)}. 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.
``... 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.
Note
The following is a Z version of the first example found in [Jon95] (with the
function f renamed to h).
Zero == { i: ZZ | i = 0 }
axdef
h: ZZ -+> Zero
where
forall i: ZZ @ h i = if i = 0 then 0 else h (i - 1)
end
The type of the expression `h i' is ZZ, not Zero hence the range of h does not
contain a single element (as required for the example).
References
==========
GG91
Stephen J. Garland and John V. Guttag. A guide to LP, the Larch
Prover. Report 82, DEC Systems Research Center, Palo Alto, CA,
December 1991.
GH93
John V. Guttag and James J. Horning, editors. Larch: Languages
and Tools for Formal Specification. Texts and Monographs in
Computer Science. Springer-Verlag, 1993. With Stephen J.
Garland, Kevin D. Jones, Andrés Modet, and Jeannette M. Wing.
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.
Spi89
J.M. Spivey. The Z Notation: A Reference Manual. Computer
Science Series. Prentice Hall International, 1989.
Patrice
-------------------------------------------------------------------------------
http://www.cs.concordia.ca/~faculty/chalin
Follow-Up(s):
Reference(s):