Re: Partial Functions and Logics (2)

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

I don't think so. To the contrary, in my opinion it directly concerns LL.
Jones is talking about an interpretation of partial functions as total
functions where the value of that function when applied to some arguments is
of no interest (eg. the arguments are not in the domain of f seen as a
partial function).

A typical example are stacks.  What should be the top of the empty stack? In
a setting where partial functions are available, top(empty) is undefined.
However, in Larch (LSL) specifications where all functions are total,
top(empty) has to have a value. The usual solution is to not fix this value
in the specification and thus to allow different models of the specification
assigning different values to top(empty). This is exactly the method Jones

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

Just to support this, it is trival to prove from the following LSL
specification using the Larch Prover that forall i : Int (f(i) = unit). 

Unit : trait
   includes Integer
      unit : -> U
      f : Int -> U
      forall u : U
         u == unit        % U contains exactly one element
      forall i : Int
         f(i) == if i = 0 then unit else f(i-1)

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


                 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/