利用者:NGiraffe/作業中の記事/関係代数

This versionis on 16 November 2009 at 07:37.

• スタブテンプレートを貼る
• 曖昧さ回避が必要か
• 投稿時の記事名を「関係代数 (数学)」とすること

数学の抽象代数学の分野において 関係代数 (relation algebra) とは逆と呼ばれる対合 を持つ residued boolean algebra のことである。動機付けとなるような関係代数の例は、集合 X 上の全ての二項関係からなる集合 Pow(X×X) であって、演算 R · S を通常の関係の合成とし、R の逆を逆関係で定義する。関係代数は 19世紀の オーガスタス・ド・モルガン と チャールズ・サンダース・パースの結果から現れ、Ernst Schroder(en)の代数的論理学において全盛となった。現在の、関係代数の等式的な形は 1940 年代よりアルフレト・タルスキと彼の弟子たちによって開発された。

In mathematics and abstract algebra, a relation algebra is a residuated Boolean algebra equipped with an involution called "converse". The motivating example of a relation algebra is the algebra 2^X2 of all binary relations on a set X, with R?S interpreted as the usual composition of binary relations and the converse of R as the inverse relation. Relation algebra emerged in the 19th century work of Augustus De Morgan and Charles Peirce, which culminated in the algebraic logic of Ernst Schroder. The present-day purely equational form or relation algebra was developed by Alfred Tarski and his students, starting in the 1940s.

定義

関係代数とは組 (L, ∧, ∨, ¬, 0, 1, · , I, ▷, ◁, ^{${\breve {\ }}$}) であって、以下の条件を満たす:

1. (L, ∧, ∨, ¬, ·, I, ▷, ◁) は residuated Boolean algebra である。
2. 単項演算子 x^{${\breve {\ }}$} は x^{${\breve {}}$}▷I = x = I◁x^{${\breve {}}$} を満たす。

x▷y は合成と逆を使って x^{${\breve {\ }}$} · y と定義可能で、双対的に x◁y を x · y^{${\breve {\ }}$} と定義できるので演算 ▷ や ◁ を関係代数の指標に含める必要はなく、通常そうされているように組 (L, ∧, ∨, ¬, 0, 1, · , I, ^{${\breve {\ }}$}) として定めることができる。一方、x^{${\breve {\ }}$} は x ▷ I または I◁x として定義でき、関係代数は residuated Boolean algebra と同じ指標を持つともいえる。この定義においては公理は (x▷I)▷I = x = I◁(I◁x) の形になる。しかし、このことは単に ▷I と I◁ が対合であると言っている。Jonsson と Tsinakis はもしどちらかが対合ならば他方も対合であるので両者は同一の操作であり、つまり逆となることを示した。このことが特に直接的な定義を導く:

関係代数とは residuated Boolean algebra (L, ∧, ∨, ¬, 0, 1, · , I, ▷, ◁) であって I◁ が対合となるものである。

x◁y を x の y による商とみなし、I を対応する乗法の単位元とみなしたとき、x^{${\breve {\ }}$} = I◁x は文法的に 1/x との類推から x の 逆数 と理解できる。

residuated Boolean algebra は有限個の等式で公理化されるので、関係代数も同様に公理化される。よってそれは関係代数の有限公理化代数多様体を形成する( RA と呼ばれる)。

A relation algebra (L, ∧, ∨, ¬, 0, 1, ?, I, ?, ?, ^{${\breve {\ }}$}) is an algebraic structure such that

(i) (L, ∧, ∨, ?, I, ▷, ◁) is [dumb] a residuated Boolean algebra, and

(ii) the unary operation x^{${\breve {\ }}$} satisfies x^{${\breve {}}$}▷I = x = I◁x^{${\breve {}}$}.

Since x?y can be defined in terms of composition and converse as x^{${\breve {\ }}$}?y, and dually x?y as x?y^{${\breve {}}$}, it is not necessary to include ? or ? in the signature, which can therefore be simplified to (L, ∧, ∨, ¬, 0, 1, ?, I, ^{${\breve {\ }}$}), the more usual form of the signature for relation algebras. On the other hand x^{${\breve {}}$} is definable as either x?I or I?x, in which case a relation algebra can have the same signature as a residuated Boolean algebra. With that definition the axioms become (x?I)?I = x = I?(I?x). But this simply asserts that ?I and I? are involutions. Jonsson and Tsinakis have shown that if either one is an involution then so is the other and they are then the same operation, namely converse. This leads to a particularly straightforward definition:

