nLab
Kleene equality

In the setting of partial functions and operations, saying that an equality between terms such as

s=t s = t

is a Kleene equality means that it asserts that if either side of the equality is defined, then so is the other, and they are equal. Sometimes another symbol is used for Kleene equality, such as

st. s \simeq t .

Elementary examples

For example, in elementary algebra (or more generally, the first-order theory of a field),

(1)xx 2=1x \frac x {x^2} = \frac 1 x

is always true as Kleene equality, even when x=0x = 0, because then both sides are undefined. In contrast,

(2)x 2x=x \frac {x^2} x = x

is not always true, even though the two sides are equal whenever both are defined, because the right-hand side is defined when x=0x = 0 but the left-hand side is not.

The example (2) can be fixed in either of two ways. First, we can make its statement contingent on some condition under which the equality holds, as follows:

(3)x 2x=x, if x0. \frac {x^2} x = x, \text{ if } x \ne 0 .

This states that (2) holds whenever x0x \ne 0, which is correct. Alternatively, we can add a clause to the term on the right-hand side that forces it to be undefined when x=0x = 0, as follows:

(4)x 2x=(x,x0). \frac {x^2} x = (x, x \ne 0) .

The idea here is that x,x0x, x \ne 0 is a term (like a piecewise-defined? expression with only one piece) that is defined only when x0x \ne 0. Note that (4) is a stronger statement than (3); while (3) states only that (2) holds when x0x \ne 0, (4) states additionally that the left-hand side of (2) is defined only when x0x \ne 0.

The version usually seen in elementary algebra textbooks,

(5)x 2x=x,x0, \frac {x^2} x = x,\; x \ne 0 ,

is ambiguous and could mean either (3) or (4). In any case, there is no need to add anything to (1) if one adopts Kleene equality; in practice, some textbooks do and some don't.

Models

In general, if Γ\Gamma is a context and AA is a type, then the set of terms of type AA with free variables given by Γ\Gamma can be thought of as something like the set of sections of a product projection Γ×AΓ\Gamma \times A \to \Gamma. Aside from the fact that we only get definable operations this way, we also get a finer notion of equality, as several distinct terms may denote equal operations. However, that is where the proposition ‘s=ts = t’ comes in; it states that the terms ss and tt denote equal operations.

If we now allow for terms for undefined expressions, then we get sections of the projection Γ×A Γ\Gamma \times A_\bot \to \Gamma (where X X_\bot is the set of subsingletons of XX). Then Kleene equality denotes equality of these operations.

If we instead use the partial order of inclusion of subsingletons, then we have directed equality? (which is not symmetric).

Revised on June 7, 2010 04:39:30 by Toby Bartels (75.88.89.146)