Re: Partial Functions and Logics

In article <CLIFF.95Aug28161133@rdf042.cs.man.ac.uk>
cliff@cs.man.ac.uk (Cliff B Jones) writes:

   [About the example from his 'warning note':]

   Of course, in this example it is easy to see what is going on - but in
   more subtle cases I think that the least fixed point interpretation of
   functions is very intuitive and doing anything that moves away from it
   should be done with great caution.

   The point of my original note (see the "equations" about fact(orial))
   was this worry about the meaning of functions. Saying that all terms
   denote, pushes through recursive definitions to give some odd results.

I'm glad Cliff said that, because it reveals an unstated difference of
understanding.  Cliff wants to think about functions intentionally, to
define them by writing recursive definitions.  And that's very
intuitive for a programmer.  In Z we are victims of the set theorists,
and cannot see functions other than extensionally.  It's just about
possible to make a definition in Z that says f is the lfp of (say)
McCarthy's definition of the 91 function, but it's long-winded enough
that nobody could really work like that.

   [... about the style of writing "x in dom f /\ f(x) = y" ...]

   Where do these ``customary Z stylistic guidelines'' fit into a formal
   semantics of a specification language?

They just stop us from writing nonsense, either the kind of nonsense
from which you can prove nothing, or the kind of nonsense from which
you can prove anything you like.

I meant to say before, so I'll say it now, that it's long overdue for
someone to work out precisely what the implications of the Z approach
(or another one like it) would be for a system of inference rules.
John Rushby raised the question in this newsgroup some time ago, and
it's not one that can go unanswered for much longer.

-- Mike