[Prev][Next][Index]
Re: Partial Functions and Logics
>>>>> "Mike" == Mike Spivey <mike@comlab.ox.ac.uk> writes:
In article <1995Aug29.140459.17052@zermelo.comlab.ox.ac.uk> mike@comlab.ox.ac.uk (Mike Spivey) writes:
Mike> ...
Mike> As _I_ understand my intentions, I wanted to say (as I _do_
Mike> say in the later reference manual) that E1 = E2 is true if
Mike> they are defined and equal, false if they are defined and
Mike> unequal AND I REFUSE TO SAY WHETHER IT IS TRUE OR FALSE if
Mike> one or both is undefined. The idea is that we should use
Mike> rules for reasoning about a specification that are valid
Mike> whatever choice is made about undefined expressions.
Mike> Let's not talk about the formula on p.71, which gives
Mike> existential equality (although I don't think existential
Mike> equality is such a bad thing). What I really wanted to say
Mike> at the time is explained on p.93, where an
Mike> incompletely-specfied function 'equality' is used to give
Mike> the meaning of equations.
I had not realized this and have spent some time trying to see the
consequences. As Mike, I am fairly comfortable with existential
equality but am less sure about an equality which could have such a
range of interpretations. For example, if the "weak" (or
"computational") equality (i.e. the one that programs are stuck with)
is a possible interpretation, then the undefined *does* propogate to
the logical operator!
Has any one else any reaction?
cliff
Reference(s):