A relation algebra is a residuated Boolean algebra (L, ∧, ∨, ¬, 0, 1, ?, I, ▷, ◁) such that I◁ is an involution.

When x?y is viewed as a form of quotient of x by y, with I as the corresponding multiplicative unit, x^{${\breve {\ }}$} = I?x can be understood as the reciprocal of x by syntactic analogy with 1/x, a term some authors use synonymously with converse.

Since residuated Boolean algebras are axiomatized with finitely many equations, so are relation algebras, which therefore form a finitely axiomatized variety called RA, the variety of relation algebras.

公理

以下にあげる公理 B1-B10 は元々タルスキが 1948年に提唱したものを Givant が 2006年に修正したものである。この公理化は、関係代数が直積 L の上の指標 ⟨L,∨, · ,^-, ^{${\breve {\ }}$}, I⟩(そのアリティは ⟨2,2,1,1,0⟩ である)を持つ代数的構造であることに基づいている。

L は選言 ∨ と補元 ()^- の下でブール代数である。

B1: A ∨ B = B ∨ A

B2: A ∨ (B ∨ C) = (A ∨ B) ∨ C

B3: (A^- ∨ B)^- ∨ (A^- ∨ B^-)^- = A

ブール代数のこの種の公理化は Huntington (en) による(1933年)。

L は (·) と I に対してモノイドをなす:

B4: A · (B · C) = (A · B) · C

B5: A · I = A

逆 ()^{${\breve {\ }}$} は合成に関する対合である:

B6: A^{${\breve {\ }}{\breve {\ }}$} = A

B7: (A · B)^{${\breve {\ }}$} = B^{${\breve {\ }}$} · A^{${\breve {\ }}$}

逆と合成は選言について分配的である:

B8: (A∨B)^{${\breve {\ }}$} = A^{${\breve {\ }}$}∨B^{${\breve {\ }}$}

B9: (A∨B) · C = (A · C)∨(B · C)

B10 はド・モルガンに発見された事実 A · B ≤ C^- ⇔ A^{${\breve {\ }}$} · C ≤ B^- ⇔ C · B^{${\breve {\ }}$} ≤ A^- を等式表示したものである:

B10: (A^{${\breve {\ }}$} · (A · B)^-)∨B^- = B^-

これらの公理は ZFC 上の定理である。ブール代数に関する B1-B3 についてはこの事実は自明であり、またそれ以外のものについては 1960年に出版された Suppes の本の第三章で紹介されている。

The axioms B1-B10 below are adapted from Givant (2006: 283), and were first set out by Tarski in 1948. This axiomatization is predicated on a relation algebra being an algebraic structure over some Cartesian square L, having signature ⟨L,∨,?,^?, ^{${\breve {\ }}$}, I⟩ of type ⟨2,2,1,1,0⟩.

L is a Boolean algebra under binary disjunction, ∨, and unary complementation ()^?:

B1: A ∨ B = B ∨ A

B2: A ∨ (B ∨ C) = (A ∨ B) ∨ C

B3: (A^? ∨ B)^? ∨ (A^? ∨ B^?)^? = A

This axiomatization of Boolean algebra is due to Huntington (1933).

L is a monoid under binary composition (?) and nullary identity I:

B4: A?(B?C) = (A?B)?C

B5: A?I = A

Unary converse ()^{${\breve {\ }}$} is an involution with respect to composition:

B6: A^{${\breve {\ }}{\breve {\ }}$} = A

B7: (A?B)^{${\breve {\ }}$} = B^{${\breve {\ }}$}?A^{${\breve {\ }}$}

Converse and composition distribute over disjunction:

B8: (A∨B)^{${\breve {\ }}$} = A^{${\breve {\ }}$}∨B^{${\breve {\ }}$}

