The Constructors bring structure in formulas and interpretations.
They allow for the composition of complex syntaxes and semantics in
logics. Recursive structures are often introduced by a recursive
composition of these functors. They often mimick data structures in
programming languages. Many of these structures can be defined as
combinators of simpler functors, hence a great saving of means.
The product of syntaxes and interpretation domains. Formulas are
couples of sub-formulas, and interpretations are couples of
sub-interpretations. This functor corresponds to couples in
programming languages, and enables the combination of orthogonal
properties such as attributes and values to form valued attributes.
or f = (f1,f2) g = (g1,g2) f1 ⊑1g1f2 ⊑2g2:
∀ i ∈ {1,2}: cs⊑i(fi,gi)
⇒ ∀ i ∈ {1,2}: fi ⊑igi ⇒ Mi(fi) ⊆ Mi(gi)
⇒ ∀ i ∈ {1,2}: fi ⊑igi ⇒ M1(f1) × M2(f2) ⊆ M1(g1) × M2(g2)
⇒ (f1,f2) ⊑ (g1,g2) ⇒ M((f1,f2)) ⊆ M((g1,g2))
⇒ M(f) ⊆ M(g).
Hence in all cases M(f) ⊆ M(g).
■
cp⊑(f,g) ⇐ ∀ i ∈ {1,2}: cp⊑i(fi,gi) reduced.boti cp⊑⇐ ∀ i ∈ {1,2}: cp⊑ireduced.boti cp'⊑⇐ ∀ i ∈ {1,2}: cp'⊑ireduced.bot'i
Proof: M(f) ⊆ M(g) implies
either M(f) = ∅:
⇒ f = 0 (f = (f1,f2) (M1(f1) = ∅ M2(f2) = ∅))
⇒ f = 0 (f = (f1,f2) ({f1} ⊑1* ∅ {f2} ⊑2* ∅)) (reduced.bot1,reduced.bot2)
⇒ f = 0 (f = (f1,f2) f1 ⊑1 ⊥1f2 ⊑2 ⊥2)
⇒ f ⊑ g.
or M(f) ≠ ∅:
⇒ f = (f1,f2) g = (g1,g2) M((f1,f2)) ⊆ M((g1,g2))
⇒ f = (f1,f2) g = (g1,g2) M1(f1) × M2(f2) ⊆ M1(g1) × M2(g2)
⇒ f = (f1,f2) g = (g1,g2) M1(f1) ⊆ M1(g1) M2(f2) ⊆ M2(g2)
⇒ f = (f1,f2) g = (g1,g2) f1 ⊑1g1f2 ⊑ g2 (∀ i ∈ {1,2}: cp⊑i(fi,gi))
⇒ f ⊑ g.
reduced.bot ⇐ ∀ i ∈ {1,2}: reduced.boti reduced.bot' ⇐ ∀ i ∈ {1,2}: reduced.bot'i
Proof:
Let f ∈ AS: M(f) ⊆ ∅. Then
either f = 0: f ⊑ ⊥ ⇒ {f} ⊑* ∅,
or f = (f1,f2): M1(f1) × M2(f2) = ∅, which implies
either M1(f1) = ∅: so {f1} ⊑1* ∅ (reduced.boti)
⇒ f1 ⊑1 ⊥1 ⇒ f ⊑ ⊥
⇒ {f} ⊑* ∅,
or M2(f2) = ∅: idem.
Hence in all cases {f} ⊑* ∅.
■
reduced.right ⇐ ∀ i ∈ {1,2}: cs⊑icp⊑ics⊥icp⊤idefst⊓icp⊓ireduced.righti
Proof:
Let f ∈ AS, G ⊆ AS.
We prove that given M(f) ⊆ ∪g ∈ GM(g),
we obtain that {f} ⊑*G.
Firstly, assume that for some i ∈ {1,2}, we have Mi(fi) ⊆ ∪gi ∈ GiMi(gi)
⇒ {fi} ⊑i* ⊔iGi) (reduced.righti)
⇒
∨
⎧
⎨
⎩
fi ⊑i ⊥i
∃ hi ∈ ⊔iGi: ⊤i ⊑ihi
∃ hi ∈ ⊔iGi: fi ⊑ihi
⇒
∨
⎧
⎨
⎩
Mi(fi) ⊆ ∅
(cs⊥i)
∃ hi ∈ ⊔iGi: Ii ⊆ Mi(hi)
(cp⊤i)
∃ hi ∈ ⊔iGi: Mi(fi) ⊆ Mi(hi)
(cs⊑i)
⇒ ∃ hi ∈ ⊔iGi: Mi(fi) ⊆ Mi(hi)
⇒ Mi(fi) ⊆ Mi([⊔iGi]), where [E] denotes “some element in the set E”.
Hence the equation
Mi(fi) ⊆
∪
gi ∈ Gi
Mi(gi) ⇒ Mi(fi) ⊆ Mi([⊔iGi]).
(C.1)
Secondly, let K = (M1(f1),G1,⊨1) be a formal context,
where G1 denotes the projection of G on the first logic.
Let G = {G' ⊆ G ∣ ∃ c ∈ Max(γK(M1(f1))): (g'1,g'2) ∈ G' ⇔ g'1 ∈ int(c)}.
Then we obtain:
∀ G' ∈ G: extK(G'1) ≠ ∅, because G'1 is the intent of some γ-concept
⇒ ∀ G' ∈ G: M1(f1) ∩ ∩g'1 ∈ G'1M1(g'1) ≠ ∅
⇒ ∩g'1 ∈ G'1M1(g'1) ≠ ∅
⇒ def(⊓1G'1) M1(⊓1G'1) ⊇ ∩g'1 ∈ G'1M1(g'1), (defst⊓1, cp⊓1)
and M1(f1) ⊆ ∪G' ∈ GextK(G'1), because maximum γ-concepts cover all objects
⇒ M1(f1) ⊆ ∪G' ∈ G(∩g'1 ∈ G'1M1(g'1)), which entails with previous result
M1(f1) ⊆
∪
G' ∈ G
M1(⊓1G'1).
(C.2)
Now, starting from M(f) ⊆ ∪g ∈ GM(g), there are 2 cases:
Also, from (C.2), M1(f1) ⊆ ∪G' ∈ GM1(⊓1G'1), which implies by (C.1)
x1 = [⊔G' ∈ G⊓1G'1] M1(f1) ⊆ M1(x1).
(C.4)
Hence, by putting (C.4) and (C.3) together, we obtain M1(f1) × M2(f2) ⊆ M1(x1) × M2(x2)
⇒ M((f1,f2)) ⊆ M((x1,x2)),
where (x1,x2) = ([⊔1H1], ⊓2H2),
where H = { (⊓1G'1,[⊔2G'2]) ∣ G' ∈ G}.
From the definition of ⊔, extended as in (C.1), we have
H ⊆ ⊔ G, and (x1,x2) ∈ ⊔ H. Hence
(x1,x2) ∈ ⊔ G
⇒ ∃ x ∈ ⊔ G: M(f) ⊆ M(x)
⇒ ∃ x ∈ ⊔ G: f ⊑ x (cp⊑)
⇒ {f} ⊑*G.
■
The multisets of sub-formulas and interpretations. These can also be
seen as unordered tuples. Multisets can contain several equivalent
elements, so that it can be expressed that a multiset contains “at
least n elements of some type”. It can also be expressed that 2
properties are satisfied by 2 different elements.
AS =defNASE TELL =defNTELLE ASK =defNASKE
Formulas are multisets, whose elements are formulas of E. A possible
concrete syntax is {e1,...,en}. A shorthand for e, ...,e (n
times the same element e) is ne; and a shorthand for {ne}
is simply ne. In this way the property “contains at least n
elements of type e” can be expressed as ne. This can be
combined for different numbers and types of elements as in {n1e1, n2e2}, whose meaning is “contains n1 different elements
of type e1, and n2 other elements of type e2”.
Proof: E ∈ TELL ⇒ ∀ e ∈ E: e ∈ TELLE
⇒ ∀ e ∈ E: ∃ iE ∈ IE: iE ⊨Ee
⇒ ∃ i ∈ I: ∃ ρ ∈ E ↪ i: ∀ e ∈ E: ρ(e) ⊨Ee
⇒ ∃ i ∈ I: i ⊨ E.
■
cs⊑(E,F) ⇐ ∀ e ∈ E, f ∈ F: cs⊑E(e,f) cs⊑⇐ cs⊑E
Proof: E ⊑ F —→ ∃ ρ ∈ F ↪ E: ∀ f ∈ F: ρ(f) ⊑Ef. i ⊨ E ⇒ ∃ ρ' ∈ E ↪ i: ∀ e ∈ E: ρ'(e) ⊨Ee
⇒ ∃ ρ' ∈ E ↪ i: ∀ f ∈ F: ρ'(ρ(f)) ⊨E ρ(f) ⊑Ef hypothesis
⇒ ∃ ρ'' = ρ ∘ ρ' ∈ F ↪ i: ∀ f ∈ F: ρ'(ρ(f)) ⊨Ef ∀ e ∈ E, f ∈ F: cs⊑E(e,f)
⇒ ∃ ρ'' ∈ F ↪ i: ∀ f ∈ F: ρ''(f) ⊨Ef
⇒ i ⊨ F.
Hence M(E) ⊆ M(F).
■
cp⊑(E,F) ⇐ ∀ e ∈ E:sg(e) ∀ e ∈ E, f ∈ F: cp⊑E(e,f) cp'⊑⇐ cp'⊑Esg'E
Proof:
We prove that E ¬ ⊑F implies ∃ i ∈ I: i ⊨ Ei ¬ ⊨F.
Firstly, E ¬ ⊑F
⇒ ∀ ρ ∈ F ↪ E: ∃ f ∈ F: ρ(f) ¬ ⊑Ef
⇒ ∀ ρ ∈ F ↪ E: ∃ f ∈ F: ME(ρ(f)) ¬ ⊆ME(f). ∀ e ∈ E, f ∈ F: cp⊑E(e,f)
Secondly, let i = ⊎e ∈ EME(e) multiset union
and ∀ e ∈ E: ρ'(e) = choice(ME(e)). (∀ e ∈ E: sgE(e))
This implies that ρ' is a bijection from E to i
⇒ ∃ ρ' ∈ E ↪ i: ∀ e ∈ E: ρ'(e) ⊨Ee
⇒ i ⊨ E.
Now, let ρ'' ∈ F ↪ i
⇒ ∃ ρ ∈ F ↪ E: ρ'' = ρ ∘ ρ' ρ' is a bijection
⇒ ∃ ρ ∈ F ↪ E: ρ'' = ρ ∘ ρ', ∃ f ∈ F: ME(ρ(f)) ¬ ⊆ME(f) hypothesis
⇒ ... ∃ f ∈ F: ρ'(ρ(f)) ∉ ME(f) hypothesis
⇒ ... ∃ f ∈ F: ρ''(f) ¬ ⊨Ef
⇒ ∃ f ∈ F: ρ''(f) ¬ ⊨Ef.
Hence ∀ ρ'' ∈ F ↪ i: ∃ f ∈ F: ρ''(f) ¬ ⊨Ef
⇒ i ¬ ⊨f.
■
cp⊤
Proof:
Trivial from definition of ⊤, and semantics.
■
This combinator defines vectors as a generalization of pairs to an
arbitrary number of elements (starting from 0). This is close to
arrays in programming languages.
This combinator defines trees in a very generic way. X abstracts the
labelling of nodes, and F is a functor that abstracts the way the
children of a node are organized.
