Formal Formal Topology, Topology, Chu Chu Space Space and and Approximable Approximable Concept Concept Xueyou Chen ∗ Qingguo Li Xueyou Chen2 and Qingguo Li1 (College of Mathematics and Economics, Hunan University, 1 College of Mathematics Chang and 410012, Sha, Hunan Economics, Hunan University, P.R.CHINA) ∗ Chang Sha, Hunan 410012, P.R.CHINA ( College of Mathematics and Information Science, 2 College of Mathematics Shandong andofInformation University Technology,Science, Shandong Zibo, University Shandong 255012,ofP.Technology, R. CHINA.) Zibo, Shandong 255012, P. R. CHINA. xueyou-chen@163.com xueyou-chen@163.com Abstract. Within Martin-Lőf type theory ([4]), G. Sambin initiated the intuitionistic formal topology which includes Scott algebraic domain theory as a special case (unary formal topology)([7]). In [6], he introduced the notions of (algebraic) information base and translation, and proved the equivalence between the category of (algebraic) information bases and the category of (algebraic) Scott domains. In [1], B. Ganter, R. Wille initiated formal concept analysis, which is an order-theoretical analysis of scientific data. Concept is one of the main notions and tools. Zhang considered a special form of Chu space, and introduced the notion of approximable concept in [3, 9, 10], which is a generalization of concept. These are two “parallel worlds”. In this paper, we introduce the notion of (new) information base, and investigate the relations between points of an information base and approximable concepts of a Chu space; the translations and context morphisms. Keywords: information base, Chu space, approximable concept, translation, context morphism 1 Introduction Within Martin-Lőf type theory [4], G. Sambin introduced formal topology, and proved that the category of unary formal topologies (information bases) with translations is equivalent to the category of Scott algebraic domains with Scott continuous mappings in [6]. In [7], he also introduced the new notion of formal topology. In [1], B. Ganter, R. Wille initiated formal concept analysis, which is an order-theoretical analysis of scientific data. Concept is one of the main notions and tools. Zhang, P. Hitzler and Shen considered a special kind of Chu space, and introduced the notion of approximable concept, as a generalization of concept. They obtained the equivalence between the category of formal contexts with context morphisms ([3]), the category of complete algebraic lattices with Scott Radim Bělohlávek, Václav Snášel (Eds.): CLA 2005, pp. 158–165, ISBN 80–248–0863–3. Formal Topology, Chu Space and Approximable Concept 159 continuous functions and the category of information systems (trivial consistency predicates) with approximable mappings. Formal topology and formal concept analysis ( Chu space, approximable concept) are two “parallel worlds”. In this paper, we define a new notion of information base, and investigate the relation between them. In this paper, we begin with an overview of information base, and Chu spaces, including Zhang’s work, that is Section 2, surveys preliminaries. Then we in- vestigate the relation between points of an information base and approximable concepts of a Chu space, that is Section 3. In the end, we investigate the relation between context morphisms and translations , i.e., Section 4. 2 Preliminaries Let us recall some main notions needed in the paper. i.e., information base and Chu space. The other notions, for examples: algebraic lattice, Scott continuous mapping, Scott algebraic domain, etc., see [2, 9]. 2.1 Information Base Within Martin-Lőf type theory ([4]), G. Sambin initiated the intuitionistic formal topology which includes Scott algebraic domain theory as a special case (unary formal topology)([7]). In [6], he introduced the notions of (algebraic) in- formation base and translation, and proved the equivalence between the category of (algebraic) information bases and the category of (algebraic) Scott domains, thus he obtained a new, simple representation of (algebraic) Scott domain. Infor- mation bases play the role which, in the customary approach, is played by two notions introduced by Scott, namely information systems and neighbourhood systems. Information bases with translations form a category, and S. Valentini showed that it is cartesian closed in [8]. In [7], G. Sambin introduced the new notion of formal topology, correspond- ing to the new definition, we also obtain a new definition of information base. Definition 1. An (algebraic) information base ϕ is a structure, i.e., ϕ = hS, ·, P os, /i, where S is a set, · a binary associative operation called com- bination, P os a property on S called positivity or consistency, and / a binary relation between elements of S called cover, which satisfy the following condi- tions, for a, b, c ∈ S. P os(a) a / b (monotonicity) P os(b) P os(a) → a / b (positivity) a/b (reflexivity) a / a 160 Xueyou Chen, Qingguo Li a/b b/c (transitivity) a/c a/b a/b (·−left) and a·c/b c·a/b a/b a/c (·−right) a/b·c In fact, the definition of information base given by G. Sambin, there exists a distinguished element 4, called unit, and for every a ∈ S, a / 4. In the above definition, we omit it. Definition 1 corresponds to the new definition of unary formal topology in [7]. As discussed in [6], an information base is a set S of pieces of information, a / b means a is more informative; a, b can always be put together in order to obtain a piece of information a · b, which combines the information given by a and b; P os(a) implies that a is individually consistent, P os(a · b) shows that a and b are compatible with the relation /; and if a is more informative than b, the consistency of a implies that that of b. For more details, see [6]. The notion of a point of an information base was defined as follow. Definition 2. A subset γ ⊆ S is a point of an information base ϕ, if a∈γ b∈γ a∈γ a/b 1 (i) , (ii) , a·b∈γ b∈γ a∈γ 2 . P os(a) A point is a filter of positive pieces of information. The set of all points of an information base ϕ, denoted by P t(ϕ). In [6], G. Sambin introduced the notion of a translation F . Definition 3. A relation F is called a translation between two information bases ϕ and φ = hT, ·, P os, /i, if for all a, c ∈ S and b, d ∈ T : aF b aF d aF b b / d P os(a) aF b 1 (1) (2) (3) aF b · d aF d P os(b) a / c cF b P os(a) → aF b 2 3 . aF b aF b 2.2 Chu Space As constructive models of linear logic, Barr and Seely brought Chu space to light in computer science. V. Pratt investigated the notion of Chu space in [5], and Zhang, P. Hitzler, Shen considered a special form of Chu spaces in [3, 9, 10] as follows. Definition 4. A Chu space P is a triple P = (Po , |=P , Pa ), where Po is a set of objects and Pa is a set of attributes. The satisfaction relation |=P is a Formal Topology, Chu Space and Approximable Concept 161 subset of Po × Pa . A mapping from a Chu space P = (Po , |=P , Pa ) to a Chu space Q = (Qo , |=Q , Qa ) is a pair of functions (fa , fo ) with fa : Pa → Qa and fo : Qo → Po such that for any x ∈ Pa and y ∈ Qo , fo (y) |=P x iff y |=Q fa (x). With respect to a Chu space P = (Po , |=P , Pa ), two functions can be defined: α : P (Po ) → P (Pa ) with X → {a | ∀x ∈ X x |=P a}, ω : P (Pa ) → P (Po ) with Y → {o | ∀y ∈ Y o |=P y}. α, ω form a Galois connection between P (Po ) and P (Pa ) , i.e., α, ω are anti-monotonic, and α ◦ ω , ω ◦ α are idempotent. Using the above two functions, Zhang and Shen introduced the notion of approximable concept in [9]. A subset A ⊆ Pa is an approximable concept if for every finite subset X ⊆ A, we have α(ω(X)) ⊆ A. 3 Information Base and Chu Space For any information base ϕ = hS, ·, P os, /i. Let P os(S) = {a ∈ S | P os(a)}, and ↑ a = {b | a / b}. Proposition 1. Pϕ = (P t( ϕ) , |=ϕ , P os(S)) is a Chu space, where γ ∈ P t(ϕ), a ∈ P os(S), γ |=ϕ a iff a ∈ γ. Proof. It is trivial. Lemma 1. (1) a ∈ S, P os(a) ⇒↑ a ∈ P t(ϕ). (2) γ ∈ P t(ϕ) ⇒ γ = ∪{↑ a | a ∈ γ}. Proof. It is trivial. Lemma 2. For a ∈ S, P os(a) ⇒↑ a is an approximable concept of Pϕ . Proof. For {b1 , b2 , · · · , bm } ⊆↑ a. ω({b1 , b2 , · · · , bm }) = {β | β |=ϕ bi , i = 1, 2, · · · , m} = {β | bi ∈ β, i = 1, 2, · · · , m}. This implies that ↑ (b1 · b2 · · · · · bm ) ∈ ω({b1 , b2 , · · · , bm }). ∀x ∈ α(ω({b1 , b2 , · · · , bm })) = {x | x |=ϕ β, ∀β ∈ ω({b1 , b2 , · · · , bm })}, that is to say, x ∈ β for all β ∈ ω({b1 , b2 , · · · , bm }). Hence we have x ∈↑ (b1 · b2 · · · · · bm ), so a/(b1 ·b2 ·· · ··bm )/x. By this , we get x ∈↑ a, thus α(ω({b1 , b2 , · · · , bm })) ⊆↑ a, ↑ a is an approximable concept. Lemma 3. Suppose A ⊆ Pa (P os(S)) is an approximable concept, a ∈ A ⇒↑ a ⊆ A. Proof. By the definition of an approximable concept, we know that α(ω({a})) ⊆ A. Since ω({a}) = {β | β |=ϕ a} = {β | a ∈ β} = {β |↑ a ⊆ β}, we have α(ω({a})) = {y | ∀β ∈ ω({a}), β |=ϕ y} = {y | ∀β ∈ ω({a}), y ∈ β}. So ∀b ∈↑ a, we have b ∈ β for all β ∈ ω({a}). This implies that b ∈ α(ω({a}), thus b ∈ A. By the above proof, we obtain that ↑ a ⊆ A. Proposition 2. γ ⊆ S is a point of ϕ ⇔ γ is a non-empty approximable concept of Pϕ . Proof. Suppose γ ∈ P t(ϕ), i.e., γ is a point. Since ∀a ∈ γ, P os(a), we have γ ⊆ Pa . For any finite subset {a1 , a2 , · · · , am } ⊆ γ. 162 Xueyou Chen, Qingguo Li ω({a1 , a2 , · · · , am }) = {β | ∀i(i = 1, 2, · · · , m), β |=ϕ ai } = {β | ∀i(i = 1, 2, · · · , m), ai ∈ β}. By Lemma 1, we have ↑ (a1 · a2 · · · · · am ) ∈ ω({a1 , a2 , · · · , am }). α(ω({a1 , a2 , · · · , am })) = α({β |↑ (a1 · a2 · · · · · am ) ⊆ β}). For b ∈ α(ω{a1 , a2 , · · · , am }), and for every β ∈ {β |↑ (a1 · a2 · · · · · am ) ⊆ β}, we have β |=ϕ b. This implies that b ∈ β for all β of the above set. So b ∈↑ (a1 · a2 · · · · · am ), thus b ∈ γ. By the above proof, we obtain that γ is an approximable concept. On the other hand, given an approximable concept A ⊆ Pa (P os(S)) of the derived Chu space, we will prove that A is a point of the information base ϕ. 1(i) Assume that x, y ∈ A, by the definition of an approximable concept, we have α(ω({x, y})) ⊆ A. ω({x, y}) = {β | β |=ϕ {x, y}} = {β | x ∈ β, y ∈ β}. This implies that x · y ∈ β for all β ∈ ω({x, y}). So we obtain x · y ∈ α(ω({x, y})), thus x · y ∈ A. 1(ii) If x ∈ A, x / y, by Lemma 3, y ∈ A. 2 x ∈ A, by the definition of Pa , we get P os(x). By the above proof and Definition 3, we obtain that A is a point of the information base ϕ. Conversely, suppose P = (Po , |=P , Pa ) is a Chu space. Let S = F in(Pa ), the set of finite subsets of Pa . The elements of Pa will be noted by x, y, z; the subsets of Pa (the elements of S) denoted by u, v, w. We define for every u ∈ S, P os(u); u · v = u ∪ v; u / v iff v ⊆ α(ω(u)). Proposition 3. As defined above, ϕP = (S, ·, P os, /) is an information base induced by a Chu space P . Proof. By the above definition, we have to prove ϕP satisfies the transitivity property. If u / v, v / w, then v ⊆ α(ω(u)), w ⊆ α(ω(v)). ω(u) = {ou | ou |=P y, ∀y ∈ u}; ω(v) = {ov | ov |=P x, ∀x ∈ v}. ∀x ∈ v, x ∈ α(ω(u)), we have for every ou ∈ ω(u), ou |=P x, thus ou ∈ ω(v). ∀z ∈ w, z ∈ α(ω(v)), we obtain that for every ov ∈ ω(v), ov |=P z, so ou |=P z. This implies that ∀ou ∈ ω(u), ou |=P z. Hence z ∈ α(ω(u)), w ⊆ α(ω(u)), thus u / w. Lemma 4. Suppose A ⊆ Pa is an approximable concept, then βA = {u | u ∈ F in(A)} is a point of ϕP . Proof. It is clear that βA satisfies the conditions 1(i) and 2 of Definition 2. we have to prove that it satisfies 1(ii). For u ∈ βA , v ∈ S, u / v, we have v ⊆ α(ω(u)) ⊆ A. But because v is a finite set, we get v ∈ βA . Lemma 5. Suppose β ⊆ S is a point of ϕP , then Aβ = ∪{α(ω(u)) | u ∈ β} is an approximable concept. Proof. For any subset w = {x1 , x2 , · · · , xm } ⊆ Aβ , by the definition of Aβ , there exist u1 , u2 , · · · , um ∈ β, such that xi ∈ α(β(ui )). Hence ui / {xi }. Formal Topology, Chu Space and Approximable Concept 163 Since β is a point of ϕP , we have u = u1 ∪· · ·∪um = u1 ·· · ··um /{x1 }·· · ··{xm } = {x1 , · · · , xm }, and u ∈ β. By the definition of /, {x1 , · · · , xm } ⊆ α(ω(u)). This implies that α(ω({x1 , · · · , xm })) ⊆ α(ω(α(ω(u)))) = α(ω(u)) ⊆ Aβ ([2]). So Aβ is an approximable concept. Proposition 4. There exists a bijection between the set of points of ϕP and the set of approximable concepts of P . Proof. (1) Given A is an approximable concept, by Lemma 4, we obtain a point βA = {u | u ∈ F in(A)}. By Lemma 5, we also know that AβA = ∪{α(ω(u)) | u ∈ βA } is an approximable concept of P . We try to prove A = AβA . Clearly, A ⊆ AβA . For every y ∈ AβA , there exists u ∈ βA , such that y ∈ α(ω(u)). Since u ∈ βA , we have u ∈ F in(A), so y ∈ α(ω(u)) ⊆ A by the definition of an approximable concept. Thus AβA ⊆ A. (2) Given β is a point ϕP , then we obtain an approximable concept Aβ by Lemma 5. But by Lemma 4, we also obtain a point βAβ of ϕP . In the similar way, we may prove β = βAβ . 4 Context Morphism and Translation In [3], P.Hitzler and Zhang introduced the notion of a context morphism as follows. Definition 5. Given formal contexts P = (Po , |=P , Pa ) and Q = (Qo , |=Q , Qa ), a context morphism →P Q =→ from P to Q is a relation →⊆ F in(Pa ) × 0 F in(Qa ), such that the following conditions are satisfied for all X, X , Y1 , Y2 ∈ 0 F in(Pa ), and Y, Y ∈ F in(Qa ); (1) ∅ → ∅, (2) X → Y1 and X → Y2 implies X → Y1 ∪ Y2 , 0 0 0 0 (3) X ⊆ αP (ωP (X)) and X → Y and Y ⊆ αQ (ωQ (Y )) imply X → Y . The category of formal contexts with context morphisms is cartesian closed ([3]). Given a context morphism →P Q ,we define a relation F ∗ between the derived information bases ϕP = (SP , ·, P os, /) and ϕQ = (SQ , ·, P os, /). For u, v ∈ SP , m, n ∈ SQ , uF ∗ v iff u →P Q v. Lemma 6. F ∗ is a translation between ϕP and ϕQ . Proof. By the definition of /, the condition (3) in Definition 5 may be written as: u / v, vF ∗ m, m / n imply uF ∗ n. By this, the proof is trivial. For the other direction, suppose F is a translation between two information bases ϕ and φ, F determines a context morphism →F from the Chu space Pϕ = (P t(ϕ), |=ϕ , P os(S)) to the Chu space Pφ = (P t(φ), |=φ , P os(T )). For X ∈ F in(P os(S)), Y ∈ F in(P os(T )), X →F Y iff ∀y ∈ Y, ∃x ∈ X, xF y. Lemma 7. →F is a context morphism between Pϕ and Pφ . Proof. It is clear that to prove →F satisfies the conditions (1) and (2) of Definition 5. 0 0 0 0 (3) If X ⊆ αP (ωP (X)), X → Y and Y ⊆ αQ (ωQ (Y )). Then for all y ∈ Y , 0 0 0 y ∈ Y , we have y / y. 0 0 0 0 0 0 0 0 Since X → Y , for y ∈ Y , there exists x ∈ X , such that x F y . 164 Xueyou Chen, Qingguo Li 0 0 0 In the similarly way, for all x ∈ X, x ∈ X , we also have x / x . By the above proof and Definition 3, we obtain that xF y, so X → Y . By the above analysis, for an information base ϕ = hS, ·, P os, /i, as defined in Proposition 1, we obtain a context CT (ϕ) = Pϕ . On the other hand, given a Chu space P , we also get an information base IN B(P ) = ϕP , as defined in Proposition 3. Hence we have two functors CT and IN B between the category of (new) information bases and the category of formal contexts. We say two categories C and D is equivalent, if there exist functors E : C → D and F : D → C, such that E ◦ F = idD , F ◦ E = idC . As showed above, G. Sambin introduced the new definition of formal topol- ogy in [7], and obtained that the category of (new) unary formal topologies is equivalent to the category of algebraic domains. The definition of (new) infor- mation base corresponds the new definition of unary formal topology, by this, we know that the category of (new) information bases is equivalent to the category of algebraic domains; by [9], we also know that the category of formal contexts is equivalent to the category of complete algebraic lattices; while the category of complete algebraic lattices is embedded into the category of algebraic domains, so the category of formal contexts is embedded into the category of information bases. In [3], P. Hitzler investigated the category of information systems with triv- ial consistency predicate, i.e., Con = the set of all finite tokens. By this, we may define the subcategory of the category of information bases, where ϕ = hS, ·, P os, /i, and S = P os. Furthermore we may prove that the subcategory is equivalent to the category of formal contexts. So we obtain the following propo- sitions. Proposition 5. The following four categories are equivalent, (1) the category of complete algebraic lattices and Scott continuous map- pings, (2) the category of formal contexts and context morphisms, (3) the category of information systems with trivial consistency predicates and approximable mappings, (4) the category of information bases with S = P os and translations. Acknowledgements This work was supported by the National Natural Science Foundation of China (Grant No. 10471035/A010104) and Natural Science Foundation of Shandong Province (Grant No. 2003ZX13). References 1. B. Ganter, R. Wille, Formal concept analysis, Springer-Verlag, 1999. 2. G. Gierz, et. al., Continuous lattices and Domain, Cambridge University Press, 2003. Formal Topology, Chu Space and Approximable Concept 165 3. P. Hitzler, G.Q. Zhang, A cartesian closed category of approximable concept struc- tures, Lecture Notes in Artificial Intelligence, 2004, to appear. 4. P. Martin-Lőf, Intuitionistic type theory, Notes by G. Sambin of a series of lecture given in Padua, June, 1980, Bibliopolis, Napoli, 1984. 5. V. Pratt, Chu spaces as a semantic bridge between linear logic and mathematics, Theoretical Computer Science, 294(2003), 439-471. 6. G. Sambin, S. Valentini, P. Virgili, Constructive domain theory as a branch of intuitionistic pointfree topology, Theoretical Computer Science 159 (1996), 319- 341. 7. G. Sambin, Formal topology and domains, Electronic Notes in Theoretical Com- puter Science 35, 2000. 8. S. Valentini, A cartesian closed category in Martin-lőf’s intuitionistic type theory, Theoretical Computer Science 290(2003),189-219. 9. G.Q. Zhang, G.Q. Shen, Approximable concepts, Chu spaces, and information systems, Theory and Applications of Categories, to appear. 10. G.Q. Zhang, Chu space, concept lattices, and domains, Electronic Notes in Theo- retical Computer Science Vol.83, 2004, 17 pages.