API reference

Xitip

Information Theoretic Inequality Prover in pure Julia.

Decides whether an information expression (over entropies and mutual informations of discrete random variables) follows from the basic properties of Shannon entropy, optionally under constraints such as Markov chains, independence or functional dependence.

This is a reimplementation of Xitip/Citip/ITIP that needs only Julia's standard library. Every answer comes with a proof or a counterexample that is verified in exact rational arithmetic, so no floating point tolerance decides whether an inequality holds.

julia> using Xitip

julia> prove("I(X;Y|Z) <= I(X;Y)", "H(Z) = 0")
true

julia> explain("H(X,Y) <= H(X) + H(Y)")
TRUE
Proof of  H(X) + H(Y) - H(X,Y) >= 0:
         1 * ( I(X;Y) >= 0 )

Exported: prove, explain, count_variables, Result, Proof, Counterexample, XitipError, SyntaxError.

prove(lines...; method=:auto) -> Bool

Check whether the first statement is a Shannon-type consequence of the remaining ones (the constraints). false means the statement is either false or a non-Shannon-type inequality. Throws XitipError for contradictory constraints and SyntaxError for invalid input.

Every result is exact: method=:auto finds a proof or a counterexample with non-negative least squares and verifies it in exact rational arithmetic (falling back to the exact simplex method); method=:simplex uses the exact simplex method only, which is much slower beyond about 7 variables.

See explain to get the proof or counterexample itself.

Examples

julia> prove("I(X;Y|Z) <= I(X;Y)")
false

julia> prove("I(X;Y|Z) <= I(X;Y)", "H(Z) = 0")
true

explain(lines...; method=:auto) -> Result

Like prove, but also returns the exactly verified certificates: a Proof for each part of a true statement, or one Counterexample.

Examples

julia> explain("H(X,Y) <= H(X) + H(Y)")
TRUE
Proof of  H(X) + H(Y) - H(X,Y) >= 0:
         1 * ( I(X;Y) >= 0 )

count_variables(lines...) -> Int

Number of distinct random variables in all statements (like oXitipLen).

Examples

julia> count_variables("I(X;Y|Z) <= I(X;Y)")
3

Result

The verdict of explain together with its certificates: one Proof per inquiry if verdict is true, one Counterexample otherwise. certificates is empty if the exact simplex method decided, which produces none.

Proof

Why an information expression is Shannon-type: it equals a non-negative combination of elemental inequalities and constraints, plus a non-negative constant.

steps is the same proof as a derivation that subtracts one non-negative quantity at a time; print it with print_proof.

ProofStep

One step of a step-by-step proof: coefficient times the non-negative quantity name is split off the expression, leaving remainder. So

expression so far  =  coefficient * name  +  remainder

expansion is the quantity written with entropies, label is how it is written in the chain of equalities (a short C1 for a constraint, whose text is then in source), and remainder_name is the remainder as a single information quantity where it is one.

named is the quantity itself under a name where it has one — an equality constraint used in reverse is the negation of one, as in -I(W;Y|X) — and justification says why it is non-negative: ">= 0" for an inequality, "= 0" for an equality constraint.

Counterexample

Why an information expression could not be proven: entropy values h satisfying every elemental inequality and every constraint, but not the expression itself. Such an h need not come from an actual probability distribution: beyond three variables not every polymatroid is entropic, so the expression may still be a (non-Shannon-type) truth.

direction marks the degenerate case where h is not a point but a direction along which the expression decreases without bound.

A Proof or a Counterexample.

print_proof([io=stdout], x)

Print a Proof, Counterexample or Result as a step-by-step derivation: each step subtracts one non-negative quantity from the expression and shows what is left, until nothing (or a non-negative constant) remains.

Examples

julia> print_proof(explain("I(X;Z) <= I(X;Y)", "X/Y/Z"))
Proof of  E >= 0  where  E = H(Y) - H(Z) - H(X,Y) + H(X,Z)

  step 1:  subtract  1 * ( constraint 1 (negated) )
                     = -H(Y) + H(Z) + H(X,Y) - H(X,Z) + H(Y,Z) - H(X,Y,Z)
           leaving   H(Y,Z) - H(X,Y,Z) ... 