B9: (A∨B)?C = (A?C)∨(B?C)

B10 is Tarski's equational form of the fact, discovered by Augustus De Morgan, that A?B ≤ C^? $\leftrightarrow$ A^{${\breve {\ }}$}?C ≤ B^? $\leftrightarrow$ C?B^{${\breve {\ }}$} ≤ A^?.

B10: (A^{${\breve {\ }}$}?(A?B)^?)∨B^? = B^?

These axioms are ZFC theorems; for the purely Boolean B1-B3, this fact is trivial. After each of the following axioms is shown the number of the corresponding theorem in chpt. 3 of Suppes (1960), an exposition of ZFC: B4 27, B5 45, B6 14, B7 26, B8 16, B9 23.

RA を使った二項関係の性質の記述

次の表は、二項関係で通常扱われる性質のうちのどれくらいが，RA の演算を用いて簡潔な(不)等式で記述できるかを一覧にしたものである。以下不等式 A≦B は A∨B=B の略記である。

この種の記述の最も完全なリストは Carnap の本の第 C章にある(記号がここで用いているものと若干異なるので注意)。Suppes の本の第 3.2節に少数の結果が挙げられているが、それらはここで使われているものと似た記号を用いてZFC上の定理として示されている。 どちらにしてもRAの枠組みで、つまり等式としての定式化はなされていない。

R の性質	RAでの定式化:
全射的	R$^{\breve {\ }}$ ·R ≦ I
単射的 (R${\breve {\ }}$ が全射的)	R ·R$^{\breve {\ }}$ ≦ I
全単射的	R が全射かつ単射
完全	I ≦ R∨R$^{\breve {\ }}$
関数的
関数	R が完全かつ関数的
全単射	R$^{\breve {\ }}$ ·R = I and R ·R$^{\breve {\ }}$ = I. つまり R は完全、関数的、かつ単射的
反射律	I ≦ R
非反射律	R ∧ I = 0. (0 = I-)
推移律	R ·R ≦ R
擬順序	R が反射律と推移律をみたす
反対称律	R ∧ R$^{\breve {\ }}$ ≦ I
順序関係	R が反対称律をみたす擬順序
全順序関係	R は完全な順序関係
強半順序関係	R が推移律と非反射律をみたす
強全順序関係	R が完全な強半順序関係
対称律	R = R$^{\breve {\ }}$
同値関係	R が対称律をみたす擬順序：R ·R$^{\breve {\ }}$ = R
非対称律	R ≠ R$^{\breve {\ }}$
稠密	R∧0≦(R∧0) ·(R∧0)

The following table shows how many of the usual properties of binary relations can be expressed as succinct inequalities or equalities using RA operations. Below, an inequality of the form A?B is shorthand for a Boolean equation of the form A∨B = B.

The most complete set of results of this nature is chpt. C of Carnap (1958), where the notation is rather distant from those of this entry. Chpt. 3.2 of Suppes (1960) contains fewer results, but they are presented as ZFC theorems, using a notation that more resembles that of this entry. Neither Carnap nor Suppes formulate their results using the RA of this entry, or in an equational manner.

R is	If and only if:
Surjective	R$^{\breve {\ }}$?R ? I
Injective (R${\breve {\ }}$ surjective)	R?R$^{\breve {\ }}$ ? I
1-to-1	R is surjective and injective.
Total or Connected	I ? R∨R$^{\breve {\ }}$
Functional
Function	R is functional and total.
1-1 Function	R$^{\breve {\ }}$?R = I and R?R$^{\breve {\ }}$ = I. R is total, functional, and injective.
Reflexive	I ? R
Irreflexive	R ∧ I = 0. (0 = I?)
Transitive	R?R ? R
Preorder	R is reflexive and transitive.
Antisymmetric	R ∧ R$^{\breve {\ }}$ ? I
Partial order	R is an antisymmetric preorder.
Total order	R is a total partial order.
Strict partial order	R is transitive and irreflexive.
Strict total order	R is a total strict partial order.
Symmetric	R = R$^{\breve {\ }}$
Equivalence	R?R$^{\breve {\ }}$ = R. R is a symmetric preorder.
Asymmetric	R ≠ R$^{\breve {\ }}$
Dense	R∧0 ? (R∧0)?(R∧0).

