Libkin Decomposition

README.md

@@ -33,7 +33,8 @@ much more.
    8. [Computing Traces in Contexts](doc/code/trace-context.clj)
    9. [Counting Quasiorders](doc/code/quasiorders.clj)
    10. [Rudolph's Algorithm for Computing Bases](doc/code/rudolph_computation.clj)
-   11. [Discovering Causal Implications](doc/Causal-Implications.org)
+   11. [Libkin Decompositions](doc/LibkinDecomposition.org)
+   12. [Direct Product Decompositions](doc/DirectProductDecompositions.org)
 5. Advanced Topics
    1. [pq-cores](doc/pq-cores-in-Formal-Contexts.md)
    2. [REST-API Usage](doc/REST-API-usage.md)

doc/DirectProductDecompositions.org

@@ -0,0 +1,123 @@
+#+property: header-args :wrap src text
+#+property: header-args:text :eval never
+
+* Direct Product Decompositions
+
+Based on the ~Libkin Decomposition~ formalized by Leonid Libkin, a variety of approaches for decomposing concept lattices were proposed, some of which are implemented in ~conexp-clj~.
+
+For a detailed description of these methods, consult [[https://doi.org/10.17170/kobra-2025021510916][Direct Product Decompositions of Concept Lattices]]:
+
+#+begin_src clojure
+(use 'conexp.fca.decompositions)
+(def ctx (make-context  #{"black" "red" "green" "blue" "yellow" "violet" "cyan" "white"}#{"R" "G" "B"} #{["red" "R"] ["green" "G"] ["blue" "B"] ["yellow" "R"] ["yellow" "G"] ["violet" "R"] ["violet" "B"] ["cyan" "G"] ["cyan" "B"] ["white" "R"] ["white" "G"] ["white" "B"]}))
+(def lat (concept-lattice ctx))
+(draw-lattice lat)
+#+end_src
+
+
+[[./images/rgb-lattice.png]]
+
+
+The decomposition pairs of a lattice can be computed using the method ~libkin-decomposition-pairs~:
+
+#+begin_src clojure :exports both
+(def pairs (libkin-decomposition-pairs lat))
+#+end_src
+
+#+RESULTS:
+#+begin_src text
+([[#{"cyan" "white"} #{"G" "B"}]
+  [#{"white" "violet" "yellow" "red"} #{"R"}]]
+ [[#{"white" "violet" "yellow" "red"} #{"R"}]
+  [#{"cyan" "white"} #{"G" "B"}]]
+ [[#{"white" "violet"} #{"R" "B"}]
+  [#{"cyan" "white" "yellow" "green"} #{"G"}]]
+ [[#{"blue" "cyan" "white" "violet" "yellow" "green" "red" "black"}
+   #{}]
+  [#{"white"} #{"G" "R" "B"}]]
+ [[#{"white" "yellow"} #{"G" "R"}]
+  [#{"blue" "cyan" "white" "violet"} #{"B"}]]
+ [[#{"white"} #{"G" "R" "B"}]
+  [#{"blue" "cyan" "white" "violet" "yellow" "green" "red" "black"}
+   #{}]]
+ [[#{"cyan" "white" "yellow" "green"} #{"G"}]
+  [#{"white" "violet"} #{"R" "B"}]]
+ [[#{"blue" "cyan" "white" "violet"} #{"B"}]
+  [#{"white" "yellow"} #{"G" "R"}]])
+#+end_src
+
+These can now be used to compute either a ~downset decomposition~, which is equivalent to the libkin decomposition, or a ~downset decomposition~.
+We will compute one each using the decomposition pari ~[[#{"cyan" "white"} #{"G" "B"}] [#{"white" "violet" "yellow" "red"} #{"R"}]]~:
+
+#+begin_src clojure :exports both
+(def downsets (downset-decomposition-lattices lat [[#{"cyan" "white"} #{"G" "B"}] [#{"white" "violet" "yellow" "red"} #{"R"}]]))
+(draw-lattice (first downsets))
+(draw-lattice (second downsets))
+#+end_src
+
+[[./images/downset-lattices.png]]
+
+
+#+begin_src clojure :exports both
+(def upsets (upset-decomposition-lattices lat [[#{"cyan" "white"} #{"G" "B"}] [#{"white" "violet" "yellow" "red"} #{"R"}]]))
+(draw-lattice (first upsets))
+(draw-lattice (second upsets))
+#+end_src
+
+[[./images/upset-lattices.png]]
+
+These pairs of lattices can now be reconstructed into their original lattices by applying the ~downset product~ or ~uzpset product~, respectively:
+
+#+begin_src clojure :exports both
+(downset-product (first downsets) (second downsets))
+(upset-product (first upsets) (second upsets))
+#+end_src
+
+Whether a lattice has non-trivial decomposition pairs may be verified using the ~decomposable?~ method.
+
+
+It may be useful to visualize all possible upset decomposition of a single concept lattice.
+To this end, the ~direct decomposition lattice~ of a concept lattice may be computed:
+
+[[./images/decomp-lattice.png]]
+
+#+begin_src clojure :exports both
+(def decomp-lat (direct-decomposition-lattice lat))
+(draw-lattice decomp-lat)
+#+end_src
+
+It is unfortunately not currently possible to directly visualize the concept lattices that form the elements of the ~direct decomposition lattice~:
+
+[[./images/decomp-lattice-drawing.png]]
+
+This lattice can also be computed in terms of the contexts of its constituent lattices using the ~ctx-decomposition-lattice~ method.
+
+This ~direct decomposition lattice~ can slo be used to determine the ~upset prime factorization~ of a concept lattice; a set of indecomposable concept lattices whose upset product is the original concept lattice:
+
+#+begin_src clojure :exports both
+(def factors (prime-factorization lat))
+(draw-lattice (first factors))
+(draw-lattice (second factors))
+(draw-lattice (last factors))
+#+end_src
+
+[[./images/prime-factors.png]]
+
+
+In practice, non-trivial direct product decomposition are rare. Therefore it is useful to consider substructures of concept lattices that may be decomposable.
+~conexp-clj~ offers two variants of such an algorithm.
+
+The method ~maximally-decomposable-filters~ returns all inclusion-maximal principal filters of a concept lattice, that have non-trivial upset decompostions.
+
+An example using the ~bodies-of-water~ context:
+
+[[./images/max-decomp-filters.png]]
+
+Alternatively, all maximally decomposable intervals may be computed using the ~maximally-decomposable-intervals~ method:
+
+[[./images/max-decomp-intervals.png]]
+
+#+begin_src clojure :exports both
+(maximally-decomposable-filters lat)
+(maximally-decomposable-intervals lat)
+#+end_src

doc/LibkinDecomposition.org

@@ -0,0 +1,87 @@
+#+property: header-args :wrap src text
+#+property: header-args:text :eval never
+
+* Libkin Decomposition
+
+~conexp-clj~ allows for the computation of Libkin Decompositions of lattices.
+For an explanation of the concept consult "Direct product decompositions of lattices, closures and relation schemes" by Leonid Libkin
+
+Some of the following functions require the ~decompositions~ namespace:
+
+
+#+begin_src clojure
+(use 'conexp.fca.decompositions)
+#+end_src
+
+(use 'conexp.fca.decompositions)
+
+We will consider the following lattice as an example:
+
+#+begin_src clojure :exports both
+(def ctx (read-context "testing-data/drive_concepts_for_motorcars.cxt"))
+(def lat (concept-lattice ctx))
+#+end_src
+
+[[./images/car-lattice.png]]
+
+A Libkin decomposition of a lattice L is a pair of sublattices of L, whose product is isomorphic to L.
+Libkin decompositions are each induced by a decomposition pair, a neutral element in L and its Complement.
+
+All decomposition pairs of the lattice can be computed using the method ~libkin-decomposition-pairs~:
+
+#+begin_src clojure :exports both
+(def pairs (libkin-decomposition-pairs lat))
+#+end_src
+
+#+RESULTS:
+#+begin_src text
+([[#{"Conventional" "All-wheel" "Rear-wheel" "Mid-engine"} #{"Dl+"}]
+  [#{"Front-wheel"}
+   #{"E+" "C-l" "De+" "C-vl" "E++" "Dl-" "S-u" "R+" "M+" "R++"}]]
+ [[#{}
+   #{"E+" "C-l" "E-" "C-h" "De+" "Dl+" "C-vl" "E++" "S-u/n" "Dl++"
+     "Dl-" "M++" "S-u" "R+" "S-n" "S-o" "De-" "De++" "M+" "M--" "R--"
+     "C-m" "M-" "R++" "E--"}]
+  [#{"Conventional" "All-wheel" "Rear-wheel" "Mid-engine"
+     "Front-wheel"}
+   #{}]]
+ [[#{"Conventional" "All-wheel" "Rear-wheel" "Mid-engine"
+     "Front-wheel"}
+   #{}]
+  [#{}
+   #{"E+" "C-l" "E-" "C-h" "De+" "Dl+" "C-vl" "E++" "S-u/n" "Dl++"
+     "Dl-" "M++" "S-u" "R+" "S-n" "S-o" "De-" "De++" "M+" "M--" "R--"
+     "C-m" "M-" "R++" "E--"}]]
+ [[#{"Front-wheel"}
+   #{"E+" "C-l" "De+" "C-vl" "E++" "Dl-" "S-u" "R+" "M+" "R++"}]
+  [#{"Conventional" "All-wheel" "Rear-wheel" "Mid-engine"} #{"Dl+"}]])
+#+end_src
+
+Computing the order ideal of both entries of the pair yields the two sublattices forming the decomposition.
+
+The lattices implied by the decomposition through a specific decomposition pair can be exlicitely generated using ~libkin-decomposition-lattices~:
+
+#+begin_src clojure :exports both
+(def lattice-pair (libkin-decomposition-lattices lat [[#{"Conventional" "All-wheel" "Rear-wheel" "Mid-engine"} #{"Dl+"}]
+  [#{"Front-wheel"}
+   #{"E+" "C-l" "De+" "C-vl" "E++" "Dl-" "S-u" "R+" "M+" "R++"}]]))
+#+end_src
+
+These lattices may be visualized as described in Concept-Lattices.org .
+
+#+begin_src text
+(draw-lattice (first lattice-pair))
+(draw-lattice (last lattice-pair))
+#+end_src
+
+[[./images/decomposed-lattice1.png]]
+[[./images/decomposed-lattice2.png]]
+
+#+begin_src text
+(def prod-lat (lattice-product (first lattice-pair) (last lattice-pair)))
+(draw-lattice prod-lat)
+#+end_src
+
+The product of these lattices yields a lattice isomorphic to L:
+
+[[./images/prod-lattice.png]]