For any adjunction F\dashv U, it is an easy corollary of Lemma 3.6.2 that the composite M = UoF is idempotent, and in this section we concentrate on its fixed points. In the common situation where the ambient poset S is a powerset P(X), the fixed points of M are often called closed subsets of X. They feature in analysis as those subsets which contain the limits of their convergent sequences. Maurice Fréchet's approach to general topology (1906) was to consider the operations which take an arbitrary subset X to the smallest closed set containing it (often written [`(X)], but called MX here), and to the largest open set inside it (its interior).
DEFINITION 3.7.1 A monotone endofunction M:S® S of a poset such that \idS £ M = MoM is called a closure operation.
LEMMA 3.7.2 For any adjunction, U is injective iff F is surjective iff Fo U = \idA . Every closure operation M arises as UoF like this, where
omitted diagram environment
split the idempotent M (Definition 1.3.12); F takes an element X to the least A which is a fixed point of M above X (Remark 3.6.3). []
PROPOSITION 3.7.3 Let A Ì S be the image of a closure operation, so meets in A agree with those in S by Proposition 3.6.8. To calculate joins in A, we first find them in S and then apply the closure operation. A is already closed under any joins the closure operation preserves. []
In particular, topological closures preserve finite joins, and the finitary closure operations which arise in algebra are Scott-continuous.
Closure conditions Behind this static definition lies a dynamic point of view, which leads us into a notion of induction. Unfortunately the established terms ``operation'' and ``condition'' convey exactly the wrong idea. This kind of induction is actually more general than that treated in Section 2.5, as it allows for the non-deterministic recursive paradigm which lies behind resolution with backtracking in logic programming.
Given any subset X of some space, let TX be the set of limits t (in the sense of analysis) of sequences (\termui) Ì X. Now TX need not be closed, so we form the set T2X of limits of sequences (\termui) Ì TX , and so on, but, unlike Proposition 3.3.11, even ÈnTnX need not be closed. Nevertheless, MX exists by the Adjoint Function Theorem 3.6.9.
DEFINITION 3.7.4 A system of closure conditions on a set S is given by any relation \triangleright :P(S)\leftharpoondown\rightharpoonup S, without restriction. Then a subset A Ì S is said to be \triangleright -closed if
|
Let A º Mod(L) be the set of \triangleright-closed subsets, ordered by inclusion, and U:Mod(L)\hookrightarrow P(S). Since this is closed under intersections , the Adjoint Function Theorem 3.6.9 gives F\dashv U, and we call F(X) the closure of X Ì S. (We shall write FX Î A for the closure considered as a model or closed subset, and MX Î S for its underlying set.)
The left hand side of K\triangleright t is called the arity of this instance of the closure condition: the choice of letter reflects our use of k for the arity of operation-symbols. If this is always a finite set, we sometimes write it as a list, and say that \triangleright is finitary.
EXAMPLES 3.7.5 There are many familiar binary closure conditions.
|
|
REMARK 3.7.6 A nullary closure condition Æ\triangleright t says that t must be in every closed set. If \triangleright consists only of such conditions, for t Î G, then F(X) = GÈX and A is the upper set G¯ S (Example 3.1.6(f)).
For any system of closure conditions, in order to find the closure F(G) of a set G (of generators), we may instead consider the extended system \triangleright ¢, with an extra nullary closure condition Æ\triangleright ¢x for each x Î G. We write \triangleright +G for \triangleright ¢. Without loss of generality we therefore need only consider F(Æ), which is the smallest \triangleright -closed set, so long as we study closure conditions in general, for example in Corollary 3.9.2.
Unary closure conditions are considered in detail in the next section.
REMARK 3.7.7 In any situation A Ì S, we may always regard S as a set of propositions: each element x:S names the proposition ``x Î A .'' Then we can read any finitary closure condition
|
In logic programming (Remark 1.7.2), the collection of terms generated by the constants and operation-symbols (of the underlying term calculus) is known as the Herbrand base, and the set S of all instances of the predicates is the Herbrand universe. A program is then a Horn theory.
Induction on closures Each instance K\triangleright t of a closure condition may be seen as an introduction rule for the (term t of) type A = F(Æ). Conversely there is an elimination rule, with a premise corresponding to each case of introduction. This manifests itself as an induction scheme, which is to propositions what structural recursion is to types.
DEFINITION 3.7.8 The induction scheme for a system of closure conditions \triangleright is
|
|
LEMMA 3.7.10 Define T:P(S)® P(S) by
|
Exercises 3.40 and 3.42 give the induction scheme in terms of T. We can use induction on closure conditions to investigate the least fixed point.
PROPOSITION 3.7.11 Let S be a complete (join-semi)lattice and T a monotone endofunction of it. Then T has a least fixed point A Î S, whose properties may be deduced from the following induction scheme:
|
PROOF: Define a closure condition on S = S by Á\triangleright ÚÁ for all Á Ì S, and also {U}\triangleright T(U). (Notice that we have not said U ³ VÞ U\triangleright V: see Exercise 3.41. Nor is this the closure condition derived from T in the lemma.) In particular Æ\triangleright ^, and any closed subset A has a greatest element A = ÚA Î A. By \triangleright -induction, "X.X Î AÞ X £ T(X), whilst "X.X Î AÞ X £ q for any fixed point q = T(q). But T(A) Î A so A = T(A) is the least fixed point of T. Other properties of A may be proved by instantiation of \triangleright -induction at A Î A = F(Æ). []
REMARK 3.7.12 For finitary closure conditions, the function T defined in Lemma 3.7.10 is Scott-continuous, and F(Æ) = \dirunionn Î NTn(Æ) is the least fixed point by Proposition 3.3.11. Then in the induction scheme it is enough to consider countable directed subsets Á, or just w-sequences. This idiom of induction is due to David Park (1976). When S = P(S), as in Lemma 3.7.10, this construction says that if X Î F(Æ) Ì S then X Î Tn(Æ) for some n. Classically, the least such n is called the rank of X, but in general this is not well defined intuitionistically.
It is a common but very clumsy idiom to prove something over a closed set by induction on the first time n when each element X gets in. For example, the rank of a goal in a logic program is the depth of its proof tree, which gives a lower bound on the execution time. But it is both difficult to calculate, and extremely crude, as the corresponding upper bound is kn, where k is the maximum arity. As in Remark 2.5.7, the assumption that n is least is unnecessary: it would be clearer to use induction on the closure condition directly. By Lemma 3.7.10 these two idioms of induction are equally expressive.
We have seen that Tarski's Theorem can be proved without the Scott-continuity assumption, and so can properties of the least fixed point:
THEOREM 3.7.13 Let \triangleright be a (possibly infinitary) system of closure conditions on a set S and q[X] any predicate on S = P(S) such that
Then q[A] holds, where A is the smallest \triangleright -closed subset.
PROOF: (Thierry Coquand) Let q be the least such predicate. Consider
|
Classically, the least fixed point can be approached by a transfinite union, which we investigate in Section 6.7, but Exercise 3.40 defines an intrinsic notion of ordinal for a particular problem.
For the obvious reasons of constructivity, we are primarily interested in finitary algebra, and we shall find in Section 5.6 that there is a significant obstacle to the extension of equational reasoning to infinitary operations. Why, then, should we be interested in infinitary algebra at all? Since there is a duality between finiteness and (infinitary) directed joins, the more we concentrate on the finitary, the more we need to know about infinitary operations and Scott-continuous functions between domains.
Section 3.9 considers the lattice of models of any Horn theory, and the semilattice which ``classifies'' models, making use of induction on closure conditions. We shall study algebraic theories in Section 4.6, using closure conditions in Sections 5.6 and 7.4 to impose relations. Recursion for free algebraic theories is the subject of Chapter VI. Closure operations are generalised to reflective subcategories in Examples 7.1.6 and further to monads in Section 7.5.