text:
\section{Introduction}
Boolean functions are wide-spread in mathematics and computer science and can describe yes-no voter systems, hardware circuits, and predicates \citep{o2014analysis}.
A Boolean function is a function from \ensuremath{\Varid{n}} bits to one bit, for example majority (\ensuremath{\Varid{maj}_{\Varid{n}}}), which returns the value that has majority among the \ensuremath{\Varid{n}} inputs for odd \ensuremath{\Varid{n}}.
We are interested in the cost of evaluating Boolean functions: in the context of vote-counting after an election the cost is the number of votes we need to count before we know the outcome for certain.

\subsection{Vote counting example}
In US elections a presidential candidate can lose even if they win the popular vote.
One reason for this is that the outcome is not directly determined by the majority, but rather majority iterated two times.%
\footnote{The actual presidential election is a direct majority vote among the electors who are not formally bound by their state's outcome.}
Our running example is a very much simplified case: consider 3 states with 3 voters in each.
\[\majbrace{\majbrace{\val{(1,1)}}{\val{(1,2)}}{\val{(1,3)}}{m_1 = \ensuremath{\Varid{maj}_{3}\;(\mathbin{...})}}}
    {\majbrace{\val{(2,1)}}{\val{(2,2)}}{\val{(2,3)}}{m_2 = \ensuremath{\Varid{maj}_{3}\;(\mathbin{...})}}}
    {\majbrace{\val{(3,1)}}{\val{(3,2)}}{\val{(3,3)}}{m_3 = \ensuremath{\Varid{maj}_{3}\;(\mathbin{...})}}}{\ensuremath{\Varid{maj}_{3}}(m_1,m_2,m_3)}
\]
We first compute the majority in each ``state'' of three bits, and then the majority of $m_1$, $m_2$, and $m_3$.
For example we see here $\ensuremath{\mathbf{0}},\ensuremath{\mathbf{1}},\ensuremath{\mathbf{0}}$ which gives $m_1 =  \ensuremath{\mathbf{0}}$, then $\ensuremath{\mathbf{1}},\ensuremath{\mathbf{0}},\ensuremath{\mathbf{1}}$ which gives $m_2 = \ensuremath{\mathbf{1}}$, and $\ensuremath{\mathbf{0}},\ensuremath{\mathbf{1}},\ensuremath{\mathbf{0}}$ again which gives $m_3 = \ensuremath{\mathbf{0}}$.
The final majority is \ensuremath{\mathbf{0}}:
\[\majbrace{\majbrace{\ensuremath{\mathbf{0}}}{\ensuremath{\mathbf{1}}}{\ensuremath{\mathbf{0}}}{m_1 = \ensuremath{\mathbf{0}}}}
    {\majbrace{\ensuremath{\mathbf{1}}}{\ensuremath{\mathbf{0}}}{\ensuremath{\mathbf{1}}}{m_2 = \ensuremath{\mathbf{1}}}}
    {\majbrace{\ensuremath{\mathbf{0}}}{\ensuremath{\mathbf{1}}}{\ensuremath{\mathbf{0}}}{m_3 = \ensuremath{\mathbf{0}}}}{\ensuremath{\Varid{maj}_{3}} = \ensuremath{\mathbf{0}}}
\]
\noindent
But if we switch the first and 8th bit (perhaps through
gerrymandering) we get another example with the changed bits marked
in red:
\[\majbrace{\majbrace{\textcolor{red}{\ensuremath{\mathbf{1}}}}{\ensuremath{\mathbf{1}}}{\ensuremath{\mathbf{0}}}{m_1 = \textcolor{red}{\ensuremath{\mathbf{1}}}}}
    {\majbrace{\ensuremath{\mathbf{1}}}{\ensuremath{\mathbf{0}}}{\ensuremath{\mathbf{1}}}{m_2 = \ensuremath{\mathbf{1}}}}
    {\majbrace{\ensuremath{\mathbf{0}}}{\textcolor{red}{\ensuremath{\mathbf{0}}}}{\ensuremath{\mathbf{0}}}{m_3 = \ensuremath{\mathbf{0}}}}{\ensuremath{\Varid{maj}_{3}} = \textcolor{red}{\ensuremath{\mathbf{1}}}}
\]
This changes $m_1$ from \ensuremath{\mathbf{0}}{} to \ensuremath{\mathbf{1}}{} without affecting $m_2$, or $m_3$.
But now the two-level majority is changed to \ensuremath{\mathbf{1}}, just from the switch of two bits.
Both examples have four \ensuremath{\mathbf{1}}{}'s  and five \ensuremath{\mathbf{0}}{}'s  but the result is different based on the positioning of the bits.
In our case the two-level majority is \ensuremath{\mathbf{1}}{} even though there are fewer \ensuremath{\mathbf{1}}{}'s  than \ensuremath{\mathbf{0}}{}'s.
This means that the \ensuremath{\mathbf{0}}{}'s ``lose'' even though they won the ``popular vote''.

\subsection{Related work}
We use binary decision trees to describe the evaluation order of Boolean functions.
The depth of the decision tree corresponds to the number of votes needed to know the outcome for certain.
This is called deterministic complexity.
Another well-known notion is randomized complexity, and the complexity bounds of iterated majority have been studied in \cite{landau2006lower}, \cite{leonardos2013improved} and \cite{magniez2016improved}.
Iterated majority on two levels corresponds to the Boolean function for US elections as described above, and we are particularly interested in this function.

Other relevant concepts are certificate complexity, degree of a Boolean function, and communication complexity \citep{buhrman2002complexity}.
Complexity measures related specifically to circuits are circuit complexity, additive, and multiplicative complexity \citep{wegener1987complexity}.
Thus, there are many competing complexity measures but we focus on level-\ensuremath{\Varid{p}}-complexity --- a function of the probability that a bit is 1 \citep{garban2014noise}.
Level-\ensuremath{\Varid{p}}-complexity is more complicated than deterministic complexity but is easier to compute than other more general complexity measures like full randomized complexity.
Moreover, level-\ensuremath{\Varid{p}}-complexity has many interesting properties, as can be seen in \citep{jansson2022level}.
This paper presents a purely functional library for computing level-\ensuremath{\Varid{p}}-complexity of Boolean functions in general, and for two-level iterated three-bit majority in particular.
The implementation is in Haskell but should work also in other languages.
\subsection{Motivation}
\begin{figure}[tbp]
        \centering
\begin{tikzpicture}
\node at (0,0){\includegraphics[width=0.7\textwidth]{plots/4polys.pdf}};
\node at (-0.5,-0.5){%
  \begin{minipage}{0.3\textwidth}%
    \tiny
    \begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{7}{@{}>{\hspre}l<{\hspost}@{}}%
\column{9}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[7]{}\Varid{sim}_{5}\;[\mskip1.5mu \Varid{x}_{1},\Varid{x}_{2},\Varid{x}_{3},\Varid{x}_{4},\Varid{x}_{5}\mskip1.5mu]\mathrel{=}{}\<[E]%
\\
\>[7]{}\hsindent{2}{}\<[9]%
\>[9]{}\neg \;(\Varid{same}\;[\mskip1.5mu \Varid{x}_{1},\Varid{x}_{2},\Varid{x}_{3}\mskip1.5mu]){}\<[E]%
\\
\>[7]{}\hsindent{2}{}\<[9]%
\>[9]{}\mathrel{\vee}\Varid{same}\;[\mskip1.5mu \Varid{x}_{4},\Varid{x}_{5}\mskip1.5mu]{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
  \end{minipage}
};
\end{tikzpicture}
        \caption{The four polynomials computed by \ensuremath{\Varid{genAlgThinMemo}\;\mathrm{5}\;\Varid{sim}_{5}}.}
        \label{fig:4polys}
\end{figure}
To get a feeling for what the end result will look like we start with two examples which will be explained in detail later: the level-\ensuremath{\Varid{p}}-complexity of 2-level iterated majority \ensuremath{\Varid{maj}_{3}^2} and of a 5-bit function we call \ensuremath{\Varid{sim}_{5}}, defined in Fig.~\ref{fig:4polys}\footnote{The function \ensuremath{\Varid{sim}_{5}} is referred to as $f_{\!AC}$ in \citep{jansson2022level}.}.
The complexity is a piecewise polynomial function of the probability \ensuremath{\Varid{p}} and \ensuremath{\Varid{sim}_{5}} is the smallest arity Boolean function we have found which has more than one polynomial piece contributing to the complexity.
Polynomials are represented by their coefficients: for example, \ensuremath{\Conid{P}\;[\mskip1.5mu \mathrm{5},\mathbin{-}\mathrm{8},\mathrm{8}\mskip1.5mu]} represents \(5-8x+8x^2\).
The function \ensuremath{\Varid{genAlgThinMemo}} uses thinning and memoization to generate a set of minimal cost polynomials.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{11}{@{}>{\hspre}l<{\hspost}@{}}%
\column{25}{@{}>{\hspre}l<{\hspost}@{}}%
\column{30}{@{}>{\hspre}l<{\hspost}@{}}%
\column{31}{@{}>{\hspre}l<{\hspost}@{}}%
\column{49}{@{}>{\hspre}l<{\hspost}@{}}%
\column{67}{@{}>{\hspre}c<{\hspost}@{}}%
\column{67E}{@{}l@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\Varid{ps5}\mathrel{=}\Varid{genAlgThinMemo}\;\mathrm{5}\;{}\<[25]%
\>[25]{}\Varid{sim}_{5}{}\<[31]%
\>[31]{}\mathbin{::}\Conid{Set}\;(\Conid{Poly}\;\mathbb{Q}){}\<[E]%
\\
\>[B]{}\Varid{check5}\mathrel{=}{}\<[11]%
\>[11]{}\Varid{ps5}\doubleequals\Varid{fromList}\;[\mskip1.5mu {}\<[30]%
\>[30]{}\Conid{P}\;[\mskip1.5mu \mathrm{2},\mathrm{6},\mathbin{-}\mathrm{10},\mathrm{8},\mathbin{-}\mathrm{4}\mskip1.5mu],{}\<[49]%
\>[49]{}\Conid{P}\;[\mskip1.5mu \mathrm{4},\mathbin{-}\mathrm{2},\mathbin{-}\mathrm{3},\mathrm{8},\mathbin{-}\mathrm{2}\mskip1.5mu],{}\<[E]%
\\
\>[30]{}\Conid{P}\;[\mskip1.5mu \mathrm{5},\mathbin{-}\mathrm{8},\mathrm{9},\mathrm{0},\mathbin{-}\mathrm{2}\mskip1.5mu],{}\<[49]%
\>[49]{}\Conid{P}\;[\mskip1.5mu \mathrm{5},\mathbin{-}\mathrm{8},\mathrm{8}\mskip1.5mu]{}\<[67]%
\>[67]{}\mskip1.5mu]{}\<[67E]%
\ColumnHook
\end{hscode}\resethooks
The graph, in Fig.~\ref{fig:4polys}, shows that different polynomials dominate in different intervals.
\ensuremath{\Conid{P}_{1}} is best near the end-points, but \ensuremath{\Conid{P}_{4}} is best near \ensuremath{\Varid{p}\mathrel{=}\mathrm{1}\mathbin{/}\mathrm{2}} (despite being really bad near the endpoints).
The level-\ensuremath{\Varid{p}}-complexity is the piecewise polynomial minimum, a combination of \ensuremath{\Conid{P}_{1}} and \ensuremath{\Conid{P}_{4}}.
This computation can be done by exhaustive search over the \ensuremath{\mathrm{54192}} different decision trees and \ensuremath{\mathrm{39}} resulting polynomials, but for more complex Boolean functions the doubly exponential growth makes that impractical.

For our running example, \ensuremath{\Varid{maj}_{3}^2}, a crude estimate indicates we would have $10^{111}$ decision trees to search and very many polynomials.
Thus the computation would be intractable if it were not for the combination of thinning, memoization, and symbolic comparison of polynomials.
Thanks to symmetries in the problem there turns out to be just one dominating polynomial:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{11}{@{}>{\hspre}l<{\hspost}@{}}%
\column{25}{@{}>{\hspre}l<{\hspost}@{}}%
\column{30}{@{}>{\hspre}l<{\hspost}@{}}%
\column{31}{@{}>{\hspre}l<{\hspost}@{}}%
\column{60}{@{}>{\hspre}c<{\hspost}@{}}%
\column{60E}{@{}l@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\Varid{ps9}\mathrel{=}\Varid{genAlgThinMemo}\;\mathrm{9}\;{}\<[25]%
\>[25]{}\Varid{maj}_{3}^2{}\<[31]%
\>[31]{}\mathbin{::}\Conid{Set}\;(\Conid{Poly}\;\mathbb{Q}){}\<[E]%
\\
\>[B]{}\Varid{check9}\mathrel{=}{}\<[11]%
\>[11]{}\Varid{ps9}\doubleequals\Varid{fromList}\;[\mskip1.5mu {}\<[30]%
\>[30]{}\Conid{P}\;[\mskip1.5mu \mathrm{4},\mathrm{4},\mathrm{6},\mathrm{9},\mathbin{-}\mathrm{61},\mathrm{23},\mathrm{67},\mathbin{-}\mathrm{64},\mathrm{16}\mskip1.5mu]{}\<[60]%
\>[60]{}\mskip1.5mu]{}\<[60E]%
\ColumnHook
\end{hscode}\resethooks
The graph, shown later in Fig.~\ref{fig:itermajalgs2}, shows that only 4 bits are needed in the limiting cases of \ensuremath{\Varid{p}\mathrel{=}\mathrm{0}} or \ensuremath{\Varid{p}\mathrel{=}\mathrm{1}} and that a bit more than 6 bits are needed in the maximum at \ensuremath{\Varid{p}\mathrel{=}\mathrm{1}\mathbin{/}\mathrm{2}}.

\subsection{Contributions}
\label{sec:aim}
This paper presents a Haskell library for computing level-\ensuremath{\Varid{p}}-complexity of Boolean functions in general, and for \ensuremath{\Varid{maj}_{3}^2} in particular.
The level-\ensuremath{\Varid{p}}-complexity of \ensuremath{\Varid{maj}_{3}^2} was conjectured in \citet{jansson2022level}, but could not be proven because it was hard to generate all possible decision trees.
This paper fills that gap, by showing that the conjecture is false and by computing the true level-\ensuremath{\Varid{p}}-complexity of \ensuremath{\Varid{maj}_{3}^2}.

The strength of our implementation is that it can calculate the level-$p$-complexity for boolean functions quickly and correctly, compared to tedious calculations by hand.
Our specification uses exhaustive search and considers all possible candidates (decision trees).
Some partial candidates dominate (many) others, which may be discarded.
Thinning \citep{bird_gibbons_2020} is an algorithmic design technique which maintains a small set of partial candidates which provably dominate all other candidates.
We hope that one contribution of this paper is an interesting example of how a combination of algorithmic techniques can be used to make the intractable tractable.
The code in this paper is available on GitHub\footnote{The paper repository is at \url{https://github.com/juliajansson/BoFunComplexity}.} and uses packages from \citet{JanssonIonescuBernardyDSLsofMathBook2022}.
\begin{comment}
This paper builds on work from \citet{jansson2022level} where the level-\ensuremath{\Varid{p}}-complexity of some Boolean functions is calculated.
In particular the level-\ensuremath{\Varid{p}}-complexity of iterated three-bit majority on two levels was conjectured in \citet{jansson2022level}, but could not be proven because it was hard to generate all possible decision trees (also called algorithms in \citep{jansson2022level}, \citep{garban2014noise} and \citep{landau2006lower}).\TODO{move also called part to background}
We show that the conjecture is false, and compute the true level-\ensuremath{\Varid{p}}-complexity of two-level three-bit majority.

The executable specification, and naive implementation, simply enumerates all decision trees, computes their cost polynomials, and selects the best.
But as the number of decision trees grows doubly exponentially, we hit a wall very soon.
Fortunately, a combination of thinning, memoization, and symbolic comparison of polynomials makes it possible to compute the best polynomial in under a second!
Our specification uses exhaustive search and considers all possible candidates (decision trees).
Some partial candidates dominate (many) others, which may be discarded.
Thinning \citep{bird_gibbons_2020} is an algorithmic design technique which maintains a small set of partial candidates which provably dominate all other candidates.

Thus this paper fills the gap in \citet{jansson2022level}, by finding a more efficient way to calculate the level-\ensuremath{\Varid{p}}-complexity using memoization and thinning.
The paper also goes more into detail about the implementation than \citet{jansson2022level}, and leaves out some of the theory which is not deemed relevant.
The code in this paper is available on GitHub\footnote{The paper repository is at \url{https://github.com/juliajansson/BoFunComplexity}.} and uses packages from \citet{JanssonIonescuBernardyDSLsofMathBook2022}.
\end{comment}

\section{Background}
\label{sec:Background}
To explain what level-\ensuremath{\Varid{p}}-complexity of Boolean functions means we introduce some background about Boolean functions, decision trees, cost and complexity.

\subsection{Boolean functions}
A Boolean function \ensuremath{\Varid{f}\mathop{:}\mathbb{B}^{\Varid{n}}\,\to\,\mathbb{B}} is a function from \ensuremath{\Varid{n}} Boolean inputs to one Boolean output.
The Boolean input type \ensuremath{\mathbb{B}} could be \ensuremath{\{\mskip1.5mu \Conid{False},\Conid{True}\mskip1.5mu\},\{\mskip1.5mu \Conid{F},\Conid{T}\mskip1.5mu\}} or \ensuremath{\{\mskip1.5mu \mathrm{0},\mathrm{1}\mskip1.5mu\}} and from now on we use \ensuremath{\mathbf{0}}{} for false and \ensuremath{\mathbf{1}}{} for true in our notation.
The easiest example of a Boolean function is the function which is constant \ensuremath{\ensuremath{\mathbf{0}}{}} or constant \ensuremath{\ensuremath{\mathbf{1}}{}}.
The usual logical gates like \ensuremath{\Varid{and}} and \ensuremath{\Varid{or}} are very common Boolean functions.
Another example is the dictator function (also known as first projection), which is defined as \ensuremath{\ensuremath{\Varid{dict}_{\Varid{n}}}\;[\mskip1.5mu \Varid{x}_{1},\mathbin{...},\Varid{x}_n\mskip1.5mu]\mathrel{=}\Varid{x}_{1}} when the dictator is bit~\ensuremath{\mathrm{1}}.

A naive implementation of Boolean functions could be as functions \ensuremath{\Varid{f}\mathop{:}[\mskip1.5mu \mathbb{B}\mskip1.5mu]\,\to\,\mathbb{B}}, but that turns out to be inefficient.
Instead we use Binary Decision Diagrams \ensuremath{\Conid{BDD}}s \citep{Bryant_BDD_1986} as implemented in Masahiro Sakai's excellent Hackage package\footnote{\url{https://github.com/msakai/haskell-decision-diagrams}}.
In the complexity computation, we only need two operations on Boolean functions which we capture in the following type class interface:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{12}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\mathbf{class}\;\Conid{BoFun}\;\Varid{bf}\;\mathbf{where}{}\<[E]%
\\
\>[B]{}\hsindent{3}{}\<[3]%
\>[3]{}\Varid{isConst}{}\<[12]%
\>[12]{}\mathbin{::}\Varid{bf}\,\to\,\Conid{Maybe}\;\mathbb{B}{}\<[E]%
\\
\>[B]{}\hsindent{3}{}\<[3]%
\>[3]{}\Varid{setBit}{}\<[12]%
\>[12]{}\mathbin{::}\Conid{Index}\,\to\,\mathbb{B}\,\to\,\Varid{bf}\,\to\,\Varid{bf}{}\<[E]%
\\[\blanklineskip]%
\>[B]{}\mathbf{type}\;\Conid{Index}\mathrel{=}\mathbb{N}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
The use of a type class here means we keep the interface to the BDD implementation minimal, which makes proofs easier and gives better feedback from the type system.
The first method, \ensuremath{\Varid{isConst}\;\Varid{f}}, returns \ensuremath{\Conid{Just}\;\Varid{b}} iff the function \ensuremath{\Varid{f}} is constant and always returns \ensuremath{\Varid{b}\mathbin{::}\mathbb{B}}.
The second method, \ensuremath{\Varid{setBit}\;\Varid{i}\;\Varid{b}\;\Varid{f}}, restricts a Boolean function (on \ensuremath{\Varid{n}\mathbin{+}\mathrm{1}} bits) by setting its \ensuremath{\Varid{i}}:th bit to \ensuremath{\Varid{b}}.
The result is a ``subfunction'' on the remaining \ensuremath{\Varid{n}} bits, abbreviated $\fixatill{i}{b}{f}$, and illustrated in Figure \ref{fig:subf}.
\begin{figure}[tbp]
  \centering
  \begin{forest}
    for tree =

        minimum height=1ex, text depth = 0.25ex,
       anchor = north,

         edge = {-Stealth},
        s sep = 3em,
        l sep = 2em
                },
    EL/.style =
       before typesetting nodes=
    where n=1{edge label/.wrap value={node[pos=0.5,anchor=east]{#1}}
             {edge label/.wrap value={node[pos=0.5,anchor=west]{#1}}
                                }

    [\ensuremath{\Varid{f}},
        [, edge label = {node[midway,anchor = south] {1}}
            [\ensuremath{\fixatill{\mathrm{1}}{\ensuremath{\mathbf{0}}{}}{\Varid{f}}}, EL = \ensuremath{\ensuremath{\mathbf{0}}{}}]
            [\ensuremath{\fixatill{\mathrm{1}}{\ensuremath{\mathbf{1}}{}}{\Varid{f}}}, EL = \ensuremath{\ensuremath{\mathbf{1}}{}}]
        ]
        [, EL = 2
            [\ensuremath{\fixatill{\mathrm{2}}{\ensuremath{\mathbf{0}}{}}{\Varid{f}}}, EL = \ensuremath{\ensuremath{\mathbf{0}}{}}]
            [\ensuremath{\fixatill{\mathrm{2}}{\ensuremath{\mathbf{1}}{}}{\Varid{f}}}, EL = \ensuremath{\ensuremath{\mathbf{1}}{}}, s sep = 1em
                [, EL = 1, s sep = 1ex
                [$\ldots$, EL = \ensuremath{\ensuremath{\mathbf{0}}{}}]
                    [$\ldots$, EL = \ensuremath{\ensuremath{\mathbf{1}}{}}]
                ]
                [, EL = 2, s sep = 1ex
                [$\ldots$, EL = \ensuremath{\ensuremath{\mathbf{0}}{}}]
                    [$\ldots$, EL = \ensuremath{\ensuremath{\mathbf{1}}{}}]
                ]
                [,no edge,EL = $\ldots$]
                [,no edge, EL = {}]
                [, EL = $n$, s sep = 1ex
                    [$\ldots$, EL = \ensuremath{\ensuremath{\mathbf{0}}{}}]
                    [$\ldots$, EL = \ensuremath{\ensuremath{\mathbf{1}}{}}]
                ]
            ]
        ]
        [,no edge,EL = $\ldots$]
        [,no edge]
        [, edge label = {node[midway,anchor = south]{$n+1$}}
            [\ensuremath{\fixatill{\Varid{n}\mathbin{+}\mathrm{1}}{\ensuremath{\mathbf{0}}{}}{\Varid{f}}}, EL = \ensuremath{\ensuremath{\mathbf{0}}{}}]
            [\ensuremath{\fixatill{\Varid{n}\mathbin{+}\mathrm{1}}{\ensuremath{\mathbf{1}}{}}{\Varid{f}}}, EL = \ensuremath{\ensuremath{\mathbf{1}}{}}]
      ]
    ]
\end{forest}
  \caption{The tree of subfunctions of a Boolean function \ensuremath{\Varid{f}}.
    For brevity \ensuremath{\Varid{setBit}\;\Varid{i}\;\Varid{b}\;\Varid{f}} is denoted \ensuremath{\fixatill{\Varid{i}}{\Varid{b}}{\Varid{f}}}.
    This tree structure is also the call-graph for our generation of decision trees.
    Note that this is related to, but not the same as, the decision trees.}
  \label{fig:subf}
\end{figure}
As an example, for the function \ensuremath{\Varid{and}_{2}} we have that \ensuremath{\Varid{setBit}\;\Varid{i}\;\ensuremath{\mathbf{0}}{}\;\Varid{and}_{2}\mathrel{=}\Varid{const}\;\ensuremath{\mathbf{0}}{}} and \ensuremath{\Varid{setBit}\;\Varid{i}\;\ensuremath{\mathbf{1}}{}\;\Varid{and}_{2}\mathrel{=}\Varid{id}}.

For \ensuremath{\Varid{and}_{2}} we get the same result for \ensuremath{\Varid{i}\mathrel{=}\mathrm{1}}, or \ensuremath{\mathrm{2}} but for the dictator function it depends if we pick the dictator index or not.
We get \ensuremath{\Varid{setBit}\;\mathrm{1}\;\Varid{b}\;\ensuremath{\Varid{dict}_{\Varid{n}\mathbin{+}\mathrm{1}}}\mathrel{=}\ensuremath{\Varid{const}_{\Varid{n}}}\;\Varid{b}}, since the result of the dictator function is already decided.
Otherwise, if \ensuremath{\Varid{i}\not\doubleequals\mathrm{1}}, we get \ensuremath{\Varid{setBit}\;\Varid{i}\;\Varid{b}\;\ensuremath{\Varid{dict}_{\Varid{n}\mathbin{+}\mathrm{1}}}\mathrel{=}\ensuremath{\Varid{dict}_{\Varid{n}}}} irrespective of the value of \ensuremath{\Varid{b}} since only the value of the dictator bit matters.
This behaviour is shown in Figure \ref{fig:dict}.

\begin{figure}[htbp]
  \centering
  \begin{forest}
    for tree =

        minimum height=1ex, text depth = 0.25ex,
       anchor = north,

         edge = {-Stealth},
        s sep = 1em,
        l sep = 2em
                },
    EL/.style =
       before typesetting nodes=
    where n=1{edge label/.wrap value={node[pos=0.5,anchor=east]{#1}}
             {edge label/.wrap value={node[pos=0.5,anchor=west]{#1}}
                                }

    [\ensuremath{\ensuremath{\Varid{dict}_{\Varid{n}\mathbin{+}\mathrm{1}}}},
        [, edge label = {node[midway,anchor = south] {1}}
            [\ensuremath{\ensuremath{\Varid{const}_{\Varid{n}}}\;\ensuremath{\mathbf{0}}{}}, EL = \ensuremath{\ensuremath{\mathbf{0}}{}}]
            [\ensuremath{\ensuremath{\Varid{const}_{\Varid{n}}}\;\ensuremath{\mathbf{1}}{}}, EL = \ensuremath{\ensuremath{\mathbf{1}}{}}]
        ]
        [, EL = 2
            [\ensuremath{\ensuremath{\Varid{dict}_{\Varid{n}}}}, EL = \ensuremath{\ensuremath{\mathbf{0}}{}}]
            [\ensuremath{\ensuremath{\Varid{dict}_{\Varid{n}}}}, EL = \ensuremath{\ensuremath{\mathbf{1}}{}}]
        ]
        [,no edge,EL = $\ldots$]
        [,no edge]
        [, edge label = {node[midway,anchor = south]{$n+1$}}
            [\ensuremath{\ensuremath{\Varid{dict}_{\Varid{n}}}}, EL = \ensuremath{\ensuremath{\mathbf{0}}{}}]
            [\ensuremath{\ensuremath{\Varid{dict}_{\Varid{n}}}}, EL = \ensuremath{\ensuremath{\mathbf{1}}{}}]
      ]
    ]
\end{forest}
  \caption{The tree of subfunctions of the \ensuremath{\ensuremath{\Varid{dict}_{\Varid{n}\mathbin{+}\mathrm{1}}}} function.}
  \label{fig:dict}
\end{figure}

\subsection{Decision trees}
Consider a decision tree that picks the \ensuremath{\Varid{n}} bits of a Boolean function \ensuremath{\Varid{f}} in a deterministic way depending on the values of the bits picked further up the tree.
Decision trees are referred to as algorithms in \citep{jansson2022level}, \citep{garban2014noise} and \citep{landau2006lower}.
Given a natural number \ensuremath{\Varid{n}} and a Boolean function \ensuremath{\Varid{f}}, a decision tree \ensuremath{\Varid{t}} describes one way to evaluate the function \ensuremath{\Varid{f}}.
The Haskell datatype is as follows:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\mathbf{data}\;\Conid{DecTree}\mathrel{=}\Conid{Res}\;\mathbb{B}\mid \Conid{Pick}\;\Conid{Index}\;\Conid{DecTree}\;\Conid{DecTree}{}\<[E]%
\\
\>[B]{}\hsindent{3}{}\<[3]%
\>[3]{}\mathbf{deriving}\;(\Conid{Eq},\Conid{Ord},\Conid{Show}){}\<[E]%
\ColumnHook
\end{hscode}\resethooks
Parts of the ``rules of the game'' in the mathematical literature is that you must return a \ensuremath{\Conid{Res}}ult if the function is constant and you may only \ensuremath{\Conid{Pick}} an index once.
We can capture most of these rules with a type family version of the \ensuremath{\Conid{DecTree}} datatype (here expressed in \ensuremath{\Conid{Agda}} syntax).
Here we use two type indices: \ensuremath{\Varid{t}\mathop{:}\Conid{DecTree}\;\Varid{n}\;\Varid{f}} is a decision tree for the Boolean function \ensuremath{\Varid{f}}, of arity \ensuremath{\Varid{n}}.
The \ensuremath{\Conid{Res}} constructor may only be used for constant functions (but for any arity), while \ensuremath{\Conid{Pick}\;\Varid{i}} takes two subtrees for Boolean functions of arity \ensuremath{\Varid{n}} to a tree of arity \ensuremath{\Varid{suc}\;\Varid{n}\mathrel{=}\Varid{n}\mathbin{+}\mathrm{1}}.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{9}{@{}>{\hspre}c<{\hspost}@{}}%
\column{9E}{@{}l@{}}%
\column{12}{@{}>{\hspre}l<{\hspost}@{}}%
\column{15}{@{}>{\hspre}c<{\hspost}@{}}%
\column{15E}{@{}l@{}}%
\column{18}{@{}>{\hspre}l<{\hspost}@{}}%
\column{40}{@{}>{\hspre}l<{\hspost}@{}}%
\column{62}{@{}>{\hspre}l<{\hspost}@{}}%
\column{88}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\mathbf{data}\;\Conid{DecTree}{}\<[15]%
\>[15]{}\mathop{:}{}\<[15E]%
\>[18]{}(\Varid{n}\mathop{:}\mathbb{N})\,\to\,(\Varid{f}\mathop{:}\Conid{BoolFun}\;\Varid{n})\,\to\,\Conid{Set}\;\mathbf{where}{}\<[E]%
\\
\>[B]{}\hsindent{3}{}\<[3]%
\>[3]{}\Conid{Res}{}\<[9]%
\>[9]{}\mathop{:}{}\<[9E]%
\>[40]{}(\Varid{b}\mathop{:}\mathbb{B})\,\to\,{}\<[62]%
\>[62]{}\Conid{DecTree}\;\Varid{n}\;(\ensuremath{\Varid{const}_{\Varid{n}}}\;\Varid{b}){}\<[E]%
\\
\>[B]{}\hsindent{3}{}\<[3]%
\>[3]{}\Conid{Pick}{}\<[9]%
\>[9]{}\mathop{:}{}\<[9E]%
\>[12]{}\{\mskip1.5mu \Varid{f}\mathop{:}\Conid{BoolFun}\;(\Varid{suc}\;\Varid{n})\mskip1.5mu\}\,\to\,{}\<[40]%
\>[40]{}(\Varid{i}\mathop{:}\Conid{Fin}\;(\Varid{suc}\;\Varid{n}))\,\to\,{}\<[62]%
\>[62]{}\Conid{DecTree}\;\Varid{n}\;(\Varid{setBit}\;\Varid{i}\;\ensuremath{\mathbf{0}}{}\;\Varid{f})\,\to\,{}\<[E]%
\\
\>[62]{}\Conid{DecTree}\;\Varid{n}\;(\Varid{setBit}\;\Varid{i}\;\ensuremath{\mathbf{1}}{}\;{}\<[88]%
\>[88]{}\Varid{f})\,\to\,{}\<[E]%
\\
\>[62]{}\Conid{DecTree}\;(\Varid{suc}\;\Varid{n})\;\Varid{f}{}\<[E]%
\\[\blanklineskip]%
\>[B]{}\Varid{setBit}\mathop{:}\Conid{Fin}\;(\Varid{suc}\;\Varid{n})\,\to\,\mathbb{B}\,\to\,\Conid{BoolFun}\;(\Varid{suc}\;\Varid{n})\,\to\,\Conid{BoolFun}\;\Varid{n}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
Note that the dependently type version of \ensuremath{\Varid{setBit}} clearly indicates that the resulting function \ensuremath{\Varid{g}\mathrel{=}(\Varid{setBit}\;\Varid{i}\;\Varid{b}\;\Varid{f})\mathop{:}\Conid{BoolFun}\;\Varid{n}} has arity one less that of \ensuremath{\Varid{f}\mathop{:}\Conid{BoolFun}\;(\Varid{suc}\;\Varid{n})}.
This helps maintaining the invariant that each input bit may only be picked once.
We use the Haskell versions, but the Agda versions capture the invariants better.

We can use these rules backwards to generate all possible decision trees for a certain function.
If the function is constant, returning \ensuremath{\Varid{b}\mathop{:}\mathbb{B}}, we immediately know that the only decision tree allowed is \ensuremath{\Conid{Res}\;\Varid{b}}.
If it is not constant, we pick any index \ensuremath{\Varid{i}}, any decision tree \ensuremath{\Varid{t}_{0}} for the subfunction \ensuremath{\Varid{setBit}\;\Varid{i}\;\ensuremath{\mathbf{0}}{}\;\Varid{f}} and \ensuremath{\Varid{t}_{1}} for the subfunction \ensuremath{\Varid{setBit}\;\Varid{i}\;\ensuremath{\mathbf{1}}{}\;\Varid{f}} recursively.

\begin{figure}[htbp]
  \centering

\begin{forest}
    for tree =

        draw, rounded corners,
        top color=white, bottom color=blue!20,
        font = \ttfamily,
        minimum height=1ex, text depth = 0.25ex,
       anchor = north,

         edge = {-Stealth},
        s sep = 2em,
        l sep = 2em
                },
    EL/.style =
       before typesetting nodes=
    where n=1{edge label/.wrap value={node[pos=0.5,anchor=east]{#1}}
             {edge label/.wrap value={node[pos=0.5,anchor=west]{#1}}
                                }

    [$x_1$, root
        [$x_3$, EL=\ensuremath{\mathbf{0}}
          [\ensuremath{\mathbf{0}}, EL=\ensuremath{\mathbf{0}}, sharp corners]
          [$x_2$, EL=\ensuremath{\mathbf{1}}
              [\ensuremath{\mathbf{0}}, EL=\ensuremath{\mathbf{0}}, sharp corners]
              [\ensuremath{\mathbf{1}}, EL=\ensuremath{\mathbf{1}}, sharp corners]]]
        [$x_2$, EL=\ensuremath{\mathbf{1}}
            [$x_3$, EL=\ensuremath{\mathbf{0}}
              [\ensuremath{\mathbf{0}}, EL=\ensuremath{\mathbf{0}}, sharp corners]
              [\ensuremath{\mathbf{1}}, EL=\ensuremath{\mathbf{1}}, sharp corners]]
            [\ensuremath{\mathbf{1}}, EL=\ensuremath{\mathbf{1}}, sharp corners]]
    ]
\end{forest}

  \caption{An example of a decision tree for \ensuremath{\Varid{maj}_{3}}.
    %
    The root node branches on the value of bit 1.
    %
    If it is \ensuremath{\mathbf{0}}{}, it picks bit 3, while if it is \ensuremath{\mathbf{1}}{}, it picks bit 2.
    %
    It then picks the last remaining bit if necessary.
  }
  \label{fig:Algex}
\end{figure}
An example of a decision tree for the majority function \ensuremath{\Varid{maj}_{3}} on three bits
is defined by the expression \ensuremath{\Varid{ex1}} visualised in Figure~\ref{fig:Algex}.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{15}{@{}>{\hspre}l<{\hspost}@{}}%
\column{36}{@{}>{\hspre}l<{\hspost}@{}}%
\column{56}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\Varid{ex1}\mathrel{=}\Conid{Pick}\;\mathrm{1}\;{}\<[15]%
\>[15]{}(\Conid{Pick}\;\mathrm{3}\;(\Conid{Res}\;\ensuremath{\mathbf{0}}{})\;{}\<[36]%
\>[36]{}(\Conid{Pick}\;\mathrm{2}\;(\Conid{Res}\;\ensuremath{\mathbf{0}}{})\;(\Conid{Res}\;\ensuremath{\mathbf{1}}{})))\;{}\<[E]%
\\
\>[15]{}(\Conid{Pick}\;\mathrm{2}\;(\Conid{Pick}\;\mathrm{3}\;(\Conid{Res}\;\ensuremath{\mathbf{0}}{})\;(\Conid{Res}\;\ensuremath{\mathbf{1}}{}))\;{}\<[56]%
\>[56]{}(\Conid{Res}\;\ensuremath{\mathbf{1}}{})){}\<[E]%
\ColumnHook
\end{hscode}\resethooks

We will define several functions as folds over \ensuremath{\Conid{DecTree}} and to do that we introduce a type class \ensuremath{\Conid{TreeAlg}} (for ``Tree Algebra'') which collects the two methods \ensuremath{\Varid{res}} and \ensuremath{\Varid{pic}} which are then used in the fold to replace the constructors \ensuremath{\Conid{Res}} and \ensuremath{\Conid{Pick}}.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{24}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\mathbf{class}\;\Conid{TreeAlg}\;\Varid{a}\;\mathbf{where}{}\<[E]%
\\
\>[B]{}\hsindent{3}{}\<[3]%
\>[3]{}\Varid{res}\mathbin{::}\mathbb{B}\,\to\,\Varid{a}{}\<[E]%
\\
\>[B]{}\hsindent{3}{}\<[3]%
\>[3]{}\Varid{pic}\mathbin{::}\Conid{Index}\,\to\,\Varid{a}\,\to\,\Varid{a}\,\to\,\Varid{a}{}\<[E]%
\\[\blanklineskip]%
\>[B]{}\Varid{foldDT}\mathbin{::}\Conid{TreeAlg}\;\Varid{a}\Rightarrow \Conid{DecTree}\,\to\,\Varid{a}{}\<[E]%
\\
\>[B]{}\Varid{foldDT}\;(\Conid{Res}\;\Varid{b}){}\<[24]%
\>[24]{}\mathrel{=}\Varid{res}\;\Varid{b}{}\<[E]%
\\
\>[B]{}\Varid{foldDT}\;(\Conid{Pick}\;\Varid{i}\;\Varid{t}_{0}\;\Varid{t}_{1}){}\<[24]%
\>[24]{}\mathrel{=}\Varid{pic}\;\Varid{i}\;(\Varid{foldDT}\;\Varid{t}_{0})\;(\Varid{foldDT}\;\Varid{t}_{1}){}\<[E]%
\ColumnHook
\end{hscode}\resethooks
The \ensuremath{\Conid{TreeAlg}} class is used to define our decision trees but also for several other purposes.
(In the implementation we additionally require some total order on \ensuremath{\Varid{a}} to enable efficient set computations.)
We see that our decision tree type is the initial algebra of \ensuremath{\Conid{TreeAlg}} and that we can reimplement a generic version of \ensuremath{\Varid{ex1}} which can be instantiated to any \ensuremath{\Conid{TreeAlg}} instance:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{14}{@{}>{\hspre}l<{\hspost}@{}}%
\column{34}{@{}>{\hspre}l<{\hspost}@{}}%
\column{53}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\mathbf{instance}\;\Conid{TreeAlg}\;\Conid{DecTree}\;\mathbf{where}\;\Varid{res}\mathrel{=}\Conid{Res};\Varid{pic}\mathrel{=}\Conid{Pick};{}\<[E]%
\\[\blanklineskip]%
\>[B]{}\Varid{ex1}\mathbin{::}\Conid{TreeAlg}\;\Varid{a}\Rightarrow \Varid{a}{}\<[E]%
\\
\>[B]{}\Varid{ex1}\mathrel{=}\Varid{pic}\;\mathrm{1}\;{}\<[14]%
\>[14]{}(\Varid{pic}\;\mathrm{3}\;(\Varid{res}\;\ensuremath{\mathbf{0}}{})\;{}\<[34]%
\>[34]{}(\Varid{pic}\;\mathrm{2}\;(\Varid{res}\;\ensuremath{\mathbf{0}}{})\;(\Varid{res}\;\ensuremath{\mathbf{1}}{})))\;{}\<[E]%
\\
\>[14]{}(\Varid{pic}\;\mathrm{2}\;(\Varid{pic}\;\mathrm{3}\;(\Varid{res}\;\ensuremath{\mathbf{0}}{})\;(\Varid{res}\;\ensuremath{\mathbf{1}}{}))\;{}\<[53]%
\>[53]{}(\Varid{res}\;\ensuremath{\mathbf{1}}{})){}\<[E]%
\ColumnHook
\end{hscode}\resethooks

\subsection{Cost}
The cost of a given \ensuremath{\Varid{x}\in \mathbb{B}^{\Varid{n}}} for some decision tree \ensuremath{\Varid{t}} is the length of the path from root to leaf when the input to \ensuremath{\Varid{f}} is \ensuremath{\Varid{x}}.
This computation can be defined as an instance of \ensuremath{\Conid{TreeAlg}}:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{24}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\mathbf{type}\;\Conid{CostFun}\mathrel{=}\mathbb{B}^{\Varid{n}}\,\to\,\Conid{Int}{}\<[E]%
\\[\blanklineskip]%
\>[B]{}\mathbf{instance}\;\Conid{TreeAlg}\;\Conid{CostFun}\;\mathbf{where}\;\Varid{res}\mathrel{=}\Varid{resC};\Varid{pic}\mathrel{=}\Varid{pickC}{}\<[E]%
\\[\blanklineskip]%
\>[B]{}\Varid{resC}\mathbin{::}\mathbb{B}\,\to\,\Conid{CostFun}{}\<[E]%
\\
\>[B]{}\Varid{resC}\;\Varid{b}\mathrel{=}\Varid{const}\;\mathrm{0}{}\<[E]%
\\[\blanklineskip]%
\>[B]{}\Varid{pickC}\mathbin{::}\Conid{Index}\,\to\,\Conid{CostFun}\,\to\,\Conid{CostFun}\,\to\,\Conid{CostFun}{}\<[E]%
\\
\>[B]{}\Varid{pickC}\;\Varid{i}\;\Varid{c}_{0}\;\Varid{c}_{1}\mathrel{=}\lambda \Varid{t}\,\to\,{}\<[24]%
\>[24]{}\mathrm{1}\mathbin{+}\mathbf{if}\;\Varid{index}\;\Varid{t}\;\Varid{i}\;\mathbf{then}\;\Varid{c}_{1}\;\Varid{t}\;\mathbf{else}\;\Varid{c}_{0}\;\Varid{t}{}\<[E]%
\\[\blanklineskip]%
\>[B]{}\Varid{cost}\mathbin{::}\Conid{DecTree}\,\to\,\Conid{CostFun}{}\<[E]%
\\
\>[B]{}\Varid{cost}\mathrel{=}\Varid{foldDT}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks

We get that \ensuremath{\Varid{cost}\;\Varid{ex1}\;[\mskip1.5mu \ensuremath{\mathbf{1}}{},\ensuremath{\mathbf{0}}{},\ensuremath{\mathbf{1}}{}\mskip1.5mu]} is \ensuremath{\mathrm{3}}, while \ensuremath{\Varid{cost}\;\Varid{ex1}\;[\mskip1.5mu \ensuremath{\mathbf{1}}{},\ensuremath{\mathbf{1}}{},\ensuremath{\mathbf{0}}{}\mskip1.5mu]} is \ensuremath{\mathrm{2}}, as can be seen in Figure \ref{fig:Algex}.
Taking the maximum of the cost over all \ensuremath{\Varid{x}\in \mathbb{B}^{\Varid{n}}} gives us the depth of the decision tree \ensuremath{\Varid{t}}.
This can also be defined as an instance of \ensuremath{\Conid{TreeAlg}}.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\mathbf{type}\;\Conid{MaxCost}\mathrel{=}\mathbb{N}{}\<[E]%
\\
\>[B]{}\Varid{pickMC}\;\Varid{i}\;\Varid{m}_{1}\;\Varid{m}_{2}\mathrel{=}\mathrm{1}\mathbin{+}\Varid{max}\;\Varid{m}_{1}\;\Varid{m}_{2}{}\<[E]%
\\
\>[B]{}\mathbf{instance}\;\Conid{TreeAlg}\;\Conid{MaxCost}\;\mathbf{where}\;\Varid{res}\mathrel{=}\Varid{const}\;\mathrm{0};\Varid{pic}\mathrel{=}\Varid{pickMC}{}\<[E]%
\\[\blanklineskip]%
\>[B]{}\Varid{maxCost}\mathbin{::}\Conid{DecTree}\,\to\,\Conid{MaxCost}{}\<[E]%
\\
\>[B]{}\Varid{maxCost}\mathrel{=}\Varid{foldDT}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks

By evaluating \ensuremath{\Varid{maxCost}\;\Varid{ex1}} we get that the maximum cost is \ensuremath{\mathrm{3}} for this example.
Another kind of cost is \emph{expected} cost where we let the bits be independent and identically distributed.
We use the distribution $\pi_p$ for the input bits which means that they are i.i.d.\ with Bernoulli distribution with parameter $p \in [0,1]$ \citep{garban2014noise}.
As for the other cost notions, expected cost is also implemented as an instance of \ensuremath{\Conid{TreeAlg}}.

\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{62}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\mathbf{type}\;\Conid{ExpCost}\;\Varid{a}\mathrel{=}\Conid{Poly}\;\Varid{a}{}\<[E]%
\\
\>[B]{}\mathbf{instance}\;\Conid{Ring}\;\Varid{a}\Rightarrow \Conid{TreeAlg}\;(\Conid{ExpCost}\;\Varid{a})\;\mathbf{where}\;\Varid{res}\mathrel{=}\Varid{resPoly};{}\<[62]%
\>[62]{}\Varid{pic}\mathrel{=}\Varid{pickPoly}{}\<[E]%
\\[\blanklineskip]%
\>[B]{}\Varid{expCost}\mathbin{::}\Conid{Ring}\;\Varid{a}\Rightarrow \Conid{DecTree}\,\to\,\Conid{Poly}\;\Varid{a}{}\<[E]%
\\
\>[B]{}\Varid{expCost}\mathrel{=}\Varid{foldDT}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
Note that the expected cost of any decision tree for a Boolean function of \ensuremath{\Varid{n}} bits will always be a polynomial.
We represent polynomials as lists of coefficients: \ensuremath{\Conid{P}\;[\mskip1.5mu \mathrm{1},\mathrm{2},\mathrm{3}\mskip1.5mu]} represents \ensuremath{\lambda \Varid{p}\,\to\,\mathrm{1}\mathbin{+}\mathrm{2}\mathbin{*}\Varid{p}\mathbin{+}\mathrm{3}\mathbin{*}\ensuremath{\Varid{p}^{\mathrm{2}}}}.
The polynomial implementation relies heavily on material from \cite{JanssonIonescuBernardyDSLsofMathBook2022}.
This includes the polynomial ring operations (\ensuremath{(\mathbin{+})}, \ensuremath{(\mathbin{-})}, \ensuremath{(\mathbin{*})}), \ensuremath{\Varid{gcd}}, \ensuremath{\Varid{divMod}}, symbolic derivative, and ordering.
The \ensuremath{\Varid{res}} and \ensuremath{\Varid{pic}} functions are as follows:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\Varid{resPoly}\mathbin{::}\Conid{Ring}\;\Varid{a}\Rightarrow \mathbb{B}\,\to\,\Varid{a}{}\<[E]%
\\
\>[B]{}\Varid{resPoly}\;\kern0.06em \vbox{\hrule\@width.5em} \Varid{b}\mathrel{=}\Varid{zero}{}\<[E]%
\\[\blanklineskip]%
\>[B]{}\Varid{pickPoly}\mathbin{::}\Conid{Ring}\;\Varid{a}\Rightarrow \Conid{Index}\,\to\,\Conid{Poly}\;\Varid{a}\,\to\,\Conid{Poly}\;\Varid{a}\,\to\,\Conid{Poly}\;\Varid{a}{}\<[E]%
\\
\>[B]{}\Varid{pickPoly}\;\kern0.06em \vbox{\hrule\@width.5em} \Varid{i}\;\Varid{p}_{0}\;\Varid{p}_{1}\mathrel{=}\Varid{one}\mathbin{+}(\Varid{one}\mathbin{-}\Varid{xP})\mathbin{*}\Varid{p}_{0}\mathbin{+}\Varid{xP}\mathbin{*}\Varid{p}_{1}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
Here \ensuremath{\Varid{zero}\mathrel{=}\Conid{P}\;[\mskip1.5mu \mskip1.5mu]} and \ensuremath{\Varid{one}\mathrel{=}\Conid{P}\;[\mskip1.5mu \mathrm{1}\mskip1.5mu]} represent \ensuremath{\Varid{const}\;\mathrm{0}} and \ensuremath{\Varid{const}\;\mathrm{1}} respectively while \ensuremath{\Varid{xP}\mathrel{=}\Conid{P}\;[\mskip1.5mu \mathrm{0},\mathrm{1}\mskip1.5mu]} is ``the polynomial \ensuremath{\Varid{p}}''.
For \ensuremath{\Varid{pickPoly}\;\kern0.06em \vbox{\hrule\@width.5em} \;\Varid{p}_{0}\;\Varid{p}_{1}} we first have to pick one bit and then if this bit is \ensuremath{\ensuremath{\mathbf{0}}{}} (with probability $\mathbb{P}(\val{i} = \ensuremath{\mathbf{0}}) = (1-p)$) we get $p_0$ which is the polynomial for this case.
If the bit is instead \ensuremath{\ensuremath{\mathbf{1}}{}} (with probability $\mathbb{P}(\val{i} = \ensuremath{\mathbf{1}}) = p$) we get $p_1$.
The expected cost of the decision tree \ensuremath{\Varid{ex1}} is $2  + 2p - 2p^2$.

\subsection{Complexity}
Now that we have introduced some notions of cost of decision trees, we can introduce complexity of a Boolean function which is the minimum of the cost over all decision trees for the given function.
Using \ensuremath{\Varid{maxCost}} we specify the concept of deterministic complexity as \ensuremath{\Conid{D}\;(\Varid{f})\mathrel{=}\min_{\Varid{t}}\;(\Varid{maxCost}\;\Varid{t})} where \ensuremath{\Varid{t}} ranges over all the decision trees for the function \ensuremath{\Varid{f}}.
The type is \ensuremath{\Conid{D}\mathop{:}\Conid{BoFun}\;\Varid{bf}\Rightarrow \Varid{bf}\,\to\,\mathbb{N}} and to calculate it we need to generate all the decision trees.
The level-\ensuremath{\Varid{p}}-complexity is defined using \ensuremath{\Varid{expCost}} as $D_p(f) = \ensuremath{\min_{\Varid{t}}\;(\Varid{evalPoly}\;(\Varid{expCost}\;\Varid{t})\;\Varid{p})}$
Thus, for each probability \ensuremath{\Varid{p}} and Boolean function \ensuremath{\Varid{f}} the minimum over all the decision trees will give the smallest expected cost.
If we flip the argument order we can see that $D_p(f)$ takes a Boolean function \ensuremath{\Varid{f}} to a function from \ensuremath{\Varid{p}} to the smallest expected cost.
As \ensuremath{\Varid{expCost}} always returns a polynomial, the level-\ensuremath{\Varid{p}}-complexity is a continuous, piecewise polynomial, function of \ensuremath{\Varid{p}}.

In our implementation, we do not implement a special type for piecewise polynomials, we just represent them as sets of polynomials, and leave the last minimum to the surrounding code.
More about the implementation is explained in Section~\ref{sec:method}.

\subsection{Examples of Boolean functions and their costs}
\label{sec:ex}
For the constant functions, we already know the result so \ensuremath{\Varid{maxCost}\;(\Conid{Res}\;\Varid{b})\mathrel{=}\mathrm{0}} and \ensuremath{\Varid{expCost}\;(\Conid{Res}\;\Varid{b})\mathrel{=}\Varid{zero}} and then $D(\ensuremath{\ensuremath{\Varid{const}_{\Varid{n}}}}) = D_p(\ensuremath{\ensuremath{\Varid{const}_{\Varid{n}}}}) = 0$.
For the dictator function, there is only one minimizing decision tree irrespective of input: the one that picks bit 1 first.
After asking the first bit the function is reduced to the constant function as can be seen in Figure \ref{fig:dict} and we get the optimal decision tree \ensuremath{\Varid{optTree}\mathrel{=}\Conid{Pick}\;\mathrm{1}\;(\Conid{Res}\;\ensuremath{\mathbf{0}}{})\;(\Conid{Res}\;\ensuremath{\mathbf{1}}{})}.
The results are
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{10}{@{}>{\hspre}l<{\hspost}@{}}%
\column{19}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\Varid{maxCost}\;{}\<[10]%
\>[10]{}\Varid{optTree}{}\<[19]%
\>[19]{}\mathrel{=}\mathrm{1}\mathbin{+}\Varid{max}\;\mathrm{0}\;\mathrm{0}\mathrel{=}\mathrm{1}{}\<[E]%
\\
\>[B]{}\Varid{expCost}\;{}\<[10]%
\>[10]{}\Varid{optTree}{}\<[19]%
\>[19]{}\mathrel{=}\Varid{one}\mathbin{+}(\Varid{one}\mathbin{-}\Varid{xP})\mathbin{*}\Varid{zero}\mathbin{+}\Varid{xP}\mathbin{*}\Varid{zero}\mathrel{=}\Varid{one}\ .{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
This then gives $D(\ensuremath{\ensuremath{\Varid{dict}_{\Varid{n}}}}) = 1$, and similarly $D_p(\ensuremath{\ensuremath{\Varid{dict}_{\Varid{n}}}}) = 1$.

The parity function is
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\Varid{count}\mathbin{::}\Conid{Eq}\;\Varid{a}\Rightarrow \Varid{a}\,\to\,[\mskip1.5mu \Varid{a}\mskip1.5mu]\,\to\,\Conid{Int}{}\<[E]%
\\
\>[B]{}\Varid{count}\;\Varid{x}\mathrel{=}\Varid{length}\mathbin{\circ}\Varid{filter}\;(\Varid{x}\doubleequals){}\<[E]%
\\[\blanklineskip]%
\>[B]{}\Varid{par}_{\!\Varid{n}}\mathbin{::}\mathbb{B}^{\Varid{n}}\,\to\,\mathbb{B}{}\<[E]%
\\
\>[B]{}\Varid{par}_{\!\Varid{n}}\mathrel{=}\Varid{odd}\mathbin{\circ}\Varid{count}\;\ensuremath{\mathbf{1}}{}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
In this case all bits have to be picked to determine the parity, regardless of input.
For example, if we first ask one bit to determine \ensuremath{\Varid{par}_{\!\Varid{n}\mathbin{+}\mathrm{1}}}, then we are left with two subtrees: \ensuremath{\Varid{t}_{0}} for \ensuremath{\Varid{par}_{\!\Varid{n}}} and \ensuremath{\Varid{t}_{1}} for \ensuremath{\neg \;\Varid{par}_{\!\Varid{n}}} as seen in Figure \ref{fig:par}.
\begin{figure}[tbp]
  \centering
  \begin{forest}
    for tree =

        minimum height=1ex, text depth = 0.25ex,
       anchor = north,

         edge = {-Stealth},
        s sep = 1em,
        l sep = 2em
                },
    EL/.style =
       before typesetting nodes=
    where n=1{edge label/.wrap value={node[pos=0.5,anchor=east]{#1}}
             {edge label/.wrap value={node[pos=0.5,anchor=west]{#1}}
                                }

    [\ensuremath{\Varid{par}_{\!\Varid{n}\mathbin{+}\mathrm{1}}},
        [, edge label = {node[midway,anchor = south] {1}}
            [\ensuremath{\Varid{par}_{\!\Varid{n}}}, EL = \ensuremath{\ensuremath{\mathbf{0}}{}}]
            [\ensuremath{\neg \;\Varid{par}_{\!\Varid{n}}}, EL = \ensuremath{\ensuremath{\mathbf{1}}{}}]
        ]
        [, EL = 2
            [\ensuremath{\Varid{par}_{\!\Varid{n}}}, EL = \ensuremath{\ensuremath{\mathbf{0}}{}}]
            [\ensuremath{\neg \;\Varid{par}_{\!\Varid{n}}}, EL = \ensuremath{\ensuremath{\mathbf{1}}{}}]
        ]
        [,no edge,EL = $\ldots$]
        [,no edge]
        [, edge label = {node[midway,anchor = south]{$n+1$}}
            [\ensuremath{\Varid{par}_{\!\Varid{n}}}, EL = \ensuremath{\ensuremath{\mathbf{0}}{}}]
            [\ensuremath{\neg \;\Varid{par}_{\!\Varid{n}}}, EL = \ensuremath{\ensuremath{\mathbf{1}}{}}]
      ]
    ]
\end{forest}
  \caption{The recursive structure of the parity function (\ensuremath{\Varid{par}_{\!\Varid{n}}}). The pattern repeats all the way down to \ensuremath{\Varid{par}_{\!\mathrm{0}}\mathrel{=}\Varid{const}\;\ensuremath{\mathbf{0}}{}}.}
  \label{fig:par}
\end{figure}
Recursively, this gives
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{10}{@{}>{\hspre}l<{\hspost}@{}}%
\column{26}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\Varid{maxCost}\;{}\<[10]%
\>[10]{}(\Conid{Pick}\;\Varid{i}\;\Varid{t}_{0}\;\Varid{t}_{1}){}\<[26]%
\>[26]{}\mathrel{=}\mathrm{1}\mathbin{+}\Varid{max}\;(\Varid{maxCost}\;\Varid{t}_{0})\;(\Varid{maxCost}\;\Varid{t}_{1})\mathrel{=}\mathrm{1}\mathbin{+}\Varid{max}\;\Varid{n}\;\Varid{n}\mathrel{=}\mathrm{1}\mathbin{+}\Varid{n}{}\<[E]%
\\
\>[B]{}\Varid{expCost}\;{}\<[10]%
\>[10]{}(\Conid{Pick}\;\Varid{i}\;\Varid{t}_{0}\;\Varid{t}_{1}){}\<[26]%
\>[26]{}\mathrel{=}\Varid{one}\mathbin{+}(\Varid{one}\mathbin{-}\Varid{xP})\mathbin{*}(\Varid{expCost}\;\Varid{t}_{0})\mathbin{+}\Varid{xP}\mathbin{*}(\Varid{expCost}\;\Varid{t}_{1}){}\<[E]%
\\
\>[26]{}\mathrel{=}\Varid{one}\mathbin{+}(\Varid{one}\mathbin{-}\Varid{xP})\mathbin{*}\Varid{n}\mathbin{+}\Varid{xP}\mathbin{*}\Varid{n}\mathrel{=}\mathrm{1}\mathbin{+}\Varid{n}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
Thus, $D(\ensuremath{\Varid{par}_{\!\Varid{n}}}) = D_p(\ensuremath{\Varid{par}_{\!\Varid{n}}}) = n$.
This can also be seen if you compare Figure \ref{fig:dict} with Figure \ref{fig:par}, the minimum depth of the dictator tree is 1, while the minimum depth of the parity tree is $n$.

We now introduce the Boolean function \ensuremath{\Varid{same}} which checks if all bits are equal:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\Varid{same}\mathbin{::}\mathbb{B}^{\Varid{n}}\,\to\,\mathbb{B}{}\<[E]%
\\
\>[B]{}\Varid{same}\;\Varid{bs}\mathrel{=}\Varid{and}\;\Varid{bs}\mathrel{\vee}\neg \;(\Varid{or}\;\Varid{bs}){}\<[E]%
\ColumnHook
\end{hscode}\resethooks
Using \ensuremath{\Varid{same}} we construct a very specific function of 5 bits where we first split the bits into two groups, one with the first three bits and the second with the last two bits.
On the first group, called \ensuremath{\Varid{as}}, we check if the bits are not the same, and on the second group, called \ensuremath{\Varid{cs}} we check if the bits are the same.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\Varid{sim}_{5}\mathbin{::}\mathbb{B}^{\mathrm{5}}\,\to\,\mathbb{B}{}\<[E]%
\\
\>[B]{}\Varid{sim}_{5}\;\Varid{bs}\mathrel{=}\neg \;(\Varid{same}\;\Varid{as})\mathrel{\vee}\Varid{same}\;\Varid{cs}{}\<[E]%
\\
\>[B]{}\hsindent{3}{}\<[3]%
\>[3]{}\mathbf{where}\;(\Varid{as},\Varid{cs})\mathrel{=}\Varid{splitAt}\;\mathrm{3}\;\Varid{bs}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
The point of this function is to illustrate a special case where the best decision tree depends on \ensuremath{\Varid{p}} so that the level-\ensuremath{\Varid{p}}-complexity consists of several different polynomials.
This computation is shown in Section \ref{sec:fAC}.

One of the major goals of this paper was to calculate the level-\ensuremath{\Varid{p}}-complexity of 9 bit iterated majority called \ensuremath{\Varid{maj}_{3}^2}.
When extending the majority function to \ensuremath{\Varid{maj}_{3}^2}, we use \ensuremath{\Varid{maj}_{3}} inside \ensuremath{\Varid{maj}_{3}}.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{10}{@{}>{\hspre}l<{\hspost}@{}}%
\column{17}{@{}>{\hspre}l<{\hspost}@{}}%
\column{23}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\Varid{maj}_{3}^2\mathbin{::}\mathbb{B}^{\mathrm{9}}\,\to\,\mathbb{B}{}\<[E]%
\\
\>[B]{}\Varid{maj}_{3}^2\;\Varid{bs}\mathrel{=}\Varid{maj}_{3}\;[\mskip1.5mu \Varid{maj}_{3}\;\Varid{bs}_{1},\Varid{maj}_{3}\;\Varid{bs}_{2},\Varid{maj}_{3}\;\Varid{bs}_{3}\mskip1.5mu]{}\<[E]%
\\
\>[B]{}\hsindent{3}{}\<[3]%
\>[3]{}\mathbf{where}\;{}\<[10]%
\>[10]{}(\Varid{bs}_{1},{}\<[17]%
\>[17]{}\Varid{rest}{}\<[23]%
\>[23]{})\mathrel{=}\Varid{splitAt}\;\mathrm{3}\;\Varid{bs}{}\<[E]%
\\
\>[10]{}(\Varid{bs}_{2},{}\<[17]%
\>[17]{}\Varid{bs}_{3}{}\<[23]%
\>[23]{})\mathrel{=}\Varid{splitAt}\;\mathrm{3}\;\Varid{rest}{}\<[E]%
\\[\blanklineskip]%
\>[B]{}\Varid{maj}_{\Varid{n}}\mathbin{::}\mathbb{B}^{\Varid{n}}\,\to\,\mathbb{B}{}\<[E]%
\\
\>[B]{}\Varid{maj}_{\Varid{n}}\;\Varid{bs}\mathrel{=}\Varid{count}\;\ensuremath{\mathbf{1}}{}\;\Varid{bs}\geq \Varid{count}\;\ensuremath{\mathbf{0}}{}\;\Varid{bs}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
It is hard to calculate $D_p(\ensuremath{\Varid{maj}_{3}^2})$ by hand because there are very many different decision trees, and this motivated our Haskell implementation of the calculations explained in Section~\ref{sec:method}.

\section{Computing the level-$p$-complexity}
\label{sec:method}
The process of generating decision trees, memoization, thinning and comparing polynomials is explained more in detail.

\subsection{Generating decision trees}
The decision trees of a function \ensuremath{\Varid{f}} can be described in terms of the decision trees for the immediate subfunctions ($\fixatill{i}{b}{f} = \ensuremath{\Varid{setBit}\;\Varid{i}\;\Varid{b}\;\Varid{f}}$) for different \ensuremath{\Varid{i}\mathbin{::}\Conid{Index}} and \ensuremath{\Varid{b}\mathbin{::}\mathbb{B}}.
Given the Boolean function \ensuremath{\Varid{f}}, if $f$ is constant (returning \ensuremath{\Varid{b}}) we return the singleton set \ensuremath{\{\mskip1.5mu \Varid{res}\;\Varid{b}\mskip1.5mu\}}.
Otherwise, \ensuremath{\Varid{f}}'s decision trees are generated recursively by asking each bit $i$, and generating the decision trees for the subfunctions $\fixatill{i}{\ensuremath{\mathbf{0}}}{f}$ and $\fixatill{i}{\ensuremath{\mathbf{1}}}{f}$.
The recursive step is shown in the formula below:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{56}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\ensuremath{\Varid{genAlg}_{\Varid{n}\mathbin{+}\mathrm{1}}}\;\Varid{f}\mathrel{=} \{\mskip1.5mu \Varid{pic}\;\Varid{i}\;\Varid{t}_{0}\;\Varid{t}_{1}\mid \Varid{i}\leftarrow \{\mskip1.5mu \mathrm{1}\mathinner{\ldotp\ldotp}\Varid{n}\mskip1.5mu\},{}\<[56]%
\>[56]{}\Varid{t}_{0}\leftarrow \ensuremath{\Varid{genAlg}_{\Varid{n}}}\;\fixatill{\Varid{i}}{\ensuremath{\mathbf{0}}{}}{\Varid{f}},\Varid{t}_{1}\leftarrow \ensuremath{\Varid{genAlg}_{\Varid{n}}}\;\fixatill{\Varid{i}}{\ensuremath{\mathbf{1}}{}}{\Varid{f}}\mskip1.5mu\}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
  The complexity computation starts from a Boolean function \ensuremath{\Varid{f}\mathop{:}\Conid{BoolFun}\;\Varid{n}}, and generates many decision trees for it. There are two
  top level cases: either the function \ensuremath{\Varid{f}} is constant (and returns \ensuremath{\Varid{b}\mathop{:}\mathbb{B}}), in which case there is only one decision tree: \ensuremath{\Varid{res}\;\Varid{b}}; or
  the function \ensuremath{\Varid{f}} still depends on some of the input bits.

  In the latter case, for each index \ensuremath{\Varid{i}\mathop{:}\Conid{Fin}\;\Varid{n}} we can generate two
  ``subfunctions'' \ensuremath{\Varid{f}_{0}\;\Varid{i}\mathrel{=}\Varid{setBit}\;\Varid{i}\;\ensuremath{\mathbf{0}}{}\;\Varid{f}} and \ensuremath{\Varid{f}_{1}\;\Varid{i}\mathrel{=}\Varid{setBit}\;\Varid{i}\;\ensuremath{\mathbf{1}}{}\;\Varid{f}}.  Now, if we recursively generate a decision tree \ensuremath{\Varid{t}_{0}} for \ensuremath{\Varid{f}_{0}\;\Varid{i}}
  and \ensuremath{\Varid{t}_{1}} for \ensuremath{\Varid{f}_{1}\;\Varid{i}} we can combine them to a bigger decision tree
  using \ensuremath{\Varid{pic}\;\Varid{i}\;\Varid{t}_{0}\;\Varid{t}_{1}}.
  Now we only need to do this for all combinations of \ensuremath{\Varid{i}}, \ensuremath{\Varid{t}_{0}}, and
  \ensuremath{\Varid{t}_{1}}.
\begin{figure}[bp]
  \centering
  \begin{forest}
    for tree =

       anchor = north,

         edge = {-Stealth},
        s sep = 1em,
        l sep = 2em
                },
    EL/.style =
       before typesetting nodes=
    where n=1{edge label/.wrap value={node[pos=0.5,anchor=east]{#1}}
             {edge label/.wrap value={node[pos=0.5,anchor=west]{#1}}
                                }

    [\genAlgNode{3}{\ensuremath{\Varid{maj}_{3}}}{\{2 + 2p - 2p^2\}},
        [\genAlgNode{2}{\ensuremath{\Varid{and}_{2}}}{\{1+ p\}}, EL = \ensuremath{\ensuremath{\mathbf{0}}{}}
            [\genAlgNode{1}{\ensuremath{\Varid{const}\;\ensuremath{\mathbf{0}}{}}}{\{0\}}, EL = \ensuremath{\ensuremath{\mathbf{0}}{}}]
            [\genAlgNode{1}{\ensuremath{\Varid{id}}}{\{1\}}, EL = \ensuremath{\ensuremath{\mathbf{1}}{}}

            ]
        ]
        [\genAlgNode{2}{\ensuremath{\Varid{or}_{2}}}{\{2 -p\}}, EL = \ensuremath{\ensuremath{\mathbf{1}}{}}
            [\genAlgNode{1}{\ensuremath{\Varid{id}}}{\{1\}}, EL = \ensuremath{\ensuremath{\mathbf{0}}{}}

            ]
            [\genAlgNode{1}{\ensuremath{\Varid{const}\;\ensuremath{\mathbf{0}}{}}}{\{0\}}, EL = \ensuremath{\ensuremath{\mathbf{1}}{}}]
        ]
    ]
\end{forest}
  \caption{A simplified computation tree of \ensuremath{\ensuremath{\Varid{genAlg}_{\mathrm{3}}}\;\Varid{maj}_{3}}. Each node shows the input and output of the local call to \ensuremath{\ensuremath{\Varid{genAlg}_{\cdot }}}. As all the
    functions involved are ``symmetric'' in the index (\ensuremath{\Varid{setBit}\;\Varid{i}\;\Varid{b}\;\Varid{f}\doubleequals\Varid{setBit}\;\Varid{j}\;\Varid{b}\;\Varid{f}} for all \ensuremath{\Varid{i}} and \ensuremath{\Varid{j}}) we only show edges for
    \ensuremath{\ensuremath{\mathbf{0}}{}} and \ensuremath{\ensuremath{\mathbf{1}}{}} from each level.}
  \label{fig:alg}
\end{figure}

We would like to enumerate the cost polynomials of all the decision trees of a particular Boolean function (\ensuremath{\Varid{n}\mathrel{=}\mathrm{9}}, \ensuremath{\Varid{f}\mathrel{=}\Varid{maj}_{3}^2} is our main goal).
Without taking symmetries into account there are \ensuremath{\mathrm{2}\mathbin{*}\Varid{n}} immediate subfunctions $\fixatill{i}{b}{f}$ and if $T_g$ is the cardinality of the enumeration for subfunction $g$ we have that
\nopagebreak
  $$T_{\ensuremath{\Varid{f}}} = \sum_{i=1}^n T_{\fixatill{i}{\ensuremath{\mathbf{0}}}{f}}*T_{\fixatill{i}{\ensuremath{\mathbf{1}}}{f}}$$

These numbers can be really big if we count all decision trees, but if we only care about their cost polynomials, many decision trees will collapse to the same polynomial, making the counts more manageable (but still possibly really big).
Even the total number of subfunctions encountered (the number of recursive calls) can be quite big.
If all the \ensuremath{\mathrm{2}\mathbin{*}\Varid{n}} immediate subfunctions are different, and if all of them would generate \ensuremath{\mathrm{2}\mathbin{*}(\Varid{n}\mathbin{-}\mathrm{1})} different subfunctions in turn, the number of subfunctions would be $2^n * n!$.
But in practice many subfunctions will be the same.
When computing the polynomials for the 9-bit function \ensuremath{\Varid{maj}_{3}^2}, for example, only \ensuremath{\mathrm{215}} distinct subfunctions are encountered.

As a smaller example, for the 3-bit majority function \ensuremath{\Varid{maj}_{3}}, choosing \ensuremath{\Varid{i}\mathrel{=}\mathrm{1},\mathrm{2},} or \ensuremath{\mathrm{3}} gives exactly the same subfunctions.
Fig.~\ref{fig:alg} illustrates a simplified call graph of \ensuremath{\ensuremath{\Varid{genAlg}_{\mathrm{3}}}\;\Varid{maj}_{3}} and the results (the expected cost polynomials) for the different subfunctions.
In this case all the sets are singletons, but that is very unusual for more realistic Boolean functions.
It would take too long to compute all polynomials for the 9-bit function \ensuremath{\Varid{maj}_{3}^2} but there are 21 distinct 7-bit sub-functions, and the first one of them already has \ensuremath{\mathrm{18021}} polynomials.
Thus we can expect billions of polynomials for \ensuremath{\Varid{maj}_{3}^2} and this means we need to look at ways to keep only the most promising candidates at each level.
This leads us to the algorithmic design technique of thinning.

\subsection{Thinning}

The general shape of the specification has two phases: ``generate all candidates'' followed by ``pick the best one(s)''.
The first phase is recursive and we would like to push as much as possible of ``pick the best'' into the recursive computation.
In the extreme case of a greedy algorithm, we can thin the intermediate sets all the way down to singletons, but even if the sets are a bit bigger than that we can still reduce the computation cost significantly.
A good (but abstract) reference for thinning is the Algebra of Programming book \cite[Chapter 8]{bird_algebra_1997} and more concrete references are the corresponding developments in Agda \citep{DBLP:journals/jfp/MuKJ09} and Haskell \citep{bird_gibbons_2020}.

We are looking for a ``smallest'' polynomial, but we only have a preorder, not a total order, which means that we may need to keep a set of incomparable candidates (elements \ensuremath{\Varid{x}\not\doubleequals\Varid{y}} for which neither \ensuremath{\Varid{x}\prec\Varid{y}} nor \ensuremath{\Varid{y}\prec\Varid{x}}).
We start from a strict preorder \ensuremath{(\prec)\mathop{:}\Varid{a}\,\to\,\Varid{a}\,\to\,\Conid{Prop}} (an irreflexive and transitive relation).
You can think of \ensuremath{\Conid{Prop}} as \ensuremath{\mathbb{B}} because we only work with decidable relations and finite sets in this application.
As we are looking for minima, we say that \ensuremath{\Varid{x}} \emph{dominates} \ensuremath{\Varid{y}} if \ensuremath{\Varid{x}\prec\Varid{y}}.
In our case we will use it for polynomials, but the theory works more generally.

We lift the order relation to sets in two steps.
First \ensuremath{\Varid{ys}\mathrel{\dot{\prec}}\Varid{x}} means that \ensuremath{\Varid{ys}} \emph{dominates} \ensuremath{\Varid{x}},
meaning that some element in \ensuremath{\Varid{ys}} is smaller than \ensuremath{\Varid{x}}.
If this holds, there is no need to add \ensuremath{\Varid{x}} to \ensuremath{\Varid{ys}} because we already
have at least one better element in \ensuremath{\Varid{ys}}.
Then \ensuremath{\Varid{ys}\mathrel{\ddot{\prec}}\Varid{xs}} means that \ensuremath{\Varid{ys}} dominates all of \ensuremath{\Varid{xs}}.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}(\mathrel{\dot{\prec}})\mathop{:}\Conid{Set}\;\Varid{a}\,\to\,\Varid{a}\,\to\,\Conid{Prop}{}\<[E]%
\\
\>[B]{}\Varid{ys}\mathrel{\dot{\prec}}\Varid{x}\mathrel{=}\exists\,\Varid{y}\in \Varid{ys}.\,\,\Varid{y}\prec\Varid{x}{}\<[E]%
\\[\blanklineskip]%
\>[B]{}(\mathrel{\ddot{\prec}})\mathop{:}\Conid{Set}\;\Varid{a}\,\to\,\Conid{Set}\;\Varid{a}\,\to\,\Conid{Prop}{}\<[E]%
\\
\>[B]{}\Varid{ys}\mathrel{\ddot{\prec}}\Varid{xs}\mathrel{=}\forall\,\Varid{x}\in \Varid{xs}.\,\,\Varid{ys}\mathrel{\dot{\prec}}\Varid{x}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
Finally, we combine subset and domination into the thinning relation:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\Conid{Thin}\;\Varid{ys}\;\Varid{xs}\mathrel{=}(\Varid{ys}\subseteq\Varid{xs})\mathrel{\wedge}\Varid{ys}\mathrel{\ddot{\prec}}(\Varid{xs}\mathbin{\char92 \char92 }\Varid{ys}){}\<[E]%
\ColumnHook
\end{hscode}\resethooks
We will use this relation in the specification of our efficient computation to ensure that the small set of polynomials computed, still ``dominates'' the big set of all the polynomials generated by \ensuremath{\ensuremath{\Varid{genAlg}_{\Varid{n}}}\;\Varid{f}}.

But first we introduce the helper function \ensuremath{\Varid{thin}\mathop{:}\Conid{Set}\;\Varid{a}\,\to\,\Conid{Set}\;\Varid{a}} which aims at removing some elements, while still keeping the minima in the set.
It has to refine the relation \ensuremath{\Conid{Thin}} which means that if \ensuremath{\Varid{ys}\mathrel{=}\Varid{thin}\;\Varid{xs}} then \ensuremath{\Varid{ys}} must be a subset of \ensuremath{\Varid{xs}} (\ensuremath{\Varid{ys}\subseteq\Varid{xs}}) and \ensuremath{\Varid{ys}} must dominate the rest of \ensuremath{\Varid{xs}} (\ensuremath{\Varid{ys}\mathrel{\ddot{\prec}}(\Varid{xs}\mathbin{\char92 \char92 }\Varid{ys})}).
A trivial (but useless) implementation would be \ensuremath{\Varid{thin}\mathrel{=}\Varid{id}}, and any implementation which removes some ``dominated'' elements could be helpful.
The best we can hope for is that \ensuremath{\Varid{thin}} gives us a set of only incomparable elements.
If \ensuremath{\Varid{thin}} compares all pairs of elements, it can compute a smallest thinning.
In general that may not be needed (and a linear time greedy approximation is good enough), but in some settings almost any algorithmic cost which can reduce the intermediate sets will pay off.
We use the following greedy version (inspired by \citet{bird_gibbons_2020}) as one of the methods of the class \ensuremath{\Conid{Thinnable}}:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\Varid{thin}\mathbin{::}\Conid{Thinnable}\;\Varid{a}\Rightarrow \Conid{Set}\;\Varid{a}\,\to\,\Conid{Set}\;\Varid{a}{}\<[E]%
\\
\>[B]{}\Varid{thin}\mathrel{=}\Varid{foldl}\;\Varid{thinStep}\;\emptyset{}\<[E]%
\\
\>[B]{}\Varid{thinStep}\mathbin{::}\Conid{Thinnable}\;\Varid{a}\Rightarrow \Conid{Set}\;\Varid{a}\,\to\,\Varid{a}\,\to\,\Conid{Set}\;\Varid{a}{}\<[E]%
\\
\>[B]{}\Varid{thinStep}\;\Varid{ys}\;\Varid{x}\mathrel{=}\mathbf{if}\;\Varid{ys}\mathrel{\dot{\prec}}\Varid{x}\;\mathbf{then}\;\Varid{ys}\;\mathbf{else}\;\Varid{insert}\;\Varid{x}\;\Varid{ys}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
It starts from an empty set and considers one element \ensuremath{\Varid{x}} at a time.
If the set \ensuremath{\Varid{ys}} collected thus far already dominates \ensuremath{\Varid{x}}, it is kept
unchanged, otherwise \ensuremath{\Varid{x}} is inserted.
(The optimal version also removes from \ensuremath{\Varid{ys}} all elements dominated by \ensuremath{\Varid{x}}.)
It is easy to prove that \ensuremath{\Varid{thin}} implements the specification \ensuremath{\Conid{Thin}}.

Now we have what we need to specify when an efficient \ensuremath{\ensuremath{\Varid{genAlgT}_{\!\Varid{n}}}\;\Varid{f}} computation is correct.
Our specification (\ensuremath{\Varid{spec}\;\Varid{n}\;\Varid{f}}) states a relation between a (very big) set \ensuremath{\Varid{xs}\mathrel{=}\ensuremath{\Varid{genAlg}_{\Varid{n}}}\;\Varid{f}} and a smaller set \ensuremath{\Varid{ys}\mathrel{=}\ensuremath{\Varid{genAlgT}_{\!\Varid{n}}}\;\Varid{f}} we get by applying thinning at each recursive step.
We want to prove that \ensuremath{\Varid{ys}\subseteq\Varid{xs}} and \ensuremath{\Varid{ys}\mathrel{\ddot{\prec}}(\Varid{xs}\mathbin{\char92 \char92 }\Varid{ys})} because then we know we have not lost any of the candidates for minimality.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{15}{@{}>{\hspre}l<{\hspost}@{}}%
\column{20}{@{}>{\hspre}l<{\hspost}@{}}%
\column{24}{@{}>{\hspre}l<{\hspost}@{}}%
\column{40}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\Varid{spec}\;\Varid{n}\;\Varid{f}\mathrel{=}{}\<[15]%
\>[15]{}\mathbf{let}\;{}\<[20]%
\>[20]{}\Varid{xs}{}\<[24]%
\>[24]{}\mathrel{=}\ensuremath{\Varid{genAlg}_{\Varid{n}}}\;{}\<[40]%
\>[40]{}\Varid{f}{}\<[E]%
\\
\>[20]{}\Varid{ys}{}\<[24]%
\>[24]{}\mathrel{=}\ensuremath{\Varid{genAlgT}_{\!\Varid{n}}}\;{}\<[40]%
\>[40]{}\Varid{f}{}\<[E]%
\\
\>[15]{}\mathbf{in}\;{}\<[20]%
\>[20]{}(\Varid{ys}\subseteq\Varid{xs})\mathrel{\wedge}(\Varid{ys}\mathrel{\ddot{\prec}}(\Varid{xs}\mathbin{\char92 \char92 }\Varid{ys})){}\<[E]%
\ColumnHook
\end{hscode}\resethooks
We can first take care of the simplest case (for any \ensuremath{\Varid{n}}).
If the function \ensuremath{\Varid{f}} is constant (returning some \ensuremath{\Varid{b}\mathop{:}\mathbb{B}}), both \ensuremath{\Varid{xs}}
and \ensuremath{\Varid{ys}} will be the singleton set containing \ensuremath{\Varid{res}\;\Varid{b}}.
Thus both properties trivially hold.

We then proceed by induction on \ensuremath{\Varid{n}} to prove \ensuremath{\Conid{S}_{\Varid{n}}\mathrel{=}\forall\,\Varid{f}\mathop{:}\Conid{BoolFun}\;\Varid{n}.\,\,\Varid{spec}\;\Varid{n}\;\Varid{f}}.
In the base case \ensuremath{\Varid{n}\mathrel{=}\mathrm{0}} the function is necessarily constant, and we
have already covered that above.
In the inductive step case, assume the induction hypothesis \ensuremath{\Conid{IH}\mathrel{=}\Conid{S}_{\Varid{n}}} and prove \ensuremath{\Conid{S}_{\Varid{n}\mathbin{+}\mathrm{1}}} for a function \ensuremath{\Varid{f}\mathop{:}\Conid{BoolFun}\;(\Varid{n}\mathbin{+}\mathrm{1})}.
We have already covered the constant function case, so we focus on the main recursive clause of the definitions of \ensuremath{\ensuremath{\Varid{genAlg}_{\Varid{n}}}\;\Varid{f}} and \ensuremath{\ensuremath{\Varid{genAlgT}_{\!\Varid{n}}}\;\Varid{f}}:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{19}{@{}>{\hspre}l<{\hspost}@{}}%
\column{31}{@{}>{\hspre}l<{\hspost}@{}}%
\column{43}{@{}>{\hspre}l<{\hspost}@{}}%
\column{62}{@{}>{\hspre}l<{\hspost}@{}}%
\column{66}{@{}>{\hspre}l<{\hspost}@{}}%
\column{83}{@{}>{\hspre}l<{\hspost}@{}}%
\column{112}{@{}>{\hspre}l<{\hspost}@{}}%
\column{129}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\ensuremath{\Varid{genAlg}_{\Varid{n}\mathbin{+}\mathrm{1}}}\;{}\<[19]%
\>[19]{}\Varid{f}\mathrel{=}{}\<[31]%
\>[31]{}\{\mskip1.5mu \Varid{pic}\;\Varid{i}\;\Varid{x}_{0}\;{}\<[43]%
\>[43]{}\Varid{x}_{1}\mid \Varid{i}\leftarrow [\mskip1.5mu \mathrm{1}\mathinner{\ldotp\ldotp}\Varid{n}\mskip1.5mu],{}\<[62]%
\>[62]{}\Varid{x}_{0}{}\<[66]%
\>[66]{}\leftarrow \ensuremath{\Varid{genAlg}_{\Varid{n}}}\;{}\<[83]%
\>[83]{}\fixatill{\Varid{i}}{\ensuremath{\mathbf{0}}{}}{\Varid{f}},\Varid{x}_{1}{}\<[112]%
\>[112]{}\leftarrow \ensuremath{\Varid{genAlg}_{\Varid{n}}}\;{}\<[129]%
\>[129]{}\fixatill{\Varid{i}}{\ensuremath{\mathbf{1}}{}}{\Varid{f}}\mskip1.5mu\}{}\<[E]%
\\
\>[B]{}\ensuremath{\Varid{genAlgT}_{\!\Varid{n}\mathbin{+}\mathrm{1}}}\;{}\<[19]%
\>[19]{}\Varid{f}\mathrel{=}\Varid{thin}\;{}\<[31]%
\>[31]{}\{\mskip1.5mu \Varid{pic}\;\Varid{i}\;\Varid{y}_{0}\;{}\<[43]%
\>[43]{}\Varid{y}_{1}\mid \Varid{i}\leftarrow [\mskip1.5mu \mathrm{1}\mathinner{\ldotp\ldotp}\Varid{n}\mskip1.5mu],{}\<[62]%
\>[62]{}\Varid{y}_{0}{}\<[66]%
\>[66]{}\leftarrow \ensuremath{\Varid{genAlgT}_{\!\Varid{n}}}\;{}\<[83]%
\>[83]{}\fixatill{\Varid{i}}{\ensuremath{\mathbf{0}}{}}{\Varid{f}},\Varid{y}_{1}{}\<[112]%
\>[112]{}\leftarrow \ensuremath{\Varid{genAlgT}_{\!\Varid{n}}}\;{}\<[129]%
\>[129]{}\fixatill{\Varid{i}}{\ensuremath{\mathbf{1}}{}}{\Varid{f}}\mskip1.5mu\}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
All subfunctions \ensuremath{\fixatill{\Varid{i}}{\Varid{b}}{\Varid{f}}\mathop{:}\Conid{BoolFun}\;\Varid{n}} used in the recursive calls satisfy the induction hypothesis: \ensuremath{\Varid{spec}\;\Varid{n}\;\fixatill{\Varid{i}}{\Varid{b}}{\Varid{f}}}.
If we name the sets involved in these hypotheses \ensuremath{\fixatill{\Varid{i}}{\Varid{b}}{\Varid{xs}}} and \ensuremath{\fixatill{\Varid{i}}{\Varid{b}}{\Varid{ys}}} we can thus assume \ensuremath{\fixatill{\Varid{i}}{\Varid{b}}{\Varid{ys}}\subseteq\fixatill{\Varid{i}}{\Varid{b}}{\Varid{xs}}} and \ensuremath{\fixatill{\Varid{i}}{\Varid{b}}{\Varid{ys}}\mathrel{\ddot{\prec}}(\fixatill{\Varid{i}}{\Varid{b}}{\Varid{xs}}\mathbin{\char92 \char92 }\fixatill{\Varid{i}}{\Varid{b}}{\Varid{ys}})}.

First, the subset property: we want to prove that \ensuremath{\ensuremath{\Varid{genAlgT}_{\!\Varid{n}\mathbin{+}\mathrm{1}}}\;\Varid{f}\subseteq\ensuremath{\Varid{genAlg}_{\Varid{n}\mathbin{+}\mathrm{1}}}\;\Varid{f}}, or equivalently, \ensuremath{\forall\,\Varid{y}.\,\,(\Varid{y}\in \ensuremath{\Varid{genAlgT}_{\!\Varid{n}\mathbin{+}\mathrm{1}}}\;\Varid{f})\Rightarrow (\Varid{y}\in \ensuremath{\Varid{genAlg}_{\Varid{n}\mathbin{+}\mathrm{1}}}\;\Varid{f})}.
Let \ensuremath{\Varid{y}\in \ensuremath{\Varid{genAlgT}_{\!\Varid{n}\mathbin{+}\mathrm{1}}}\;\Varid{f}}.
We know from the specification of \ensuremath{\Varid{thin}} and the definition of \ensuremath{\ensuremath{\Varid{genAlgT}_{\!\Varid{n}\mathbin{+}\mathrm{1}}}\;\Varid{f}} that \ensuremath{\Varid{y}\mathrel{=}\Varid{pic}\;\Varid{i}\;\Varid{y}_{0}\;\Varid{y}_{1}} for some \ensuremath{\Varid{y}_{0}\in \fixatill{\Varid{i}}{\mathrm{0}}{\Varid{ys}}} and \ensuremath{\Varid{y}_{1}\in \fixatill{\Varid{i}}{\mathrm{1}}{\Varid{ys}}}.
The subset part of the induction hypothesis gives us that \ensuremath{\Varid{y}_{0}\in \fixatill{\Varid{i}}{\mathrm{0}}{\Varid{xs}}} and \ensuremath{\Varid{y}_{1}\in \fixatill{\Varid{i}}{\mathrm{1}}{\Varid{xs}}}.
Thus we can see from the definition of \ensuremath{\ensuremath{\Varid{genAlg}_{\Varid{n}\mathbin{+}\mathrm{1}}}\;\Varid{f}} that \ensuremath{\Varid{y}\in \ensuremath{\Varid{genAlg}_{\Varid{n}\mathbin{+}\mathrm{1}}}\;\Varid{f}}.

Now for the ``domination'' property we need to show that \ensuremath{\forall\,\Varid{x}\in \Varid{xs}\mathbin{\char92 \char92 }\Varid{ys}.\,\,\Varid{ys}\mathrel{\dot{\prec}}\Varid{x}} where \ensuremath{\Varid{xs}\mathrel{=}\ensuremath{\Varid{genAlg}_{\Varid{n}\mathbin{+}\mathrm{1}}}\;\Varid{f}} and \ensuremath{\Varid{ys}\mathrel{=}\ensuremath{\Varid{genAlgT}_{\!\Varid{n}\mathbin{+}\mathrm{1}}}\;\Varid{f}}.
Let \ensuremath{\Varid{x}\in \Varid{xs}\mathbin{\char92 \char92 }\Varid{ys}}.
Given the definition of \ensuremath{\Varid{xs}} it must be of the form \ensuremath{\Varid{x}\mathrel{=}\Varid{pic}\;\Varid{i}\;\Varid{x}_{0}\;\Varid{x}_{1}} where \ensuremath{\Varid{x}_{0}\in \fixatill{\Varid{i}}{\ensuremath{\mathbf{0}}{}}{\Varid{xs}}} and \ensuremath{\Varid{x}_{1}\in \fixatill{\Varid{i}}{\ensuremath{\mathbf{1}}{}}{\Varid{xs}}}.
The (second part of the) induction hypothesis provides the existence of \ensuremath{\Varid{y}_{\Varid{b}}\in \fixatill{\Varid{i}}{\Varid{b}}{\Varid{ys}}} such that \ensuremath{\Varid{y}_{\Varid{b}}\prec\Varid{x}_{\Varid{b}}}.
From these \ensuremath{\Varid{y}_{\Varid{b}}} we can build \ensuremath{\Varid{y'}\mathrel{=}\Varid{pic}\;\Varid{i}\;\Varid{y}_{0}\;\Varid{y}_{1}} as a candidate element to ``dominate'' \ensuremath{\Varid{xs}}.

We can now show that \ensuremath{\Varid{y'}\prec\Varid{x}} by polynomial algebra:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{7}{@{}>{\hspre}l<{\hspost}@{}}%
\column{16}{@{}>{\hspre}c<{\hspost}@{}}%
\column{16E}{@{}l@{}}%
\column{17}{@{}>{\hspre}c<{\hspost}@{}}%
\column{17E}{@{}l@{}}%
\column{20}{@{}>{\hspre}l<{\hspost}@{}}%
\column{23}{@{}>{\hspre}l<{\hspost}@{}}%
\column{26}{@{}>{\hspre}c<{\hspost}@{}}%
\column{26E}{@{}l@{}}%
\column{30}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{true}{}\<[E]%
\\
\>[B]{}\implies\mbox{\onelinecomment  Follows from the induction hypothesis}{}\<[E]%
\\
\>[B]{}\hsindent{3}{}\<[3]%
\>[3]{}(\Varid{y}_{0}\prec\Varid{x}_{0}){}\<[17]%
\>[17]{}\mathrel{\wedge}{}\<[17E]%
\>[23]{}(\Varid{y}_{1}\prec\Varid{x}_{1}){}\<[E]%
\\
\>[B]{}\implies\mbox{\onelinecomment  In the interval \ensuremath{(\mathrm{0},\mathrm{1})} both \ensuremath{\mathrm{1}\mathbin{-}\Varid{xP}} and \ensuremath{\Varid{xP}} are positive}{}\<[E]%
\\
\>[B]{}\hsindent{3}{}\<[3]%
\>[3]{}\mathrm{1}\mathbin{+}(\mathrm{1}\mathbin{-}\Varid{xP})\mathbin{*}\Varid{y}_{0}\mathbin{+}\Varid{xP}\mathbin{*}\Varid{y}_{1}{}\<[26]%
\>[26]{}\prec{}\<[26E]%
\>[30]{}\mathrm{1}\mathbin{+}(\mathrm{1}\mathbin{-}\Varid{xP})\mathbin{*}\Varid{x}_{0}\mathbin{+}\Varid{xP}\mathbin{*}\Varid{x}_{1}{}\<[E]%
\\
\>[B]{}\Leftrightarrow\mbox{\onelinecomment  Def. of \ensuremath{\Varid{pic}} for polynomials}{}\<[E]%
\\
\>[B]{}\hsindent{3}{}\<[3]%
\>[3]{}\Varid{pic}\;\Varid{i}\;\Varid{y}_{0}\;\Varid{y}_{1}{}\<[16]%
\>[16]{}\prec{}\<[16E]%
\>[20]{}\Varid{pic}\;\Varid{i}\;\Varid{x}_{0}\;\Varid{x}_{1}{}\<[E]%
\\
\>[B]{}\Leftrightarrow\mbox{\onelinecomment  Def. of \ensuremath{\Varid{y'}} and \ensuremath{\Varid{x}}}{}\<[E]%
\\
\>[B]{}\hsindent{7}{}\<[7]%
\>[7]{}\Varid{y'}\prec\Varid{x}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
We are not quite done, because \ensuremath{\Varid{y'}} may not be in \ensuremath{\Varid{ys}}.
It is clear from the definition of \ensuremath{\ensuremath{\Varid{genAlgT}_{\!\Varid{n}\mathbin{+}\mathrm{1}}}\;\Varid{f}} that \ensuremath{\Varid{y'}} is in the set \ensuremath{\Varid{ys'}} sent to \ensuremath{\Varid{thin}}, but it may be ``thinned away''.
But, either \ensuremath{\Varid{y'}\in \Varid{ys}\mathrel{=}\Varid{thin}\;\Varid{ys'}} in which case we take the final \ensuremath{\Varid{y}\mathrel{=}\Varid{y'}}, or there exists another \ensuremath{\Varid{y}\in \Varid{ys}} such that \ensuremath{\Varid{y}\prec\Varid{y'}} and then we get get \ensuremath{\Varid{y}\prec\Varid{x}} by transitivity.

To sum up, we have now proved that we can push a powerful \ensuremath{\Varid{thin}} step into the recursive enumeration of all cost polynomials in such a way that any minimum is guaranteed to reside in the much smaller set of polynomials thus computed.

\subsection{Memoization}
\label{sec:memo}
The call graph of \ensuremath{\ensuremath{\Varid{genAlgT}_{\!\Varid{n}}}\;\Varid{f}} is the same as the call graph of \ensuremath{\ensuremath{\Varid{genAlg}_{\Varid{n}}}\;\Varid{f}} and, as mentioned above, it can be exponentially big.
Thus, even though thinning helps in making the intermediate sets exponentially smaller, we still have one source of exponential computational complexity to tackle.
Fortunately, the same subfunctions often appear in many different nodes and this means we can save a significant amount of computation time using memoization.

The classical example of memoization is the Fibonacci function.
Naively computing \ensuremath{\Varid{fib}\;(\Varid{n}\mathbin{+}\mathrm{2})\mathrel{=}\Varid{fib}\;(\Varid{n}\mathbin{+}\mathrm{1})\mathbin{+}\Varid{fib}\;\Varid{n}} leads to exponential growth in the number of function calls.
But if we fill in a table indexed by \ensuremath{\Varid{n}} with already computed results we get can compute \ensuremath{\Varid{fib}\;\Varid{n}} in linear time.

Similarly, here we ``just'' need to tabulate the result of the calls to \ensuremath{\ensuremath{\Varid{genAlg}_{\Varid{n}}}\;\Varid{f}} so as to avoid recomputation.
The challenge is that the input we need to tabulate is now a Boolean function which is not as nicely structured as a natural number index.
Fortunately, thanks to \citet{DBLP:journals/jfp/Hinze00a}, Elliot, and others we have generic Trie-based memo functions only a hackage library away\footnote{Available on hackage as the \href{https://hackage.haskell.org/package/MemoTrie}{MemoTrie} Haskell package.}.
The \ensuremath{\Conid{MemoTrie}} library provides the \ensuremath{\Conid{Memoizable}} class and suitable instances and helper functions for most types.
We only need to provide a \ensuremath{\Conid{Memoizable}} instance for \ensuremath{\Conid{BDD}}s, and we do this using \ensuremath{\Varid{inSig}} and \ensuremath{\Varid{outSig}} from the \ensuremath{\Conid{BDD}} package (decision-diagrams).
They expose the top-level structure of a \ensuremath{\Conid{BDD}}: \ensuremath{\Conid{Sig}\;\Varid{bf}} is isomorphic to \ensuremath{\Conid{Either}\;\mathbb{B}\;(\Conid{Index},\Varid{bf},\Varid{bf})} where \ensuremath{\Varid{bf}\mathrel{=}\Conid{BDDFun}}.
We define our top-level function \ensuremath{\Varid{genAlgThinMemo}} by applying memoization to \ensuremath{\ensuremath{\Varid{genAlgT}_{\!\cdot }}}.

\subsection{Comparing polynomials}
As argued above that the key to an efficient computation of the best cost polynomials is to compare polynomials as soon as possible and throw away those which are ``uniformly worse''.
The specification of \ensuremath{\Varid{p}\prec\Varid{q}} is \ensuremath{\Varid{p}\;\Varid{x}\leq \Varid{q}\;\Varid{x}} for all \ensuremath{\mathrm{0}\leq \Varid{x}\leq \mathrm{1}} and \ensuremath{\Varid{p}\;\Varid{x}\mathbin{<}\Varid{q}\;\Varid{x}} for some \ensuremath{\mathrm{0}\mathbin{<}\Varid{x}\mathbin{<}\mathrm{1}}.
Note that \ensuremath{(\prec)} is a strict pre-order --- if the polynomials cross, neither is ``uniformly worse'' and we keep both.

If we have two polynomials \ensuremath{\Varid{p}}, and \ensuremath{\Varid{q}}, we want to know if \ensuremath{\Varid{p}\leq \Varid{q}} for all inputs in the interval \ensuremath{[\mskip1.5mu \mathrm{0},\mathrm{1}\mskip1.5mu]}.
Equivalently, we need to check if \ensuremath{\mathrm{0}\leq \Varid{q}\mathbin{-}\Varid{p}} in that interval.
As the difference is also a polynomial, we can focus our attention to locating polynomial roots in the unit interval.

\begin{figure}[htbp]
    \centering
    \begin{subfigure}[b]{0.3\textwidth}
        \includegraphics[width = \textwidth]{plots/noroot.pdf}
        \caption{No root.}
        \label{fig:noroot}
    \end{subfigure}
    \hfill
    \begin{subfigure}[b]{0.3\textwidth}
        \includegraphics[width = \textwidth]{plots/singleroot.pdf}
        \caption{Single root.}
        \label{fig:singleroot}
    \end{subfigure}
    \hfill
    \begin{subfigure}[b]{0.3\textwidth}
        \includegraphics[width = \textwidth]{plots/doubleroot.pdf}
        \caption{Double root.}
        \label{fig:doubleroot}
    \end{subfigure}
      \caption{To compare two polynomials \ensuremath{\Varid{p}} and \ensuremath{\Varid{q}} we use root counting for \ensuremath{\Varid{q}\mathbin{-}\Varid{p}} and there are the three main cases to consider.}
    \label{fig:roots}
\end{figure}
If there are no roots (Fig.~\ref{fig:noroot}) in the unit interval, the polynomial stays on ``one side of zero'' and we just need to check the sign of the polynomial at any point.
If there is at least one single-root (Fig.~\ref{fig:singleroot}), the original polynomials cross and we return \ensuremath{\Conid{Nothing}}.
Similarly for triple-roots or roots of any odd order.
Finally, if the polynomial only has roots of even order (some double-roots, or quadruple-roots, etc.\ as in Fig.~\ref{fig:doubleroot}) the polynomial stays on one side of zero, and we can check a few points to see what side that is.
(If the number of distinct roots is \ensuremath{\Varid{r}} we check up to \ensuremath{\Varid{r}\mathbin{+}\mathrm{1}} points to make sure at least one will be non-zero and thus tell us on which side of zero the polynomial lies.)

Thus, the top-level of the polynomial partial order implementation is as follows:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{10}{@{}>{\hspre}l<{\hspost}@{}}%
\column{12}{@{}>{\hspre}l<{\hspost}@{}}%
\column{18}{@{}>{\hspre}l<{\hspost}@{}}%
\column{42}{@{}>{\hspre}l<{\hspost}@{}}%
\column{57}{@{}>{\hspre}c<{\hspost}@{}}%
\column{57E}{@{}l@{}}%
\column{61}{@{}>{\hspre}l<{\hspost}@{}}%
\column{70}{@{}>{\hspre}l<{\hspost}@{}}%
\column{89}{@{}>{\hspre}l<{\hspost}@{}}%
\column{101}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\Varid{cmpPoly}\mathbin{::}(\Conid{Ord}\;\Varid{a},\Conid{Field}\;\Varid{a})\Rightarrow \Conid{Poly}\;\Varid{a}\,\to\,\Conid{Poly}\;\Varid{a}\,\to\,\Conid{Maybe}\;\Conid{Ordering}{}\<[E]%
\\
\>[B]{}\Varid{cmpPoly}\;\Varid{p}\;\Varid{q}\mathrel{=}\Varid{cmpZero}\;(\Varid{q}\mathbin{-}\Varid{p}){}\<[E]%
\\[\blanklineskip]%
\>[B]{}\Varid{cmpZero}\mathbin{::}(\Conid{Ord}\;\Varid{a},\Conid{Field}\;\Varid{a})\Rightarrow \Conid{Poly}\;\Varid{a}\,\to\,\Conid{Maybe}\;\Conid{Ordering}{}\<[E]%
\\
\>[B]{}\Varid{cmpZero}\;\Varid{p}{}\<[12]%
\>[12]{}\mid \Varid{isZero}\;\Varid{p}{}\<[57]%
\>[57]{}\mathrel{=}{}\<[57E]%
\>[61]{}\Conid{Just}\;\Conid{EQ}{}\<[E]%
\\
\>[12]{}\mid \Varid{all}\;\Varid{even}\;(\Varid{numRoots'}\;\Varid{p}){}\<[57]%
\>[57]{}\mathrel{=}{}\<[57E]%
\>[61]{}\mathbf{if}\;{}\<[70]%
\>[70]{}\Varid{any}\;(\mathrm{0}\mathbin{<})\;\Varid{vals}\;{}\<[89]%
\>[89]{}\mathbf{then}\;\Conid{Just}\;\Conid{LT}{}\<[E]%
\\
\>[61]{}\mathbf{else}\;\mathbf{if}\;{}\<[70]%
\>[70]{}\Varid{any}\;(\mathrm{0}\mathbin{>})\;\Varid{vals}\;{}\<[89]%
\>[89]{}\mathbf{then}\;\Conid{Just}\;\Conid{GT}{}\<[E]%
\\
\>[61]{}\mathbf{else}\;\Conid{Just}\;\Conid{EQ}{}\<[E]%
\\
\>[12]{}\mid \Varid{otherwise}{}\<[57]%
\>[57]{}\mathrel{=}{}\<[57E]%
\>[61]{}\Conid{Nothing}{}\<[101]%
\>[101]{}\mbox{\onelinecomment  incomparable}{}\<[E]%
\\
\>[B]{}\hsindent{3}{}\<[3]%
\>[3]{}\mathbf{where}\;{}\<[10]%
\>[10]{}\Varid{r}{}\<[18]%
\>[18]{}\mathrel{=}\Varid{length}\;(\Varid{numRoots'}\;\Varid{p}){}\<[42]%
\>[42]{}\mbox{\onelinecomment  the number of distinct roots}{}\<[E]%
\\
\>[10]{}\Varid{rp2}{}\<[18]%
\>[18]{}\mathrel{=}\Varid{fromIntegral}\;(\Varid{r}\mathbin{+}\mathrm{2}){}\<[E]%
\\
\>[10]{}\Varid{points}{}\<[18]%
\>[18]{}\mathrel{=}[\mskip1.5mu \Varid{i}\mathbin{/}\Varid{rp2}\mid \Varid{i}\leftarrow \Varid{take}\;(\Varid{r}\mathbin{+}\mathrm{1})\;(\Varid{iterate}\;(\Varid{one}\mathbin{+})\;\Varid{one})\mskip1.5mu]{}\<[E]%
\\
\>[10]{}\Varid{vals}{}\<[18]%
\>[18]{}\mathrel{=}\Varid{map}\;(\Varid{evalP}\;\Varid{p})\;\Varid{points}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
To make this work, we ``just'' need to implement the root-counting functions \ensuremath{\Varid{numRoots}} and \ensuremath{\Varid{numRoots'}}:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\Varid{numRoots}\mathbin{::}(\Conid{Ord}\;\Varid{a},\Conid{Field}\;\Varid{a})\Rightarrow \Conid{Poly}\;\Varid{a}\,\to\,\Conid{Int}{}\<[E]%
\\
\>[B]{}\Varid{numRoots}\mathrel{=}\Varid{sum}\mathbin{\circ}\Varid{numRoots'}{}\<[E]%
\\[\blanklineskip]%
\>[B]{}\Varid{numRoots'}\mathbin{::}(\Conid{Ord}\;\Varid{a},\Conid{Field}\;\Varid{a})\Rightarrow \Conid{Poly}\;\Varid{a}\,\to\,[\mskip1.5mu \Conid{Int}\mskip1.5mu]{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
The second function computes real root multiplicities: \ensuremath{\Varid{numRoots'}\;\Varid{p}\mathrel{=}[\mskip1.5mu \mathrm{1},\mathrm{3}\mskip1.5mu]} means \ensuremath{\Varid{p}} has one single and one triple root in the open interval \ensuremath{(\mathrm{0},\mathrm{1})}.
From this we get that \ensuremath{\Varid{p}} has \ensuremath{\mathrm{2}\mathrel{=}\Varid{length}\;[\mskip1.5mu \mathrm{1},\mathrm{3}\mskip1.5mu]} distinct real roots and \ensuremath{\mathrm{4}\mathrel{=}\Varid{sum}\;[\mskip1.5mu \mathrm{1},\mathrm{3}\mskip1.5mu]} real roots if we count multiplicities.
We will not provide all the code here, because that would take us too far from the main topic of the paper, but we will illustrate the main algorithms and concepts.

\subsection{Isolating real roots and Descartes rule of signs}

First out is Yun's algorithm \citep{10.1145/800205.806320} for square-free factorisation: given a polynomial \ensuremath{\Varid{p}} it computes a list of polynomial factors \(p_i\), each of which only has single-roots, and such that \(p = C \prod_{i} {p_i}^i\).
Note the exponent \ensuremath{\Varid{i}}: the factor \ensuremath{\Varid{p}_{2}}, for example, appears squared in \ensuremath{\Varid{p}}.
If \ensuremath{\Varid{p}} only has single-roots, the list from Yun's algorithm has just one element, \ensuremath{\Varid{p}_{1}}, but in any case we get a finite list of polynomials, each of which is ``square-free''.%
\footnote{Yun's algorithm is built around repeated computation of the polynomial greatest common divisor of \ensuremath{\Varid{p}} and its derivative, \ensuremath{\Varid{p'}}.
  %
See the associated code for the details.}

Second in line is Descartes rule of signs which can be used to determine the number of real zeros of a polynomial function.
It tells us that the number of positive real zeros in a polynomial function \ensuremath{\Varid{f}} is the same, or less than by an even number, as the number of changes in the sign of the coefficients.
Together with some polynomial transformations, this is used to count the zeroes in the interval \([0,1)\).

If the rule gives zero or one, we are done: we have isolated an interval \([0,1)\) with either no root or exactly one root.
For our use case we don't need to know the actual root, just if it exists in the interval or not.

If the rule gives more than one, we don't quite know the exact number of roots yet (only an upper bound).
In that case we subdivide the interval into the lower \([0,1/2)\) and upper \([1/2, 1)\) halves.
Fortunately the polynomial coefficients can be transformed to make the domain the unit interval again so that we can call ourselves recursively.
After a finite number of steps, this bisection terminates and we get a list of disjoint isolating intervals where we know there is exactly one root in each.

Combining Yun and Descartes, we implement our ``root counter'', and thus our partial order on polynomials.

\section{Results}
Using the method from the previous section we can now calculate the level-$p$-complexity of Boolean functions with our function \ensuremath{\Varid{genAlgThinMemo}}.
First we return to our example from the beginning (\ensuremath{\Varid{sim}_{5}}), where we get several polynomials which are optimal in different intervals.
Then, we calculate the level-$p$-complexity for \ensuremath{\Varid{maj}_{3}^2} which is lower than the proposed result in \citep{jansson2022level}, which means that our current method is better.

\subsection{Level-$p$-complexity for \ensuremath{\Varid{sim}_{5}}}
\label{sec:fAC}
When we run \ensuremath{\Varid{genAlgThinMemo}\;\mathrm{5}\;\Varid{sim}_{5}} it returns a set of four polynomials:
\begin{align*}
        \{&P_1(p) = 2 + 6 p - 10 p^2 + 8 p^3 - 4 p^4,  &P_2(p) &= 4 - 2 p - 3 p^2  + 8 p^3 - 2 p^4,\\
        &P_3(p) = 5 - 8 p + 9 p^2 - 2 p^4,&P_4(p) &= 5 - 8 p + 8 p^2 \}
\end{align*}
We don't compute their intersection points, just that they do intersect in the unit interval.
The four polynomials were shown already in Fig.~\ref{fig:4polys}.
The level-$p$-complexity for \ensuremath{\Varid{sim}_{5}} is the piecewise polynomial, pointwise minimum, of these four, with two different polynomials in different intervals: $D_p(\ensuremath{\Varid{sim}_{5}}) = P_4(p)$ for $p \in [\approx0.356,\approx0.644]$ and $D_p(\ensuremath{\Varid{sim}_{5}}) = P_1(p)$ in the rest of the unit interval.
As seen in Figure \ref{fig:ACDp}, the level-$p$-complexity has two maxima.
\begin{figure}[htbp]
        \centering
        \includegraphics[width = 0.6\textwidth]{plots/ACDp.pdf}
        \caption{Level-\ensuremath{\Varid{p}}-complexity of \ensuremath{\Varid{sim}_{5}}, where the dots show the intersections of the costs of the decision trees.}
        \label{fig:ACDp}
\end{figure}

\begin{comment}
\TODO{more of a discussion point, rewrite and move to conclusions with references to this section, or consider structure}
This example illustrates limitations of the method when it comes to intersections of the polynomials.
In this case our method returns a set of four polynomials, and it does not specify their intersection points, just that they do intersect in the interval.
Mathematica is then used to calculate the level-$p$-complexity from these four polynomials.
It would be desirable to extend our method to include this calculation, especially since we are already calculating roots and intersections, just not precisely enough.
However, it is not strictly needed since Mathematica does this in a simple way.
$$D_p(f) = \begin{cases}
        P_1(p)= 2 + 6 p - 10 p^2 + 8 p^3 - 4 p^4, &p \in [0,0.356]\\
        P_4(p) = 5 - 8 p + 8 p^2, &p \in [0.356,0.644]\\
        P_1(p)= 2 + 6 p - 10 p^2 + 8 p^3 - 4 p^4, &p \in [0.644,1]
    \end{cases}$$
\end{comment}

\subsection{Level-$p$-complexity for \ensuremath{\Varid{maj}_{3}^2}}
Running \ensuremath{\Varid{genAlgThinMemo}\;\mathrm{9}\;\Varid{maj}_{3}^2} we get \ensuremath{\{\mskip1.5mu \Conid{P}\;[\mskip1.5mu \mathrm{4},\mathrm{4},\mathrm{6},\mathrm{9},\mathbin{-}\mathrm{61},\mathrm{23},\mathrm{67},\mathbin{-}\mathrm{64},\mathrm{16}\mskip1.5mu]\mskip1.5mu\}}, which means that the expected cost (\(P_*\)) of the best decision tree (\ensuremath{\ensuremath{\Conid{T}_{\mathbin{*}}}}) is
$$P_*(p) = 4 + 4 p + 6 p^2 + 9 p^3 - 61 p^4 + 23 p^5 + 67 p^6 - 64 p^7 + 16 p^8\,.$$
This can be compared to the decision tree (that we call \ensuremath{\ensuremath{\Conid{T}_{\Varid{t}}}}) conjectured in \citep{jansson2022level} to be the best.
Its expected cost is slightly higher (thus worse):
$$P_t(p) = 4 + 4 p + 7 p^2 + 6 p^3 - 57 p^4 + 20 p^5 + 68 p^6 - 64 p^7 + 16 p^8\,.$$
The expected costs for decision trees \ensuremath{\ensuremath{\Conid{T}_{\mathbin{*}}}} and \ensuremath{\ensuremath{\Conid{T}_{\Varid{t}}}} can be seen in Figure~\ref{fig:itermajalgs2}.
\begin{figure}
        \centering
        \includegraphics[width = 0.8\textwidth]{plots/itermajalgs2.pdf}
        \caption{Expected costs of the two different decision trees.
          %
          Because they are very close we also show their difference in Fig.~\ref{fig:itermajalgsdiff2}.}
        \label{fig:itermajalgs2}
\end{figure}
Comparing the two polynomials using \ensuremath{\Varid{cmpPoly}\;\ensuremath{\Conid{P}_{\mathbin{*}}}\;\ensuremath{\Conid{P}_{\Varid{t}}}} shows that the new one has strictly lower expected cost than the one from the thesis.
The difference, which factors to exactly \(p^2(1-p)^2(1-p+p^2)\), is illustrated in Fig.~\ref{fig:itermajalgsdiff2}, and we note that it is non-negative in the whole interval.
\begin{figure}
        \centering
        \includegraphics[width = 0.9\textwidth]{plots/itermajalgsdiff2.pdf}
        \caption{Difference between the expected costs of \ensuremath{\ensuremath{\Conid{T}_{\Varid{t}}}} and \ensuremath{\ensuremath{\Conid{T}_{\mathbin{*}}}}.}
        \label{fig:itermajalgsdiff2}
\end{figure}

The value of the polynomials at the endpoints is 4 and the maximum of \ensuremath{\ensuremath{\Conid{P}_{\mathbin{*}}}} is $\approx6.14$ compared to the maximum of \ensuremath{\ensuremath{\Conid{P}_{\Varid{t}}}} which is $\approx6.19$.
The conjecture in \citep{jansson2022level} is thus false and the correct formula for the level-$p$-complexity of \ensuremath{\Varid{maj}_{3}^2} is \ensuremath{\ensuremath{\Conid{P}_{\mathbin{*}}}}.
At the time of publication of \citep{jansson2022level} it was believed that sifting through all the possible decision trees would be intractable.
Fortunately, using a combination of thinning, memoization, and exact comparison of polynomials, it is now possible to compute the correct complexity in less than a second on the author's laptop.

\section{Conclusions}

This paper describes a Haskell library for computing level-$p$-complexity of Boolean functions, and applies it to two-level iterated majority (\ensuremath{\Varid{maj}_{3}^2}).
The problem specification is straightforward: generate all possible decision trees, compute their expected cost polynomials, and select the best ones.
The implementation is more of a challenge because of two sources of exponential computational cost: an exponential growth in the set of decision trees and an exponential growth in the size of the recursive call graph (the collection of subfunctions).
The library uses thinning to tackle the first and memoization to handle the second source of inefficiency.
In combination with efficient data structures (binary decision diagrams for the Boolean function input, sets of polynomials for the output) this enables computing the level-\ensuremath{\Varid{p}}-complexity for our target example \ensuremath{\Varid{maj}_{3}^2} in less than a second.

From the mathematics point of view the strength of the methods used in this paper to compute the level-\ensuremath{\Varid{p}}-complexity is that we can get a correct result to something which is very hard to calculate by hand.
From a computer science point of view the paper is an instructive example of how a combination of algorithmic and symbolic tools can tame a doubly exponential computational cost.

The library uses type-classes for separation of concerns: the actual implementation type for Boolean functions (the input) is abstracted over by the \ensuremath{\Conid{BoFun}} class; and the corresponding type for the output is modelled by the \ensuremath{\Conid{TreeAlg}} class.
We also use our own class \ensuremath{\Conid{Thinnable}} for thinning (and pre-orders), and the \ensuremath{\Conid{Memoizable}} class from hackage.
This means that our main function has the following type:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{20}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[B]{}\Varid{genAlgThinMemo}\mathbin{::}{}\<[20]%
\>[20]{}(\Conid{BoFun}\;\Varid{bf},\Conid{Memoizable}\;\Varid{bf},\Conid{TreeAlg}\;\Varid{a},\Conid{Thinnable}\;\Varid{a})\Rightarrow {}\<[E]%
\\
\>[20]{}\mathbb{N}\,\to\,\Varid{bf}\,\to\,\Conid{Set}\;\Varid{a}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
All the Haskell code is available on GitHub\footnote{The paper repository is at \url{https://github.com/juliajansson/BoFunComplexity}.} and parts of it has been reproduced in Agda to check some of the stronger invariants.
One direction of future work is to complete the Agda formalisation so that we can provide a formally verified library, perhaps helped by \citet{swierstra_2022, 10.1145/3547636}.

The set of polynomials we compute are all incomparable in the pre-order and, together with the thinning relation this means that we actually compute what is called a Pareto front from economics: a set of solutions where no objective can be improved without sacrificing at least one other objective.
It would be interesting to explore this in more detail and to see what the overlap is between thinning as an algorithm design method and different concepts of optimality from economics.

The computed level-$p$-complexity for \ensuremath{\Varid{maj}_{3}^2} is better than the result conjectured in \citep{jansson2022level}, and the library allows easy exploration of other Boolean functions.
In the future it would be interesting to try to compute the level-\ensuremath{\Varid{p}}-complexity of iterated majority on 3 levels (27 bits).

\section*{Acknowledgments}
The authors would like to extend their gratitude to Tim Richter and Jeremy Gibbons for taking their time to give valuable feedback on the first draft.
The work presented in this paper heavily relies on free software, among others on GHC, Agda, Haskell, git, Emacs, \LaTeX\ and on the Ubuntu operating system, Mathematica, and Visual Studio Code.
It is our pleasure to thank all developers of these excellent products.

\subsection*{Conflicts of Interest}
None.

redpajama_set_name: RedPajamaArXiv


On top of the gravel we laid a DPM plastic which was to go below the polystyrene sheets. We had to run to collect concrete blocks and block cut-offs to hold down the DPM from waving around and flying away in the wind before laying the polystyrene with blocks on top too.
Next we bent the D12 steel reinforcing rods down, as well as cutting and bending new D12 rods that would act as perimeter rods. On top of the bars we laid the steel mesh on top, and cut to size for the flooring. We then tied it all together using steel ties and nibs.


Kaspersky Free. Information and Download of Kaspersky Lab Kaspersky Free at 2000Shareware.
Based on Kaspersky Lab award-winning technologies, Kaspersky Free provides truly reliable protection against suspicious or malicious files and programs, and alerts you to potentially malicious websites - so you can surf in the Internet safely.
By simply visiting a website or opening an email you can become a victim of a phishing attack that tries to steal your money or identity. Our proven Anti-Phishing technology securely protects you against accessing phishing websites, scans all incoming and outcoming emails and blocks harmful content - so your personal information remains safe and sound.
Kaspersky Free will not let hackers take control over you. Even if your computer is blocked by a Trojan that restricts access to it and demands money to lift restrictions, our Anti-Blocker technology will stop this dangerous process and launch necessary treatment procedures.
Kaspersky Free protects your computer here and now, without stops and delays, using real-time data from the cloud about the latest known threats as well as delivering proactive protection from unknown dangers. Plus free automatic updates and upgrades ensure you always have the latest version of the product all without slowing down your computer!
Kaspersky Free Free Download - 2000 Shareware periodically updates software information of Kaspersky Free from the publisher, so some information may be slightly out-of-date. You should confirm all information before relying on it. Software piracy is theft, Using Kaspersky Free crack, password, registration codes, key generators, serial numbers is illegal.
Release Notes: Kaspersky Free provides the following new features: There is now protection against infection while the operating system is being restarted. Added notification from Web Anti-Virus regarding pages containing adware or legitimate software that can be used by criminals to damage your computer.
We are frequently affected by programs and scripts, to get rid of this Kaspersky offers the best solution, you do not have to rush to service center anymore.
Polycom Announces Definitive Agreement To Divest Its Enterprise Wireless Voice Solutions Business For Approximately $110 Million To Sun Capital Partners Affiliate by Polycom, Inc.
Digital River Unveils A New Online Portal That Gives Developers Unprecedented Access To Cloud Commerce APIs by Digital River, Inc.