表現力

RAの超数学は1987年のタルスキとGivantによる本の中で大きな分量を割いて議論されている。また Givant の論文においても簡潔に述べられている。

RA は全体的に、等式どうしの一様な置き換えと代入だけで操作される等式たちから成る。この二種類の操作規則は、学校教育でも扱われ、抽象代数でも扱われ、一般的に慣れ親しまれた操作である。よって RA の証明は一般の数理論理学における証明と異なり数学者に慣れ親しんでいる形で進められる。

RA は三つ未満の変数をもつ一階述語論理(FOL)(もしくはそれと論理的に同値なもの)を記述することができる。与えられた変数は三回を越えない範囲で繰り返し量化子を用いて量化されうる。驚くべきことに、このような FOL の一部分だけでもペアノの公理を記述することができ、現在提唱されている中で殆ど全ての公理的集合論を記述することができる。よって、 RA は全ての数学を代数化する手段の一つであり、FOL とその結合子、量化子、ターンスタイルと三段論法なしで済ますことができる。RA はペアノの算術と集合論を記述するのでゲーデルの不完全性定理が適用され、RA は不完全でありimcompletable であり決定不能である(ちなみに RA におけるブール代数は完全で決定可能)。

表現可能な関係代数(representable relation algebra)とは、ある集合上の二項関係からなる関係代数と同型で 、RA の演算を通常の二項関係間の演算として解釈できるものをいう。表現可能な関係代数からなるクラスを RRA と書くことにする。RRA は quasivariety であることが、例えば pseudoelementary class の手法を以って、簡単に示される。即ち、普遍 Horn 理論により公理化可能である。1950年に Lyndon はRA では成立しないが RRA では成立する方程式が存在することを証明した。つまり、 RRA から生成される variety は RA から生成される variety の真の subvariety になっている。1955年にタルスキは RRA それ自体が variety であることを示したが、それは 1964年に Monk が示したように有限公理化を持たない(RAは定義から有限公理化される)。この、全ての関係代数が表現可能ではないということは、つねに表現可能であるブール代数と関係代数との差異を表す基本的な手段となっている。

Expressive power

The metamathematics of RA are discussed at length in Tarski and Givant (1987), and more briefly in Givant (2006).

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 more than 3 deep.) 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, Godel's incompleteness theorems apply to it; RA is incomplete, incompletable, and undecidable. (N.B. The Boolean algebra fragment of RA is complete and decidable.)

The representable relation algebras, forming the class RRA, are those relation algebras isomorphic to some relation algebra consisting of binary relations on some set, and closed under the standard interpretations of the RA operations. It is easily shown, e.g. using the method of pseudoelementary classes, that RRA is a quasivariety, that is, axiomatizable by a universal Horn theory. In 1950, Roger Lyndon proved the existence of equations holding in RRA that did not hold in RA, that is, the variety generated by RRA is a proper subvariety of the variety RA. In 1955, Alfred Tarski showed that RRA is itself a variety, which however, as shown by Donald Monk in 1964, has no finite axiomatization, unlike RA which is finitely axiomatized by definition. That not every relation algebra is representable is a fundamental way relation algebras differ from Boolean algebras, which are always representable as sets of subsets of some set closed under union, intersection, and complement.

例

