[Prev][Next][Index]

Re: Partial Functions and Logics

In article <41coud$r71@hitchcock.dfki.uni-sb.de> hubert@mpi-sb.mpg.de
(Hubert Baumeister) writes:

   As I understand [Sp88] (pp.  69,70-71,91) the equality in Z is to be
   interpreted as strict equality.  Two terms are strictly equal in an
   interpretation iff they are _both_ defined and evalutate to the same
   value.  Thus an equation of the form g(0) = 0 implies that in any
   interpretation satisfying this equation g(0) (and 0) have to be
   defined.  Therefore g has to include at least the pair (0,0). 

As _I_ understand my intentions, I wanted to say (as I _do_ say in the
later reference manual) that E1 = E2 is true if they are defined and
equal, false if they are defined and unequal AND I REFUSE TO SAY
WHETHER IT IS TRUE OR FALSE if one or both is undefined.  The idea is
that we should use rules for reasoning about a specification that are
valid whatever choice is made about undefined expressions.

Let's not talk about the formula on p.71, which gives existential
equality (although I don't think existential equality is such a bad
thing).  What I really wanted to say at the time is explained on p.93,
where an incompletely-specfied function 'equality' is used to give the
meaning of equations.

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