Critical pair
From Wikipedia, the free encyclopedia
Contents |
[edit] Usage in mathematical logic
A critical pair arises in term rewriting systems where rewrite rules overlap to yield two different terms.
For example, in the term rewriting system with rules
- ,
consider the term f(g(x,x), x). Applying ρ1 yields the term g(x,x), while applying ρ2 yields the term f(x,x). The critical pair is then (g(x,x), f(x,x)).
When one side of the critical pair reduces to the other, we say that the critical pair is convergent. Where one side of the critical pair is identical to the other, we say that the critical pair is trivial.
Note that if the term rewriting system is not confluent, the critical pair may not converge, so critical pairs are potential sources where confluence will fail. In fact, we have the critical pair lemma, which states that a term rewriting system is weakly confluent if all critical pairs are convergent. Weak confluence implies convergent critical pairs clearly as if any critical pair, say (a, b) arises, then a and b have common reduct and thus the critical pair is convergent.
[edit] Usage in order theory
A critical pair in a partially ordered set P = (X, ≤) is, loosely speaking, a pair of elements that are very nearly, but not quite, comparable. Formally, it is an ordered pair (x, y) of elements of X that are incomparable in P and such that for all z in X, if z < x then z < y and if y < z then x < z. Among the reasons that critical pairs are of interest is the fact that a family F of linear extensions of any poset P is a realizer of P if and only if for every critical pair (u, v) of P there is some linear extension L in F for which u <L v.
[edit] External links
[edit] References
- W.T. Trotter, Combinatorics and partially ordered sets: Dimension theory, Johns Hopkins Series in Mathematical Sciences, Johns Hopkins Univ. Press, Baltimore, 1992.