latex([io=stdout], x)

Write a Proof, Counterexample or Result as LaTeX, ready to paste into a paper. Proofs become an align* block that rewrites the expression as a sum of non-negative quantities; a counterexample becomes the table of entropy values that defeats it.

Examples

julia> latex(explain("H(X,Y,Z) <= H(X,Y) + H(Z)"))
\begin{align*}
  H(Z) + H(X,Y) - H(X,Y,Z)
    &= I(X ; Z \mid Y) + I(Y ; Z) \\
    &\ge 0 .
\end{align*}

latex([io], p::Proof; steps=false, expand=false, width=68)

The proof as LaTeX. By default the expression is rewritten as a sum of non-negative quantities; steps=true gives the full chain of equalities, splitting one term off at a time with the remainder in brackets. expand=true lists the entropy form of every term (constraints are always listed, as C_1, C_2, ...).

LaTeX source of x as a string; see latex.

lean(lines...; theorem="xitip_proof", imports=true) -> String

The Lean 4 source of the arithmetic core of a proof: one real variable per joint entropy, one hypothesis per inequality the proof uses, the statement as the goal, and linarith to close it.

The statement must be provable. What comes back is checked by Lean, not by this package — see Formal proof in Lean for what the core does and does not say, and for the bridge that gives its variables their meaning.

julia> print(lean("H(X,Y,Z) <= H(X,Y) + H(Z)"; imports=false))
/-
  H(X,Y,Z) <= H(X,Y) + H(Z)

  Generated by Xitip.jl. Every hypothesis is an elemental inequality;
  the goal is the statement with everything moved to one side.
-/
theorem xitip_proof
    (h_Y h_X_Y h_Y_Z h_X_Y_Z h_Z : ℝ)
    -- I(X;Z|Y) >= 0
    (e1 : 0 ≤ -h_Y + h_X_Y + h_Y_Z - h_X_Y_Z)
    -- I(Y;Z) >= 0
    (e2 : 0 ≤ h_Y + h_Z - h_Y_Z)
    : 0 ≤ h_X_Y + h_Z - h_X_Y_Z := by
  linarith

proof_tree(p::Proof) -> DecompositionTree
proof_tree(r::Result) -> DecompositionTree

The derivation behind a proof as a tree: the expression splits into the first non-negative term and what is left, that remainder splits again, and so on until nothing (or a non-negative constant) remains.

A constraint is shown as what it stands for and why it is non-negative, as in the picture:

julia> proof_tree(explain("H(X,Y,Z) <= H(X,Y) + H(Z)"))
H(Z) + H(X,Y) - H(X,Y,Z)  =  I(X,Y;Z)
  ├─ I(X;Z|Y)
  └─ I(Y;Z)

julia> proof_tree(explain("I(X;Z) <= I(X;Y)", "X/Y/Z"))
-H(Z) + H(Y) + H(X,Z) - H(X,Y)
  ├─ C1 = H(Y) - H(X,Y) - H(Z,Y) + H(X,Z,Y)
  │     = -I(X;Z|Y) = 0
  └─ I(X;Y|Z)

chain_rule_tree(vars) -> DecompositionTree
chain_rule_tree(vars, given) -> DecompositionTree

The chain rule for a joint entropy as a tree:

\[H(X_1, \ldots, X_n \mid Y) = H(X_1 \mid Y) + H(X_2, \ldots, X_n \mid X_1, Y)\]

applied again to each remainder, down to the last variable.

julia> chain_rule_tree(["X", "Y", "Z"])
H(X,Y,Z)
  ├─ H(X)
  └─ H(Y,Z|X)
     ├─ H(Y|X)
     └─ H(Z|X,Y)

constraint_graph(lines...) -> VariableGraph

