Formal concept analysis #
This file defines concept lattices. A concept of a relation r : α → β → Prop
is a pair of sets
s : Set α
and t : Set β
such that s
is the set of all a : α
that are related to all elements
of t
, and t
is the set of all b : β
that are related to all elements of s
.
Ordering the concepts of a relation r
by inclusion on the first component gives rise to a
concept lattice. Every concept lattice is complete and in fact every complete lattice arises as
the concept lattice of its ≤
.
Implementation notes #
Concept lattices are usually defined from a context, that is the triple (α, β, r)
, but the type
of r
determines α
and β
already, so we do not define contexts as a separate object.
TODO #
Prove the fundamental theorem of concept lattices.
References #
Tags #
concept, formal concept analysis, intent, extend, attribute
Intent and extent #
Concepts #
The formal concepts of a relation. A concept of r : α → β → Prop
is a pair of sets s
, t
such that s
is the set of all elements that are r
-related to all of t
and t
is the set of
all elements that are r
-related to all of s
.
- closure_fst : intentClosure r self.toProd.1 = self.toProd.2
The axiom of a
Concept
stating that the closure of the first set is the second set. - closure_snd : extentClosure r self.toProd.2 = self.toProd.1
The axiom of a
Concept
stating that the closure of the second set is the first set.
Instances For
Equations
- Concept.instSemilatticeInfConcept = Function.Injective.semilatticeInf (fun (c : Concept α β r) => c.toProd.1) ⋯ ⋯
Equations
Equations
- Concept.instSupSet = { sSup := fun (S : Set (Concept α β r)) => { toProd := (extentClosure r (⋂ c ∈ S, c.toProd.2), ⋂ c ∈ S, c.toProd.2), closure_fst := ⋯, closure_snd := ⋯ } }
Equations
- Concept.instInfSet = { sInf := fun (S : Set (Concept α β r)) => { toProd := (⋂ c ∈ S, c.toProd.1, intentClosure r (⋂ c ∈ S, c.toProd.1)), closure_fst := ⋯, closure_snd := ⋯ } }
Equations
- Concept.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- Concept.instInhabited = { default := ⊥ }
Swap the sets of a concept to make it a concept of the dual context.
Equations
- c.swap = { toProd := c.swap, closure_fst := ⋯, closure_snd := ⋯ }
Instances For
The dual of a concept lattice is isomorphic to the concept lattice of the dual context.
Equations
- Concept.swapEquiv = { toFun := Concept.swap ∘ ⇑OrderDual.ofDual, invFun := ⇑OrderDual.toDual ∘ Concept.swap, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }