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. 


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,]. 


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


    u: Unit
    Unit = {u}

    f: ZZ -+> Unit
    f i = if i = 0 then u else f (i - 1)

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, 

    g: ZZ -+> ZZ
    g 0 = 0

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. 

    f: ZZ -+> Unit
    dom f = {- 1, 0, 1}
    f i = if i = 0 then u else f (i - 1)

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
  if i = 0 then F := 0
           else F := F(i-1)

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. 


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 }

    h: ZZ -+> Zero
    forall i: ZZ @ h i = if i = 0 then 0 else h (i - 1)

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


   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. 

   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. 

   C.B. Jones. Partial functions and logics: A warning. Information
   Processing Letters, 54(2):65--67, 1995. 

   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. 

   J.M. Spivey. The Z Notation: A Reference Manual. Computer
   Science Series. Prentice Hall International, 1989. 



Follow-Up(s): Reference(s):