The structural constraints of a problem as a graph over its variables: a Markov chain becomes a path, mutual independence a set of undirected links, and a functional dependence an arrow from each argument to the variable it determines.

Constraints written as general relations (I(X;Y|Z) = 0 and the like) have no natural edge and are left out, as is the statement being proven.

julia> g = constraint_graph("I(W;Z) <= I(X;Y)", "W/X/Y/Z");

julia> g.names
4-element Vector{String}:
 "W"
 "Z"
 "X"
 "Y"

julia> g.edges
3-element Vector{Tuple{Int64, Int64, Symbol, String}}:
 (1, 3, :markov, "W/X/Y/Z")
 (3, 4, :markov, "W/X/Y/Z")
 (4, 2, :markov, "W/X/Y/Z")

entropy_table(c::Counterexample) -> Vector{Pair{String,Coef}}

The entropy values of a counterexample, as "H(X,Y)" => value pairs ordered by how many variables each subset holds.

The values are entropies in bits, so they are bounded by the logarithm of the alphabet size rather than by 1 — H(X) = 6 is a variable with up to 64 equally likely values. When the counterexample is a direction (c.direction), the scale is free as well: every positive multiple of the values fails in the same way, and small integers are simply the most readable representative.

julia> entropy_table(only(explain("H(X) <= H(Y)").certificates))
3-element Vector{Pair{String, Rational{BigInt}}}:
   "H(X)" => 5
   "H(Y)" => 4
 "H(X,Y)" => 7

sufficient_conditions(lines...; maxsize=2, limit=6, budget=4000) -> Conditions

Find assumptions under which a statement that is not provable becomes provable. Each candidate assumption sets one elemental quantity to zero — an independence, a conditional independence, or a functional dependence — and the search reports the smallest sets that work, leaving out any set that merely extends one already found.

The statement must not already be provable; explain it first if you are not sure.

julia> conditions = sufficient_conditions("I(X;Y|Z) <= I(X;Y)");

julia> [only(c.constraints) for c in conditions.found]
3-element Vector{String}:
 "I(X;Y|Z) = 0"
 "I(X;Z|Y) = 0"
 "I(Y;Z|X) = 0"

Conditioning can raise mutual information, so that statement is not provable; it becomes provable as soon as any one of the three variables is conditionally independent of another, the second and third of those being the Markov chains X/Y/Z and Y/X/Z.

maxsize is how many assumptions may be combined, limit how many sets to report, and budget a cap on how many statements are proven along the way, which matters for many variables: the number of candidates is the number of elemental inequalities, n + binomial(n,2) * 2^(n-2).

The result of sufficient_conditions: the minimal sets of assumptions found, and how far the search went.

One set of assumptions that makes a statement provable, with the constraint text to feed back to prove and what each one means.

DecompositionTree

A decomposition of an information expression, as a tree of TreeNodes. nodes[root] is the expression that was decomposed.

TreeNode

A node of a DecompositionTree: label is the short form shown in the picture, detail the entropy form behind it (may be empty), kind is one of :expression, :term, :constraint, :remainder or :constant, and children indexes into the tree's nodes.

VariableGraph

The variables of a problem and how its constraints tie them together; edges carries (src, dst, kind, label) with kind one of :markov, :independent or :function.

plot_proof_tree(x; kwargs...) -> Figure

Draw the derivation behind a proof as a hierarchical tree, with the expression at the root, the non-negative terms branching off to one side and the remainder carrying on down the other. x may be a Result, a Proof or a DecompositionTree.

plotting needs CairoMakie, GraphMakie and Graphs:

using CairoMakie, GraphMakie, Graphs, Xitip

Keywords: detail=true shows the entropy form under each label, size=(width, height), title.

plot_chain_rule(vars; kwargs...) -> Figure

Draw the chain rule expansion of a joint entropy as a tree; see chain_rule_tree.

plotting needs CairoMakie, GraphMakie and Graphs:

using CairoMakie, GraphMakie, Graphs, Xitip

