[Prev][Next][Index]

Re: Partial Functions and Logics



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


    Hubert> In article <4109ub$kja@newsflash.concordia.ca>,
    Hubert> chalin@cs.concordia.ca (CHALIN patrice) writes:

    Hubert> As I understand [Sp88] (pp.  69,70-71,91) the equality in
    Hubert> Z is to be interpreted as strict equality.  Two terms are
    Hubert> strictly equal in an interpretation iff they are _both_
    Hubert> defined and evalutate to the same value.  Thus an equation

I believe that this is often called "existential equality" (and
suspect that Schoet used this phrase) this is apposite because it
gives true only if both terms "exist". "Strong equality" can then be
used for one that gives false if one term is defined and the other is
not.

But the terminology is not the main point.

I have said before that I think the use of "existential equality" fits
well with other decisions in Z. But there is a disadvantage and that
is that the user has also to think about "weak equality" (or
"computational equality" if you prefer: in -for example- a recursive
function definition, the equality between terms (if i=j then ...) has
to be one that can be evaluated by a normal computation.

cliff jones

Reference(s):