*This website uses Javascript to render markdown documents in your browser,
apply syntax highlighting to code fragments and render $\LaTeX$ formulas.
Below is the markdown source code of this page. You can either read that or
enable Javascript to have it rendered to HTML.*

# Axioms and CI implication After [installing `CInet::Tools`](/install), you can start the program `CImake`: ``` console $ CImake 0> ``` This presents you with a REPL (read-eval-print loop) for you to enter Perl code, similar to [`polymake`]. The REPL is just an interface to a standard Perl interpreter with all the CInet modules loaded. Using `CInet::Tools`, axioms for CI structures can easily be written down. A *semigraphoid* is a set of conditional independence statements which is closed under the following boolean formula $$ (ij|L) \wedge (ik|jL) \Rightarrow (ik|L) \wedge (ij|kL) $$ for any distinct $i, j, k$ and a set $L$ disjoint from $ijk$. The module [`CInet::Propositional`] provides syntactic sugar which allows us to define semigraphoids in a similarly succinct fashion: ``` console 0> propositional Semigraphoids = cube (ijk|L) -> (ij|L) & (ik|jL) => (ik|L) & (ij|kL); # time=00:00.00 ``` Some remarks about this line are in order since it deviates from usual Perl code. It uses the powerful [`Keyword::Declare`] module to hijack the Perl parser and add our own syntax extensions. In this case, the `propositional` keyword switches from the usual Perl parser to our own, which understands a math-like syntax for CI axioms. The other remark concerns terminology around `cube`s. By pure coincide, the faces of the $n$-dimensional hypercube $C_n$ index many important concepts in the theory of conditional independence structures. Its points (vertices) correspond to subsets of $[n]$ and therefore to subvectors of a random vector. Its edges (1-faces) are described by non-empty subsets with a distinguished element. We use $(i|L)$ to denote the edge that goes from vertex $L$ to vertex $iL$, whenever $i \not\in L$. Edges index elementary functional dependence statements. Lastly, squares (2-faces) are similarly indexed by $(ij|L)$ where $i \not= j$ and $L \cap ij = \emptyset$. This symbol corresponds to the 2-face with vertices $L, iL, jL, ijL$ and it indexes an elementary conditional independence statement. The part `cube (ijk|L)` in the above statement specifies that the following axioms require distinct atoms $i,j,k$ and an arbitrary disjoint subset $L$ of the ground set. The axioms given after the arrow `->` will be replicated for every such $3$-face of the $n$-cube. The result of this statement in our `CImake` environment is that it defines a function `Semigraphoids` which can be called with a ground set argument. This results in a sequence ([`CInet::Seq::Propositional`]) to be created for dealing with the set of all semigraphoids on that ground set. This sequence has a SAT solver ([`CInet::ManySAT`]) attached which allows to efficiently test membership, count or enumerate all elements. ``` console 1> Semigraphoids(3)->count 22 # time=00:00.01 2> Semigraphoids(4)->count 26424 # time=00:00.03 ``` The symmetric group $S_n$ acts on the ground $[n]$ and it induces an action on the cube $C_n$ and its face lattice which preserves the dimension of each face. In particular, there is a resulting action on CI structures as sets of 2-faces. This symmetry is implemented in `CInet::Symmetry`. The sequence object generated by `Semigraphoids` can be reduced modulo this symmetry using the following built-in function: ``` console 3> Semigraphoids(4)->modulo(SymmetricGroup)->count 1512 # time=00:00.35 ``` This still takes less than a second to compute! Semigraphoids are also closed under the entire symmetry group of the $n$-cube, also known as the hyperoctahedral group $B_n$. This is implemented as well: ``` console 4> Semigraphoids(4)->modulo(HyperoctahedralGroup)->count 629 # time=00:00.82 ``` Our final note about axioms in this tutorial is that axiom systems like `Semigraphoid` can be reused. *Graphoids* are semigraphoids which also fulfill the intersection axiom. ``` console 5> propositional Graphoids = cube(ijk|L) -> Semigraphoids, (ij|kL) & (ik|jL) => (ij|L) & (ik|L); 6> Graphoids(4)->count 6482 # time=00:00.11 ``` If a graphoid also satisfies upwards stability and weak transitivity, then it is an undirected graphical model. Due to faithfulness of these models, the following is a very roundabout way of counting undirected graphs: ``` console 7> propositional UndirectedGraphs = cube(ijk|L) -> Graphoids, (ij|L) => (ij|kL), (ij|L) => (ik|L) | (jk|L); 8> 0+ UndirectedGraphs(4)->count 64 # time=00:00.02 9> 0+ UndirectedGraphs(5)->count 1024 # time=00:00.16 10> 0+ UndirectedGraphs(6)->count 32768 # time=00:25.02 ``` The last line took 25 seconds to execute! Recall that the `->count` method uses an exact model counter (or \#SAT solver), in this case the program `dsharp`, on the boolean formula assembled from the given axioms. One piece of advice from years of using SAT solvers: It is sometimes more efficient to *enumerate* all solutions to the formula using an AllSAT solver --- especially when the number of solutions is comparatively small --- and to count the elements in the result set. This can work because counters and enumerators use very different algorithms and sometimes the enumeration strategy is more powerful against a given formula. ``` console 11> 0+ UndirectedGraphs(6)->list 32768 # time=00:02.30 ``` ## References * <a name="Stu05">[Stu05]</a> M. Studený: *Probabilistic conditional independence structures*. Springer, 2005. [`polymake`]: https://polymake.org/doku.php [`CInet::Propositional`]: /doc/CInet::Propositional [`CInet::ManySAT`]: /doc/CInet::ManySAT [`CInet::Seq::Propositional`]: /doc/CInet::Seq::Propositional [`Keyword::Declare`]: https://metacpan.org/pod/Keyword::Declare