Kleene equality

Equality operator on partial functions

In mathematics, Kleene equality,[1] or strong equality, ( ≃ {\displaystyle \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 {\displaystyle f} and  g {\displaystyle g} ,  f ≃ g {\displaystyle f\simeq g} means that for every  x {\displaystyle x} :[2]

* f ( x ) {\displaystyle f(x)} and  g ( x ) {\displaystyle g(x)} are both defined and  f ( x ) = g ( x ) {\displaystyle f(x)=g(x)}
* or  f ( x ) {\displaystyle f(x)} and  g ( x ) {\displaystyle g(x)} are both undefined.

Some authors[3] are using "quasi-equality", which is defined like this:  ( y 1 ∼ y 2 ) :⇔ ( ( y 1 ↓ ∨ y 2 ↓ ) ⟶ y 1 = y 2 ) , {\displaystyle (y_{1}\sim y_{2}):\Leftrightarrow ((y_{1}\downarrow \lor y_{2}\downarrow )\longrightarrow y_{1}=y_{2}),} 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 ≃ g ) :⇔ ( ∀ x . ( f ( x ) ∼ g ( x ) ) ) . {\displaystyle (f\simeq g):\Leftrightarrow (\forall x.(f(x)\sim g(x))).}

## References

[edit]

1. ^ "Kleene equality in nLab". ncatlab.org.
2. ^ Cutland 1980, p. 3.
3. ^ Farmer, William M.; Guttman, Joshua D. (2000). "A Set Theory with Support for Partial Functions". Studia Logica. 66 (1): 59–78\. JSTOR 20016214.

* Cutland, Nigel (1980). Computability, an introduction to recursive function theory. Cambridge University Press. p. 251\. ISBN 978-0-521-29465-2.

This mathematics-related article is a stub. You can help Wikipedia by expanding it.

|

* v
* t
* e

*[v]: View this template
*[t]: Discuss this template
*[e]: Edit this template