plot_constraints(lines...; kwargs...) -> Figure

Draw the structural constraints of a problem as a graph over its variables; see constraint_graph.

plotting needs CairoMakie, GraphMakie and Graphs:

using CairoMakie, GraphMakie, Graphs, Xitip

plot_counterexample(x; kwargs...) -> Figure

Draw the entropy values that defeat a statement as a bar chart, grouped by how many variables each subset holds; x may be a Result or a Counterexample. See entropy_table for the numbers.

plotting needs CairoMakie, GraphMakie and Graphs:

using CairoMakie, GraphMakie, Graphs, Xitip

entropy_vector(p) -> Vector{Float64}

The entropy of every non-empty subset of n random variables under the joint distribution p, which is indexed by outcome 0:alphabet^n - 1 written in base alphabet. Entry S of the result is H of the subset whose bitmask is S, in bits.

entropic_samples(n; count=400, alphabet=2, style=:structured, rng, normalize=true)

Entropy vectors of count random distributions over n random variables, as the columns of a matrix. Every column is a point the Shannon cone must contain, since it comes from an actual distribution.

Two ways of drawing the distributions:

• :structured (the default) gives each variable a parent among the earlier ones and a noise level, so a sample runs from one variable being a function of another to the two being independent. This reaches across the cone.
• :random draws the joint distribution outright. Such a distribution is nearly always close to independent, so these samples pile up against the facet where the mutual information vanishes and leave most of the cone empty — which is worth seeing once, and is why it is not the default.
• :cover works backwards, for two variables only: it picks a point of the cone uniformly and builds a distribution with exactly those entropies, through entropic_distribution. This is the only style that covers the cone evenly, since it does not sample distributions at all; alphabet is then whatever the construction needs. Note that this is uniform over the cone, not over anything to do with the distributions: none of the styles makes X or Y uniformly distributed. :uniform is accepted as an older name for it.

With normalize, each column is divided by its joint entropy, which puts the samples on one slice of the cone rather than along the rays through it.

entropic_distribution(h) -> (p, alphabet)

A joint distribution of two random variables whose entropy vector is h, which must satisfy the elemental inequalities. Every such h has one, so the Shannon cone for two variables is exactly the set of entropy vectors of distributions — nothing in the picture of it is unreachable.

The witness is X = (U,V) and Y = (U,W) for independent U, V, W, which gives I(X;Y) = H(U), H(X|Y) = H(V) and H(Y|X) = H(W). The three elemental inequalities say exactly that those three entropies are non-negative, so the construction runs for any point of the cone.

julia> p, alphabet = entropic_distribution([0.8, 0.5, 1.0]);

julia> round.(entropy_vector(p, 2, alphabet); digits=6)
3-element Vector{Float64}:
 0.8
 0.5
 1.0

distribution_families(n; steps=41) -> Vector{Pair{String,Matrix{Float64}}}

Familiar families of distributions over n = 2 or 3 random variables, each as a curve of entropy vectors: the columns of the matrix are the entropy vectors as the family's parameter is swept from one end to the other. Drawing these inside the cone shows that a family is not scattered through it but follows a path, and that the paths land on the cone's faces for structural reasons.

For two variables the families are channels from X to Y, all starting at X = Y when the channel is clean:

• a binary symmetric channel, which keeps X and Y symmetric and so runs down the middle of the slice;
• an erasure channel and a Z channel, which do not, and so bend to one side;
• independent pairs, which lie along the I(X;Y) = 0 edge by definition;
• Y a function of X, which lies along H(Y|X) = 0 for the same reason.

For three variables:

• a Markov chain X → Y → Z, which lies exactly on the facet I(X;Z|Y) = 0, that being what the Markov property says;
• a common cause Y → (X, Z), which lies on I(X;Z|Y) = 0 as well, since it is the same conditional independence;
• Z = X xor Y through a noisy channel, which stays on the far apex however much noise there is.

imeasure(h, names=default_names(n)) -> Vector{Pair{String,Float64}}

