Kleene equality explained

In mathematics, Kleene equality,[1] or strong equality, (

\simeq

) is an equality operator on partial functions, that states that on a given argument either both functions are undefined, or both are defined and their values on that arguments are equal.

For example, if we have partial functions

f

and

g

,

f\simeqg

means that for every

x

:

f(x)

and

g(x)

are both defined and

f(x)=g(x)

f(x)

and

g(x)

are both undefined.

Some authors[2] are using "quasi-equality", which is defined like this:

(y1\simy2):\Leftrightarrow((y1\downarrow\lory2\downarrow)\longrightarrowy1=y2),

where the down arrow means that the term on the left side of it is defined.Then it becomes possible to define the strong equality in the following way:

(f\simeqg):\Leftrightarrow(\forallx.(f(x)\simg(x))).

References

  1. Web site: Kleene equality in nLab. ncatlab.org.
  2. A Set Theory with Support for Partial Functions. Farmer, William M.. Guttman, Joshua D. . Studia Logica: An International Journal for Symbolic Logic. 66. 1. 2000. 59–78.