1. 任意のブール代数は、連言 ∧ で合成 · を定義すると関係代数になる。この場合逆は恒等写像(y^{${\breve {\ }}$} = y)となり、剰余 y＼x と y/x は含意 y→x となる。
2. 動機付けとなるような関係代数の例は、集合 X の上の二項関係 R を部分集合 R⊂X×X とみなせることに拠っている。X 上の全ての二項関係から成るべき集合 Pow(X×X) はブール代数をなす。よって一番目の例のようにそれだけで Pow(X×X) は関係代数であるが、標準的には、合成を x(R ·S)z = ∃y. x R y ∧y S z と定義する。この解釈で R＼S は、任意の x∈ X に対して、 x R y ならば x R z をみたす組 (y, z) からなる集合として一意に定まる。双対的に S/R は任意の z∈ X に対して y R z ならば x S z をみたす組 (x,y) からなる二項関係である。y^{${\breve {\ }}$} =￢(y＼￢I) という翻訳によって、R に対する逆 R^{${\breve {\ }}$} を、 x R y をみたす組 (y,x) からなる二項関係として定義できる。
3. 集合 X 上の同値関係 E ⊂ X×X のべき集合 Pow(E) は直前の例の重要な一般化になっている(X×X はそれ自身同値関係である)。Pow(E) は E ≠ X×X であるとき Pow(X×X) の部分代数にはならないが(Pow(X) の最大元である X×X を Pow(E) は含まない)、関係代数の各演算は同じものである。任意の関係代数はある集合のある同値関係からつくられる関係代数の部分代数であり、この例は表現可能性(前節をみよ)の観点から重要である。
4. 群の直積または直和を合成とし、逆元をとる操作を逆とし、単位元を I として、更に R が一対一対応であるとき、R^{${\breve {\ }}$} ·R = R · R^{${\breve {\ }}$} = I が成り立つ。よってこのとき L はモノイドでもあるが群にもなる。定義の B4-B7 は群論においてよく知られた定理であり、関係代数は群(とブール代数)の proper extension になる。このことは関係代数の強い表現力を示唆する事実である。

Examples

1. Any Boolean algebra can be turned into a relation algebra by interpreting conjunction as composition (the monoid multiplication  ?), i.e. x?y is defined as x∧y. This interpretation requires that converse interpret identity (? = y), and that both residuals y\x and x/y interpret the conditional y→x (i.e., ¬y∨x).

2. The motivating example of a relation algebra depends on the definition of a binary relation R on a set X as any subset R ⊆ X2. The power set 2^X2 consisting of all binary relations on X is a Boolean algebra. While 2^X2 can be made a relation algebra by taking R?S = R∧S as for the preceding example, the standard interpretation of ? is instead given by x(R?S)z = ∃y.xRySz. That is, the pair (x,z) belongs to the relation R?S just when there exists y ∈ X such that (x,y) ∈ R and (y,z) ∈ S. This interpretation uniquely determines R\S to consist of all pairs (y,z) such that for all x ∈ X, if xRy then xSz. Dually S/R consists of all pairs (x,y) such that for all z ∈ X, if yRz then xSz. The translation ? = ¬(y\¬I) then establishes the converse R^{${\breve {\ }}$} of R as consisting of all pairs (y,x) such that (x,y) ∈ R.

3. An important generalization of the previous example is the power set 2^E where E ⊆ X2 is any equivalence relation on the set X. This is a generalization because X2 is itself an equivalence relation, namely the complete relation consisting of all pairs. While 2^E is not a subalgebra of 2^X2 when E ≠ X2 (since in that case it does not contain the relation X2, the top element 1 being E instead of X2), it is nevertheless made a relation algebra using the same definitions of the operations. Its importance resides in the definition of a representable relation algebra as any relation algebra isomorphic to a subalgebra of the relation algebra 2^E for some equivalence relation E on some set. Refer to the previous section for more on the relevant metamathematics.

4. If group sum or product interprets composition, group inverse interprets converse, group identity interprets I, and if R is a one to one correspondence, so that R^{$^{\breve {\ }}$}?R = R?R^{$^{\breve {\ }}$} = I, then L is a group as well as a monoid. B4-B7 become well-known theorems of group theory, so that relation algebra becomes a proper extension of group theory as well as of Boolean algebra, a fact indicative of its great expressive power.

歴史的注意