The atoms of the I-measure at the entropy vector h: one value per region of the Venn diagram of n random variables, named by the information quantity it is. The atoms sum to the joint entropy, and every one of them is an elemental inequality — except the ones shared by three or more variables, which may be negative.

julia> h = entropy_vector([1,0,0,1,0,1,1,0] ./ 4, 3, 2);   # Z = X xor Y

julia> imeasure(h)
7-element Vector{Pair{String, Float64}}:
 "H(X|Y,Z)" => 0.0
 "H(Y|X,Z)" => 0.0
 "H(Z|X,Y)" => 0.0
 "I(X;Y|Z)" => 1.0
 "I(X;Z|Y)" => 1.0
 "I(Y;Z|X)" => 1.0
 "I(X;Y;Z)" => -1.0

shared_slice(h) -> (b, c) or nothing

The three-variable entropy vector h in the coordinates the cone's shape lives in, normalised. b holds I(X;Y|Z), I(X;Z|Y), I(Y;Z|X) and c holds I(X;Y;Z), all divided by their total, which is the part of H(X,Y,Z) that is not private to one variable. nothing when there is no shared information to speak of, the three variables being independent.

The private atoms H(X|Y,Z), H(Y|X,Z), H(Z|X,Y) are dropped, which loses no shape: each appears in exactly one elemental inequality, saying it is non-negative, so they contribute a free orthant and nothing more.

shared_cone_vertices() -> Vector{Pair{Vector{Float64},String}}

The five vertices of shared_slice's picture of the three-variable Shannon cone, with a distribution sitting on each. In those coordinates the cone is a triangular bipyramid: one apex where all shared information is common to all three variables, an equatorial triangle where I(X;Y;Z) is zero, and a second apex where it is as negative as it can be.

julia> [name for (_, name) in shared_cone_vertices()]
5-element Vector{String}:
 "X = Y = Z"
 "X = Y, Z independent"
 "X = Z, Y independent"
 "Y = Z, X independent"
 "Z = X xor Y"

shared_cone_facets() -> Vector{Pair{Vector{Int},String}}

The six facets of the bipyramid shared_cone_vertices describes, each as the vertices it is spanned by together with the elemental inequality that is tight on it. Every facet of the drawn body is one of the nine elemental inequalities made an equation; the other three, H(X|Y,Z), H(Y|X,Z), H(Z|X,Y) >= 0, are tight everywhere on it, since the slice is what is left after dropping exactly those directions.

julia> [name for (_, name) in shared_cone_facets()]
6-element Vector{String}:
 "I(X;Y|Z) = 0"
 "I(X;Z|Y) = 0"
 "I(Y;Z|X) = 0"
 "I(X;Y) = 0"
 "I(X;Z) = 0"
 "I(Y;Z) = 0"

shared_coefficients(statement, names=default_names(3)) -> (w, private)

Rewrite a statement about three variables as an affine function of the slice coordinates b = (I(X;Y|Z), I(X;Z|Y), I(Y;Z|X)): the statement holds at a point of the slice exactly when w[1] + w[2:4]'b >= 0. private holds the coefficients of the three private atoms H(X|Y,Z), H(Y|X,Z), H(Z|X,Y), which the slice drops.

If those are all non-negative, nothing is lost: raising a private atom only raises the left side, so the statement holds on the whole cone exactly when it holds on the slice. If one is negative the statement already fails by raising that entropy alone, whatever the shared part does.

evaluate(expression, names, h) -> Float64

The value of an information expression at the entropy vector h, whose entry S is the entropy of the subset with bitmask S.

julia> evaluate("I(X;Y)", ["X", "Y"], [1.0, 1.0, 2.0])   # independent bits
0.0

cone_rays(n) -> Vector{Pair{Vector{Int},String}}

The extreme rays of the Shannon cone, with what each one is, for the cases small enough to write down: one variable, where the cone is a half line, and two, where it is spanned by three rays.

