Abstract
This chapter serves the rest of the book: all later chapters presuppose it. It introduces the calculus of binary relations, and relates it to basic concepts and results from lattice theory, universal algebra, category theory and logic. It also fixes the notation and terminology to be used in the rest of the book. Our aim here is to write in a way accessible to readers who desire a gentle introduction to the subject of relational methods. Other readers may prefer to go on to further chapters, only referring back to Chapt. 1 as needed.
Chris Brink gratefully acknowledges the longstanding financial support of the South African Foundation for Research Development.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Notes
Chris Brink gratefully acknowledges the longstanding financial support of the South African Foundation for Research Development.
The symbol ≜ signifies that the equalities hold by definition.
Since the axioms for lattices, distributivity and complementation are equational.
The constant I does so vacuously, since it has no arguments.
In categorical terms f is the left adjoint (of g), and g is the right adjoint (of f). To avoid confusion with left and right residuals of relations, we refrain from this terminology.
Note that in general (F, ⊑) is not a sublattice of (X, ⊑).
Note that if I = θ then ∏i∈θ Bi one-element algebra, hence one-element algebras are not subdirectly irreducible.
In fact it is an algebraic lattice since every congruence is the join of the compact (= finitely generated) congruences that it contains.
The distinction between set and class is not relevant here, so readers unfamiliar with classes may just think of them as sets.
Recall that we have used the small circle rather than the semicolon to indicate functional composition; we do the same for morphisms. It is useful to keep in mind that by convention this inverts the order: g o f = f;g.
⊨ is called the satisfaction symbol and denotes semantical truth.
This traditional terminology is motivated by philosophy; in particular by the Leibnizian idea that “necessarily true” means “true in all possible worlds”.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer-Verlag Wien
About this chapter
Cite this chapter
Jipsen, P., Brink, C., Schmidt, G. (1997). Background Material. In: Brink, C., Kahl, W., Schmidt, G. (eds) Relational Methods in Computer Science. Advances in Computing Sciences. Springer, Vienna. https://doi.org/10.1007/978-3-7091-6510-2_1
Download citation
DOI: https://doi.org/10.1007/978-3-7091-6510-2_1
Publisher Name: Springer, Vienna
Print ISBN: 978-3-211-82971-4
Online ISBN: 978-3-7091-6510-2
eBook Packages: Springer Book Archive