Re: Partial Functions and Logics
In article <email@example.com> firstname.lastname@example.org
(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.