1860年にド・モルガンは RA の基盤を与えたが、パースはそれをより発展させ、その哲学的な強力さに魅了されるようになった。彼らの結果は E. Schröder(en) が著書 Vorlesungen über die Algebra der Logik (1890-1905)の第三巻で取り上げ、拡大されて決定的な形で知られるようになった。「プリンキピア・マテマティカ」では Schröder の RA について記しているが、記法の発明者としてしか認めていない。1912年、Alwin Korselt は、量化子が四回入れ子になっている、ある論理式が RA で同値なものをもたないことを証明した(Korselt は彼の発見を出版しなかった。出版物の形で公開されたのは L. Loewenheim が 1915年に出版した論文においてである)。この事実は RA への興味を失わさせ、それはタルスキが 1941年に論文を執筆するまで続いた。彼の学生は現在まで RA の開発を続けている。タルスキは 1970年代に S. Givant の助けを借りて RA の研究に復帰し、彼らの共同研究は1987年に出版されたモノグラフにまとめられた。この本はこの分野における決定的な参考文献となっている。より詳細な RA の歴史については，Maddux の本を参照すること。

Historical remarks

DeMorgan founded RA in 1860, but C. S. 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 Schroder gave it in Vol. 3 of his Vorlesungen (1890-1905). Principia Mathematica drew strongly on Schroder's RA, but acknowledged him only as the inventor of the notation. In 1912, Alwin Korselt proved that a particular formula in which the quantifiers were nested 4 deep had no RA equivalent. This fact led to a loss of interest in RA until Tarski (1941) began writing about it. His students have continued to develop RA down to the present day. Tarski returned to RA in the 1970s with the help of Steven Givant; this collaboration resulted in the monograph Tarski and Givant (1987), the definitive reference for this subject. For more on the history of RA, see Maddux (1991, 2006).

Software

• RelMICS / Relational Methods in Computer Science maintained by Wolfram Kahl
• Carsten Sinz: ARA / An Automatic Theorem Prover for Relation Algebras

See also

• Algebraic logic
• Allegory (category theory)
• Binary relation
• Cartesian product
• Cartesian square
• Composition of relations
• Converse of a relation

• Cylindric algebras
• Extension in logic
• Involution
• Logic of relatives
• Relation
• Relation construction
• Relation reduction

• Relational calculus
• Relational algebra
• Relative product of relations
• Residuated Boolean algebra
• Spatial-temporal reasoning
• Theory of relations
• Triadic relation

References

• Rudolf Carnap (1958) Introdution to Symbolic Logic and its Applications. Dover Publications.

• Halmos, P. R., 1960. Naive Set Theory. Van Nostrand.
• Leon Henkin, Alfred Tarski, and Monk, J. D., 1971. Cylindric Algebras, Part 1, and 1985, Part 2. North Holland.
• Hirsch R., and Hodkinson, I., 2002, Relation Algebra by Games, vol. 147 in Studies in Logic and the Foundations of Mathematics. Elsevier Science.
• Bjarni Jonsson and Constantine Tsinakis, 1993, "Relation algebras as residuated Boolean algebras," Algebra Universalis 30: 469-78.
• Roger Maddux, 1991, "The Origin of Relation Algebras in the Development and Axiomatization of the Calculus of Relations," Studia Logica 50(3/4): 421-55.
• --------, 2006. Relation Algebras, vol. 150 in Studies in Logic and the Foundations of Mathematics. Elsevier Science.
• Patrick Suppes, 1960. Axiomatic Set Theory. Van Nostrand. Dover reprint, 1972. Chpt. 3.
• 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.

External links

• Yohji AKAMA, Yasuo Kawahara, and Hitoshi Furusawa, "Constructing Allegory from Relation Algebra and Representation Theorems."
• Richard Bird, Oege de Moor, Paul Hoogendijk, "Generic Programming with Relations and Functors."
• R.P. de Freitas and Viana, "A Completeness Result for Relation Algebra with Binders."
• Peter Jipsen:
  • Relation algebras. In Mathematical structures. If there are problems with LaTeX, see an old HTML versionhere.
  • "Foundations of Relations and Kleene Algebra."
  • "Computer Aided Investigations of Relation Algebras."
  • "A Gentzen System And Decidability For Residuated Lattices."
• Vaughan Pratt:
  • "Origins of the Calculus of Binary Relations." A historical treatment.
  • "The Second Calculus of Binary Relations."
• Priss, Uta, "An FCA interpretation of Relation Algebra."
• Kahl, Wolfram, and Schmidt, Gunther, "Exploring (Finite) Relation Algebras Using Tools Written in Haskell." See homepage of the whole project.