In mathematics, Kleene equality, 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} :
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 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
Cutland, Nigel (1980). Computability, an introduction to recursive function theory. Cambridge University Press. p. 251. ISBN 978-0-521-29465-2.