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.

## Counting, enumerating and symmetry reduction

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
```

## Conditional independence implication

Many basic families of CI structures can be defined axiomatically. In this
case, SAT solvers can be used to compute CI statements which are implied by
the axioms and additional CI assumptions. This is known as the conditional
independence implication problem for the family under consideration.

The families considered above are already provided by the
[`CInet::Propositional::Families`](/doc/CInet::Propositional::Families) module
which is automatically loaded by `CImake`. Families defined using the
`propositional` mechanism have implication testing methods built into them.
To check if $(12|3) \wedge (13|4) \wedge (14|2) \Rightarrow (12|)$ holds
modulo the gaussoid axioms, simply execute:

``` console
12> my $p = CIR(4, [[1,2],[3]], [[1,3],[4]], [[1,4],[2]])
*0****0**0**************
13> Gaussoids->imply($p => [[1,2],[]])
"" # time=00:00.01
```

The `CIR` function creates a [`CInet::Relation`](/doc/CInet::Relation)
which is used to represent a CI structure. This structure holds the premises
of the query. The `imply` method is then used to check if the statements in
`$p` and the gaussoid axioms together imply `(12|)`. The result is a "no" in
this case and is reached in just 10ms. Note that this is rule (20) in
[[LM07]](#LM07). It is an implication which is valid for regular Gaussian
distributions but which cannot be derived from the gaussoid axioms.

On the other hand, let's consider an instance of the long semigraphoid
derivation sequences in [[Mat02]](#Mat02). The function `L` defined in
the file `longmatus.pl` quoted below constructs the sequence $\mathcal{L}_n$
of CI structures defined in the paper. It is shown there that in order to
derive the consequence $(12|3n)$ from $\mathcal{L}_n$ one needs to perform
$2^{n-2}-1$ inference steps with the semigraphoid axioms. The SAT solver
is keeping up well solving all tasks from $n = 4, \dots, 10$ in about 4
seconds. (This includes the time required to construct $\mathcal{K}_n$
from which $\mathcal{L}_n$ is extracted.)

``` console
14> do './longmatus.pl'
15> map Semigraphoids->imply(L($_) => [[1,2],[3,$_]]), 4 .. 10
(1, 1, 1, 1, 1, 1, 1) # time=00:04.25
```

``` perl
# longmatus.pl

use Modern::Perl 2018;
use CInet::Tools;

# Return the vertex set of 𝓚_n ordered according to the connected components.
# The first two elements are the first isolated edge. Then every triple is a
# connected component and the last two elements are an isolated edge again.
#
# The ordering of these vertices is crucial. It is from left to right just as
# in Matúš's pictures. This allows us to easily recurse (the construction can
# be seen as a kind of grey code) and to extract the substructure 𝓛_n below.
sub K {
    my $n = shift;
    if ($n == 4) {
        return (
            [[1,2],[3]], [[1,3],[]], [[1,3],[2]], [[1,2],[]], [[2,4],[1]],
            [[2,4],[]], [[1,2],[4]], [[1,3],[2,4]], [[1,3],[4]], [[1,2],[3,4]]
        );
    }
    else {
        my @prev = K($n-1);
        return (
            @prev, [[2,$n],[1,3,$n-1]], [[2,$n],[3,$n-1]],
            reverse map { [$_->[0], [$_->[1]->@*, $n]] } @prev
        );
    }
}

sub L {
    my $n = shift;
    my @comps = K $n;
    CIR($n,
        $comps[0], $comps[1],
        @comps[map { 4+3*($_-1) } 1 .. (@comps-4)/3]
    )
}
```

## References

* <a name="Stu05">[Stu05]</a> M. Studený: *Probabilistic conditional independence structures*. Springer (2005).
* <a name="LM07">[LM07]</a> R. Lněnička and F. Matúš: *On Gaussian conditional independence structures*. Kybernetika 43:3 (2007).
* <a name="Mat02">[Mat02]</a> F. Matúš: *Lengths of semigraphoid inferences*. Ann. Math. Artif. Intell. 35 (2002).

[`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