41 Boolean Analysis — Restriction
41.1 Overview
This module sets up the basic machinery for the switching lemma: restrictions of Boolean variables, their effect on literals, terms and DNF formulas, the restricted Boolean function, the notion of a bad restriction, and a collection of small auxiliary lemmas about list operations and decision-tree depth used in the main argument.
41.2 Declarations
A restriction on \(n\) variables is a map \(\rho : \mathrm{Fin}\, n \to \mathrm{Option}\, \mathrm{Bool}\), assigning each variable either a fixed Boolean value or leaving it free (none).
The set of free variables of a restriction \(\rho \) is the finite set of indices \(i \in \mathrm{Fin}\, n\) for which \(\rho (i)\) is unset (none).
The number of free variables of a restriction \(\rho \) is the cardinality of its set of free variables.
Given a restriction \(\rho \) and a point \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\), the extension \(\rho .\mathrm{extend}\, x\) is the Boolean assignment that uses the fixed value \(\rho (i)\) where it is set and falls back to \(x(i)\) on the free variables.
Given a list of (variable, value) pairs, \(\mathrm{fixVars}\) updates the restriction so that each listed variable is set to the corresponding fixed Boolean value.
Given a list of (variable, value) pairs, \(\mathrm{unfixVars}\) resets each listed variable to none, restoring it to a free variable.
The predicate \(\mathrm{IsRestriction}\, s\, \rho \) holds when the restriction \(\rho \) has exactly \(s\) free variables.
A literal \(l\) is killed by \(\rho \) when \(\rho \) fixes its variable to the value that makes \(l\) false; concretely \(\rho (l.\mathrm{var}) = \mathrm{some}\, l.\mathrm{neg}\).
A literal \(l\) is fixed by \(\rho \) when \(\rho \) fixes its variable to the value that makes \(l\) true; concretely \(\rho (l.\mathrm{var}) = \mathrm{some}\, (\lnot \, l.\mathrm{neg})\).
A term (conjunction of literals) is killed by \(\rho \) when at least one of its literals is killed by \(\rho \), forcing the whole term to evaluate to false.
A term is fixed by \(\rho \) when every one of its literals is fixed by \(\rho \), forcing the whole term to evaluate to true.
A term \(t\) is alive under \(\rho \) when it is neither killed nor fixed by \(\rho \).
Given \(f : (\mathrm{Fin}\, n \to \mathrm{Bool}) \to \mathrm{Bool}\) and a restriction \(\rho \), the restricted function maps \(x\) to \(f(\rho .\mathrm{extend}\, x)\), i.e. \(f\) evaluated on the free coordinates with the fixed coordinates set by \(\rho \).
A restriction \(\rho \) is bad for \(f\) at depth \(d\) when the restricted function \(\mathrm{restrictFn}\, f\, \rho \) has decision-tree depth strictly greater than \(d\).
The number of restrictions on \(n\) variables leaving exactly \(s\) free, namely \(\binom {n}{s}\, 2^{\, n-s}\).
If a literal \(l\) is killed by \(\rho \), then for every \(x\) it evaluates to false on the extended point: \(l.\mathrm{eval}(\rho .\mathrm{extend}\, x) = \mathrm{false}\).
If a literal \(l\) is fixed by \(\rho \), then for every \(x\) it evaluates to true on the extended point: \(l.\mathrm{eval}(\rho .\mathrm{extend}\, x) = \mathrm{true}\).
If a decision tree \(T\) of depth at most \(d\) computes \(f\) (i.e. \(T.\mathrm{eval}\, x = f(x)\) for all \(x\)), then the decision-tree depth of \(f\) is at most \(d\).
If a Boolean predicate \(p\) is false on every element of a list \(l\), then \(l.\mathrm{any}\, p\) is false.
If some element \(a\) of a list \(l\) satisfies \(p(a) = \mathrm{false}\), then \(l.\mathrm{all}\, p\) is false.
If some term of a DNF \(f\) is fixed by \(\rho \), then the restricted function \(\mathrm{restrictFn}\, f.\mathrm{eval}\, \rho \) is identically true and hence has decision-tree depth \(0\).
If every term of a DNF \(f\) is killed by \(\rho \), then the restricted function \(\mathrm{restrictFn}\, f.\mathrm{eval}\, \rho \) is identically false and hence has decision-tree depth \(0\).
If a term \(t\) is killed by \(\rho \) and a restriction \(\sigma \) agrees with \(\rho \) on every non-free variable (i.e. \(\sigma (v) = \rho (v)\) whenever \(\rho (v) \neq \mathrm{none}\)), then \(t\) is also killed by \(\sigma \).
Suppose \(t\) is the first term of \(f\) not killed by \(\rho \), that \(\sigma \) agrees with \(\rho \) on all non-free variables, and that \(t\) is not killed by \(\sigma \). Then \(t\) is also the first term of \(f\) not killed by \(\sigma \).
Every term \(t\) belonging to a DNF \(f\) has length at most the width of \(f\).
Searching the indexed list \(l.\mathrm{zipIdx}\) with a predicate and projecting onto the first component agrees with the corresponding \(\mathrm{find?}\) on \(l\).
If \((l, \mathit{idx}) \in t.\mathrm{zipIdx}\), then dropping \(\mathit{idx}\) elements from \(t\) yields a list starting with \(l\), i.e. \(t.\mathrm{drop}\, \mathit{idx} = l :: \mathit{rest}\) for some remaining tail.
If \((l, \mathit{idx})\) arises from filtering \(t.\mathrm{zipIdx}\) by a predicate and \(t\) has length at most \(w\), then \(\mathit{idx} \lt w\).