[Prev][Next][Index]
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
Reference(s):