Formal concept analysis #
This file defines concept lattices. A concept of a relation r : α → β → Prop→ β → Prop→ 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 #
- [Davey, Priestley Introduction to Lattices and Order][davey_priestley]
Tags #
concept, formal concept analysis, intent, extend, attribute
Intent and extent #
The intent closure of s : Set α
along a relation r : α → β → Prop→ β → Prop→ Prop
is the set of all elements
which r
relates to all elements of s
.
Equations
- intentClosure r s = { b | ⦃a : α⦄ → a ∈ s → r a b }
The extent closure of t : Set β
along a relation r : α → β → Prop→ β → Prop→ Prop
is the set of all elements
which r
relates to all elements of t
.
Equations
- extentClosure r t = { a | ⦃b : β⦄ → b ∈ t → r a b }
Concepts #
The axiom of a
Concept
stating that the closure of the first set is the second set.closure_fst : intentClosure r toProd.fst = toProd.sndThe axiom of a
Concept
stating that the closure of the second set is the first set.closure_snd : extentClosure r toProd.snd = toProd.fst
The formal concepts of a relation. A concept of r : α → β → Prop→ β → Prop→ 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
.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- Concept.instBoundedOrderConceptToLEToPreorderToPartialOrderInstSemilatticeInfConcept = BoundedOrder.mk
Equations
- One or more equations did not get rendered due to their size.
Swap the sets of a concept to make it a concept of the dual context.
Equations
- Concept.swap c = { toProd := Prod.swap c.toProd, closure_fst := (_ : extentClosure r c.toProd.snd = c.toProd.fst), closure_snd := (_ : intentClosure r c.toProd.fst = c.toProd.snd) }