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


       u: Unit
       Unit = {u}

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

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.


   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, 

       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)

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


   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. 

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

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