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 #
- [Davey, Priestley Introduction to Lattices and Order][davey_priestley]
Tags #
concept, formal concept analysis, intent, extend, attribute
Intent and extent #
Concepts #
- fst : Set α
- snd : Set β
- closure_fst : intentClosure r s.fst = s.snd
The axiom of a
Concept
stating that the closure of the first set is the second set. - closure_snd : extentClosure r s.snd = s.fst
The axiom of a
Concept
stating that the closure of the second set is the first set.
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
.
Instances For
Swap the sets of a concept to make it a concept of the dual context.
Instances For
The dual of a concept lattice is isomorphic to the concept lattice of the dual context.