julia> cone_rays(2)
3-element Vector{Pair{Vector{Int64}, String}}:
 [1, 0, 1] => "Y constant"
 [0, 1, 1] => "X constant"
 [1, 1, 1] => "X = Y"

plot_entropy_cone(; kwargs...) -> Figure

Draw the Shannon cone for n random variables, n being 2 or 3.

For two variables it lives in the three dimensions (H(X), H(Y), H(X,Y)): three facets, one per elemental inequality, meeting along three extreme rays — X constant, Y constant and X = Y.

The cone is infinite, since the inequalities are homogeneous, so the drawing truncates it at H(X,Y) = reach. A second panel shows that same slice head on, where the cone is a triangle with the rays as its corners; this is usually the easier of the two to read.

plotting needs CairoMakie, GraphMakie and Graphs:

using CairoMakie, GraphMakie, Graphs, Xitip

For three variables the cone lives in seven dimensions, but only four of them carry any shape: written in the atoms of the I-measure, the nine elemental inequalities are H(X|Y,Z), H(Y|X,Z), H(Z|X,Y) >= 0, which involve nothing else, together with I(X;Y|Z), I(X;Z|Y), I(Y;Z|X) >= 0 and I(X;Y) , I(X;Z), I(Y;Z) >= 0. Dropping the three private atoms and normalising leaves a three-dimensional body, and that body is a triangular bipyramid — drawn exactly, with a distribution named at each of its five vertices. Its equator is I(X;Y;Z) = 0, so the lower half is precisely where three-way mutual information is negative. See shared_slice and shared_cone_vertices.

Each of its six facets is one of the six elemental inequalities that survive, made an equation, and they are labelled as such. A statement about three variables is a half space, so cut draws where its boundary meets the body: the statement is provable exactly when no vertex of the body falls outside, which the figure marks. See shared_cone_facets and shared_coefficients.

Keywords for three variables: cut is a statement to draw the boundary of, facets labels the facets, plus samples, alphabet, size, fontsize, azimuth, elevation, rng.

Keywords for two variables: samples scatters that many entropy vectors of random distributions inside the cone, outside marks a point that breaks one of the inequalities and shows where it lands on the slice, style is how the samples are drawn (see entropic_samples; :uniform covers the cone evenly), slice draws the second panel, azimuth and elevation rotate the cone, reach is where it is cut off, plus alphabet, size and fontsize.

plot_imeasure(h; kwargs...) -> Figure

Draw the I-measure of two or three random variables as a Venn diagram with every region carrying its value. h is an entropy vector, or a Result whose counterexample supplies one. A negative region is drawn in red: those are the ones no elemental inequality forbids.

plotting needs CairoMakie, GraphMakie and Graphs:

using CairoMakie, GraphMakie, Graphs, Xitip

Keywords: names, title, size, fontsize.

plot_entropy_space(n; kwargs...) -> Figure

Look at the entropy vectors of n random variables, which live in 2^n - 1 dimensions, by drawing sampled ones in two dimensions.

coordinates gives two information expressions to use as the axes, e.g. ("I(X;Y)", "I(X;Y|Z)"). Prefer this: the axes then mean something, and a statement relating the two is a line you can see the points fall on one side of.

Without it the axes are the two principal directions of the sample, which carry the most spread but are mixtures of all 2^n - 1 entropies and mean nothing on their own. Distance in that picture is not distance in any quantity, and clumps in it are the sampler's dependency structures — one clump per choice of which variable follows which — not features of the cone. For three variables plot_entropy_cone draws the real thing instead.

color names an expression to colour the points by, which shows where in the cloud it turns negative.

plotting needs CairoMakie, GraphMakie and Graphs:

using CairoMakie, GraphMakie, Graphs, Xitip

Invalid input or unsolvable problem (reported to the user, exit code 2).

Syntax error; msg includes the offending line and a location marker.

main(args=ARGS; out=stdout, err=stderr) -> Int

Run the command line interface and return the exit code; see Xitip.USAGE. The streams can be redirected, which is useful for testing.