Relation algebra
From Wikipedia, the free encyclopedia
In mathematics, relation algebra (RA) is an algebraic structure, a proper extension of the two-element Boolean algebra 2 intended to capture the mathematical properties of binary relations. RA consists of two binary operations, juxtaposition and relative product, two unary operations, complementation and converse, and the constant 1. Given any set, RA stands to its Cartesian square as Boolean algebra stands to its power set.
Relational algebra is a distinct concept mainly of interest to computer science.
Contents |
[edit] Definition
For an introduction to RA, see Maddux (2006). Other treatments include Henkin, Tarski and Monk (1971 & 1985), Tarski and Givant (1987), and Hirsch and Hodkinson (2002).
In what follows, Greek letters are part of the metalanguage and denote syntactical variables ranging over formulae. Upper case Latin letters from the start of the alphabet denote sets. Lower case Latin letters from the end of the alphabet range over the members of the universal set A. A may, of course, be coextensive with the universe in first-order logic.
The ordered pair (x, y) has first element x and second element y. Let B be the Cartesian square of A, namely the set of all possible ordered pairs constructible from the members of A, i.e., B = A × A. R and S denote arbitrary binary relations, and E denotes the set membership relation, namely if x∈B, then (x,B)∈E. Just as Boolean algebra is the algebra of the power set of any set, RA is the algebra of the Cartesian square of that set. Because all members of B are ordered pairs, the scope of RA is limited to binary relations but this is not a serious limitation, simply because a single binary relation E suffices for set theory, whose enormous expressive power is beyond question.
Syntax: The notation described here for the binary and unary operations of RA is not the conventional one. The syntax of 2 is:
- () and single Latin letters are atoms;
- If φ and δ are formulae, so are (φ) and φδ. The latter binary operation is called juxtaposition.
() is often written as 1, and (()) as 0.
To this Boolean syntax, we add syntax peculiar to RA:
- 1 is an atom;
- If φ, δ, and γ are formulae, so are 〈φ〉, [φδ], [φ.δγ], and [φδ.γ].
This syntax shares with Polish notation the advantage of not requiring any bracketing to establish the order of operands. In the terminology of universal algebra, RA is a <B,--,[--],(-),〈-〉,1> algebra of type <2,2,1,1,0>, with B being any set that is the Cartesian square of another set.
Boolean Semantics: The intended interpretation of (-) is Boolean complementation; that of juxtaposition is one of Boolean meet or join. If φδ denotes the meet of φ and δ, ((φ)(δ)) denotes their join, and vice versa. Complementation with nothing in its scope denotes one of the two lattice bounds Boolean algebra requires. On the Boolean syntax and semantics employed here, see laws of form.
RA Semantics: 1 denotes the identity relation, consisting of all ordered pairs whose left and right members are identical. 0=(1) denotes the diversity relation, namely all ordered pairs whose left and right members are not identical. If (x,y)∈R, then (y,x)∈〈R〉. If, additionally, (y,z)∈S, then (x,z)∈[RS]. Hence the intended interpretations of 〈-〉 and [--] are converse and relative product, for which the customary notations are and R|S, respectively. The period serves to eliminate ambiguities that would otherwise arise when juxtaposition and relative product interact, as in RA6 below. The notation [φγ.δ] denotes the relative product of δ with the juxtaposition of φ and γ.
[edit] Axioms
The axioms RA1-RA7 are those of Tarski and Givant (1987: 235), translated into the notation set out above. BA1-BA3 are a basis for 2 set out in two-element Boolean algebra.
Label | Axiom | Remarks | |
---|---|---|---|
Axioms for the Boolean algebra 2 | |||
BA1 | φδγ=δγφ | Juxtaposition commutes, associates. | |
BA2 | (φ)φ=() | 2 is a bounded lattice. | |
BA3 | φ(φδ) = φ(δ) | ||
Axioms Peculiar to RA. | Converse : | ||
RA1 | 〈〈φ〉〉=φ | * Involution. ((φ)) = φ is a theorem of 2. | |
RA2 | 〈φδ〉=〈φ〉〈δ〉 | * Preserves juxtaposition. Contrast with RA5 below. | |
Relative Product : | |||
RA3 | [[φδ]γ]=[φ[δγ]] | * Associates. | |
RA4 | [φ1]=[1φ]=φ | * Has 1 as identity element. | |
RA5 | 〈[φδ]〉=[〈δ〉〈φ〉] | * Is preserved by converse, except transposed. Contrast with RA2. | |
RA6 | [φγ.δ]=[φδ][γδ] | * Distributes over juxtaposition. | |
RA7 | [〈φ〉([φδ])]〈δ〉=〈δ〉 | * Is residuated. |
BA1-BA3 define a Boolean lattice; ()=(1)1, an instance of BA2, and (()) are the associated lattice bounds. BA1-BA3 may be replaced by any set of axioms for Boolean algebra. By 〈x〉≤x and 〈()〉=(), both easy theorems, and by RA1 and RA2, converse is an interior operator. It then follows that 〈B,--,(-),〈-〉,()〉 is an interior algebra.
That juxtaposition commutes and associates are easy consequences of BA1 and the theorem φφ=φ. Relative product likewise associates (RA1), but commutes if (RA4) and only if one of the operands is 1. Hence '[' and ']' can bracket any number of operands, as long as it is understood that the order of operands (except, trivially, 1) cannot be altered. Note that φ and δ in RA2 may be freely interchanged on either side of '=', while the order of φ and δ in RA5 cannot be altered in this way.
RA is a semiring:
- (())φ=φ is a theorem of 2. Hence juxtaposition and (()) form a commutative monoid;
- By RA3 and RA4, <B,[--],1> is a monoid, just as the set of all functions is a monoid under function composition and the identity function. This is consistent with the fact that the relative product of two functions is the same as their composition;
- By RA6, relative product distributes over juxtaposition. Moreover, δ.φγ]=[δφ][δγ] is an RA theorem (Tarski and Givant 1987: 49 v);
- [(())φ]=[φ(())]=(()) is an RA theorem (xiii).
By virtue of RA7:
- RA is a residuated lattice, except that the usual definition of such lattices posits two binary operations in addition to meet and join, rather than one binary and one unary, as here;
- Relative product interacts with the other 3 operations via the cyclic law: [φγ]δ = [〈φ〉δ]γ = [δ〈γ〉]φ. Contrast with the Jacobi identity.
The unary operation 〈-〉 can be defined in terms of 1 and [--], as follows. Redefine [φδ] so as to have the same meaning as one of [φ〈δ〉] or [δ〈φ〉]. Hence [1δ] ⇔ 〈δ〉 and [φ[[1δ]] ⇔ [φδ].
Recall that E is the set membership relation, so that E∈R. If at least one of the following two axioms applies to E:
- Given any set C, the unit set {C} exists;
- Given any two sets, their union and Cartesian product exist,
then 1 and () can be defined in terms of E, [--], and (-) as follows: 1=([E(E)]) and ()=(E)E, the latter being a consequence of BA2. On these and other reductions in the primitives of RA, see Tarski and Givant (1987: §§5.2-3).
[edit] Expressive power
The metamathematics of RA are discussed at length in Tarski and Givant (1987). RA consists entirely of equations manipulated using nothing more than uniform replacement and the substitution of equals for equals. Both rules are wholly familiar from school mathematics and from abstract algebra generally. Hence RA proofs are carried out in a manner familiar to all mathematicians, unlike the case in mathematical logic generally.
RA can express any (and up to logical equivalence, exactly the) first-order logic (FOL) formulas containing no more than three variables (a given variable can be quantified multiple times as long as the quantifiers do not nest). Surprisingly, this fragment of FOL suffices to express Peano arithmetic and almost all axiomatic set theories ever proposed. Hence RA is, in effect, a way of algebraizing nearly all mathematics, while dispensing with FOL and its connectives, quantifiers, turnstiles, and modus ponens. Because RA can express Peano arithmetic and set theory, the classic theorems of Gödel apply to it; RA is incomplete, incompletable, and undecidable. (N.B. None of these properties describe the Boolean algebra fragment of RA.)
In 1950, Roger Lyndon proved that there are statements true in every RA that cannot be proved from the above axioms. In 1964, Donald Monk further proved that there cannot exist a finite set of axioms from which all true equations of RA can be derived. Finally, RA is a variety.
[edit] Other notations
In the literature, many notation variant exists for each operation. Thus, many combinations exist for the basic symbols of the language of relation algebra. Another example:
- Bool-algebraic operations
- , , , 0, 1
- Monoid operations
- Δ, ;
- Converse of ρ
As seen, a semicolon is often used to help the reader (because of the possible confusion caused by the non-fixed reading direction of the sign). The other monoid operation is often described using words which emphasise its “diagonal” nature. Let us select Δ sign here to denote it, in the literature it can be seen sometimes [1], although more often sign is used.
Sometimes also an assertive symbol is used (besides the operators). can be said iff for each x, y standing in ρ relation, this fact implies that x, y stands also in σ relation. Thus, can be interpreted as if we interpret the relations with their (set-theoretical) graphs. can be defined in terms of =
and vice versa:
Sign for deducibility [2] is part of the metalanguage.
For illustration, let us show the axioms [3] [4] again with this notation (ρ, σ, τ are meant universally quantified):
- Boolean algebra axioms for 0, , 1, ,
- Monoid axioms for Δ, ;:
- Δ is the identity element:
- Δ;ρ = ρ
- ρ;Δ = ρ
- Associativity:
- Δ is the identity element:
- Involution:
- Antihomomorphism:
- Homomorphism, join-preserving
- Residuated:
[edit] Examples
As mentioned, relation algebra is a surpirisingly powerful tool for reasonng about relations or formalising concepts and theorems in the theory of relations. Let us see some examples.
Let us formalize concepts for relations which we know when speaking about functions:
Other well-known properties when speaking about equivalence relations and partial orders:
- ρ is reflexive iff
- ρ is symmetric iff
- ρ is antisymmetric iff
- ρ is transitive iff
Now we can reason about equivalence relations and partial orders. If treating partial orders, we can get further and formalise more notions of order theory. Let denote a partially ordered set. The relation π (besides being partial order), can have more special properties, let us formalise some:
- π works in a directed set iff
[edit] Software
- RelMICS / Relational Methods in Computer Science maintained by Wolfram Kahl
- Carsten Sinz: ARA / An Automatic Theorem Prover for Relation Algebras
[edit] Historical Remarks
DeMorgan founded RA in 1860, but Charles Peirce took it much further and became fascinated with its philosophical power. The work of DeMorgan and Peirce came to be known mainly in the extended and definitive form Ernst Schröder gave it in his Vorlesungen (1890-1905). Principia Mathematica drew strongly on Schröder's RA, but acknowledged him only as the inventor of the notation. The foundational paper for RA as presented here is Tarski (1941); he devised the above axioms, and he and his students have continued to write on RA down to the present day. Much of the content of Tarski and Givant (1987) was worked out by Tarski alone in the 1940s, who returned to the subject in the 1970s with the help of Steven Givant. For more on the history of RA, see Maddux (2006).
The computer science formalism relational algebra was pioneered around 1970 by Edgar F. Codd. His name appears nowhere in Tarski and Givant (1987).
[edit] See also
[edit] References
- Carnap, Rudolf, 1958. Introduction to Symbolic Logic with Applications, Dover.
- Halmos, P. R., 1960. Naive Set Theory. Van Nostrand.
- Lucas, John Randolph, 1999. Conceptual Roots of Mathematics. Routledge.
- Roger Maddux, 2006. Relation Algebras, vol. 150 in Studies in Logic and the Foundations of Mathematics. Elsevier Science.
- Leon Henkin, Alfred Tarski, and Monk, J. D., Cylindric Algebras Part 1 (1971) and Part 2 (1985). North Holland.
- Hirsch R., and Hodkinson, I., 2002 "Relation Algebra by Games," v. 147 in Studies in Logic and the Foundations of Mathematics. Elsevier Science.
- Alfred Tarski,1941, "On the calculus of relations," Journal of Symbolic Logic 6: 73-89.
- ------, and Givant, Steven, 1987. A Formalization of Set Theory without Variables. Providence RI: American Mathematical Society.
[edit] External links
- Relation algebras. In Mathematical structures by Peter Jipsen. If there are problems with LaTeX, see an old HTML version here.
- An FCA interpretation of Relation Algebra by Uta Priss
- Origins of the Calculus of Binary Relations by Vaughan Pratt — a historical treatment
- The Second Calculus of Binary Relations by Vaughan Pratt
- A Completeness Result for Relation Algebra with Binders by R.P. de Freitas
- Exploring (Finite) Relation Algebras Using Tools Written in Haskell written by Wolfram Kahl and Gunther Schmidt (see homepage of the whole project RATH - Relation Algebra Tools in Haskell)
- Foundations of Relations and Kleene Algebra by Peter Jipsen
- Peter Jipsen: Computer Aided Investigations of Relation Algebras
- A Gentzen System And Decidability For Residuated Lattices by Peter Jipsen
[edit] Notes
- ^ A.A. Kirilov and A.D> Gvisiani: Feladatok a funkcionális analízis köréből. Tankönyvkiadó, Budapest, 1988. (Written in Hungarian,translated from Russian original. The title means: Theorems and exercises in functional analysis.)
- ^ a b Carsten Sinz: ARA / An Automatic Theorem Prover for Relation Algebras
- ^ Uta Priss: An FCA interpretation of Relation Algebra. School of Computing, Napier University, Edinburgh
- ^ Relation algebras. In Jipsen: Mathematical structures
- ^ a b c R.P. de Freitas: A Completeness Result for Relation Algebra with Binders