tame/design/tpl/sec/class.tex

% The TAME Programming Language Classification System
%
%  Copyright (C) 2021 Ryan Specialty Group, LLC.
%
%  Licensed under the Creative Commons Attribution-ShareAlike 4.0
%  International License.
%%

\section{Classification System}\seclabel{class}
\index{classification|textbf}
A \dfn{classification} is a user-defined abstraction that describes
  (``classifies'') arbitrary data.
Classifications can be used as predicates, generating functions, and can be
  composed into more complex classifications.
Nearly all conditions in \tame{} are specified using classifications.

\index{first-order logic!sentence}
\index{classification!coupling}
All classifications represent \dfn{first-order sentences}---%
  that is,
    they contain no \dfn{free variables}.
Intuitively,
  this means that all variables within a~classification are
  \dfn{tightly coupled} to the classification itself.
This limitation is mitigated through use of the template system.

\begin{axiom}[Classification Introduction]\axmlabel{class-intro}
\indexsym\Classify{classification}
\indexsym\gamma{classification, yield}
\index{classification!index set}
\index{index set!classification}
\index{classification!classify@\xmlnode{classify}}
\index{classification!as@\xmlattr{as}}
\index{classification!yields@\xmlattr{yields}}
\todo{Symbol in place of $=$ here ($\equiv$ not appropriate).}
\begin{subequations}
\begin{gather}
\begin{alignedat}{3}
    &\xml{<classify as="$c$" }&&\xml{yields="$\gamma$" desc}&&\xml{="$\_$"
          $\alpha$>}\label{eq:xml-classify} \\
    &\quad \MFam{M^0}jJkK   &&\VFam{v^0}jJ   &&\quad s^0    \\[-4mm]
    &\quad \quad\vdots      &&\quad\vdots    &&\quad \vdots \\
    &\quad \MFam{M^l}jJkK   &&\VFam{v^m}jJ   &&\quad s^n    \\[-3mm]
    &\xml{</classify>}
      % NB: This -50mu needs adjustment if you change the alignment above!
      &&\mspace{-50mu}= \Classify^c_\gamma\left(\odot,M,v,s\right),
\end{alignedat}
\end{gather}

\noindent
where

\indexsym\emptystr{empty string}
\index{empty string (\ensuremath\emptystr)}
\begin{align}
    J &\subset\Int \neq\emptyset, \\
    \forall{j\in J}\Big(K_j &\subset\Int \neq\emptyset\Big), \\
    \forall{k}\Big(M^k &: J \rightarrow K_{j\in J} \rightarrow \Bool\Big),
                                            \label{eq:class-matrix} \\
    \forall{k}\Big(v^k &: J \rightarrow \Bool\Big), \\
    \forall{k}\Big(s^k &\in\Bool\Big), \\
    \alpha &\in\Set{\emptystr,\, \texttt{any="true"}}, \label{eq:xml-any-domain}
\end{align}

\noindent
and the monoid~$\odot$ is defined as

\indexsym\odot{classification, monoid}
\index{classification!any@\xmlattr{any}}
\index{classification!monoid|(}
\begin{equation}\label{eq:classify-rel}
  \odot = \begin{cases}
        \Monoid\Bool\land\true &\alpha = \emptystr,\\
        \Monoid\Bool\lor\false &\alpha = \texttt{any="true"}.
      \end{cases}
\end{equation}
\end{subequations}
\end{axiom}


% This TODO was the initial motivation for this paper!
\todo{Emphasize index sets, both relationships and nonempty.}
We use a $4$-tuple $\Classify\left(\odot,M,v,s\right)$ to represent a
  $\odot_1$-classification
    (a classification with the binary operation $\land$ or~$\lor$)
  consisting of a combination of matrix~($M$), vector~($v$), and
    scalar~($s$) matches,
      rendered above in columns.\footnote{%
        The symbol~$\odot$ was chosen since the binary operation for a monoid
          is~$\monoidop$
            (see \secref{monoids})
          and~$\odot$ looks vaguely like~$(\monoidop)$,
            representing a portion of the monoid triple.}
A $\land$-classification is pronounced ``conjunctive classification'',
  and $\lor$ ``disjunctive''.\footnote{%
    \index{classification!terminology history}
    Conjunctive and disjunctive classifications used to be referred to,
      respectively,
      as \dfn{universal} and \dfn{existential},
        referring to fact that
          $\forall\Set{a_0,\ldots,a_n}(a) \equiv a_0\land\ldots\land a_n$,
            and similarly for $\exists$.
    This terminology has changed since all classifications are in fact
      existential over their matches' index sets,
        and so the terminology would otherwise lead to confusion.}

The variables~$c$ and~$\gamma$ are required in~\tame{} but are both optional
  in our notation~$\Classify^c_\gamma$,
    and can be used to identify the two different data representations of
    the classification.\footnote{%
      \xpath{classify/@yields} is optional in the grammar of \tame{},
        but the compiler will generate one for us if one is not provided.
      As such,
        we will for simplicity consider it to be required here.}

$\alpha$~serves as a placeholder for an optional \xml{any="true"},
  with $\emptystr$~representing the empty string in~\eqref{eq:xml-any-domain}.
Note the wildcard variable matching \xmlattr{desc}---%
  its purpose is only to provide documentation.

\begin{corollary}[$\odot$ Commutative Monoid]\corlabel{odot-monoid}
\index{classification!commutativity|(}
  $\odot$ is a commutative monoid in \axmref{class-intro}.
\end{corollary}
\begin{proof}
  By \axmref{class-intro},
    $\odot$ must be a monoid.
  Assume $\alpha=\emptystr$.
  Then,
    $\odot = \Monoid\Bool\land\true$,
      which is proved by \lemref{monoid-land}.
  Next, assume $\alpha=\texttt{any="true"}$.
  Then,
    $\odot = \Monoid\Bool\lor\false$,
      which is proved by \lemref{monoid-land}.
\end{proof}

While \axmref{class-intro} seems to imply an ordering to matches,
  users of the language are free to specify matches in any order
    and the compiler will rearrange matches as it sees fit.
\index{compiler!classification commutativity}
This is due to the commutativity of~$\odot$ as proved by
  \corref{odot-monoid},
    and not only affords great ease of use to users of~\tame{},
      but also great flexibility to compiler writers.
\index{classification!commutativity|)}

For notational convenience,
  we will let

\index{classification!monoid|)}
\begin{equation}
\begin{aligned}
  \Classifyland(M,v,s)
    &= \Classify\left(\Monoid\Bool\land\true,M,v,s\right), \\
  \Classifylor(M,v,s)
    &= \Classify\left(\Monoid\Bool\lor\true,M,v,s\right). \\
\end{aligned}
\end{equation}


\def\cpredmatseq{{M^0_j}_k \monoidops {M^l_j}_k}
\def\cpredvecseq{v^0_j\monoidops v^m_j}
\def\cpredscalarseq{s^0\monoidops s^n}


\begin{axiom}[Classification-Predicate Equivalence]\axmlabel{class-pred}
\index{classification!as predicate}
  Let $\Classify^c_\gamma\left(\Monoid\Bool\monoidop e,M,v,s\right)$ be a
    classification by~\axmref{class-intro}.
  We then have the first-order sentence
  \begin{equation*}
    c \equiv
      {} \Exists{j\in J}{\Exists{k\in K_j}\cpredmatseq\monoidop\cpredvecseq}
        \monoidop\cpredscalarseq.
  \end{equation*}
\end{axiom}


\begin{axiom}[Classification Yield]\axmlabel{class-yield}
\indexsym\Gamma{classification, yield}
\index{classification!yield (\ensuremath\gamma, \ensuremath\Gamma)}
  Let $\Classify^c_\gamma\left(\Monoid\Bool\monoidop e,M,v,s\right)$ be a
    classification by~\axmref{class-intro}.
  Then,

  \begin{subequations}
  \begin{align}
    r &= \begin{cases}
           2 &M\neq\emptyset, \\
           1 &M=\emptyset \land v\neq\emptyset, \\
           0 &M\union v = \emptyset,
         \end{cases} \\
    \displaybreak[0]
    \exists{j\in J}\Big(\exists{k\in K_j}\Big(
      \Gamma^2_{j_k} &= \cpredmatseq\monoidop\cpredvecseq\monoidop\cpredscalarseq
    \Big)\Big), \\
    %
    \exists{j\in J}\Big(
      \Gamma^1_j &= \cpredvecseq\monoidop\cpredscalarseq
    \Big), \\
    %
    \Gamma^0 &= \cpredscalarseq. \\
    %
    \gamma &= \Gamma^r.
  \end{align}
  \end{subequations}
\end{axiom}

\begin{theorem}[Classification Composition]\thmlabel{class-compose}
\index{classification!composition|(}
  Classifications may be composed to create more complex classifications
    using the classification yield~$\gamma$ as in~\axmref{class-yield}.
  This interpretation is equivalent to \axmref{class-pred} by
  \begin{equation}
    c \equiv \Exists{j\in J}{
               \Exists{k\in K_j}{\Gamma^2_{j_k}}
               \monoidop \Gamma^1_j
             }
             \monoidop \Gamma^0.
  \end{equation}
\end{theorem}

\def\eejJ{\equiv \exists{j\in J}\Big(}

\begin{proof}
  Expanding each~$\Gamma$ in \axmref{class-yield},
    we have

  \begin{alignat*}{3}
    c &\eejJ\Exists{k\in K_j}{\Gamma^2_{j_k}}
              \monoidop \Gamma^1_j
            \Big)
            \monoidop \Gamma^0
        &&\text{by \axmref{class-yield}} \\
      %
      &\eejJ\exists{k\in K_j}\Big(
              \cpredmatseq \monoidop \cpredvecseq \monoidop \cpredscalarseq
            \Big) \\
      &\hphantom{\eejJ}\;\cpredvecseq \monoidop \cpredscalarseq \Big)
                \monoidop \cpredscalarseq, \\
      %
      &\eejJ\exists{k\in K_j}\Big(\cpredmatseq\Big)
            \monoidop \cpredvecseq \monoidop \cpredscalarseq \\
      &\hphantom{\eejJ}\;\cpredvecseq \monoidop \cpredscalarseq \Big)
                \monoidop \cpredscalarseq,
        &&\text{by \dfnref{quant-conn}} \\
      %
      &\eejJ\exists{k\in K_j}\Big(\cpredmatseq\Big)
        &&\text{by \dfnref{prop-taut}} \\
      &\hphantom{\eejJ}\;\cpredvecseq \monoidop \cpredscalarseq \Big)
                \monoidop \cpredscalarseq, \\
      %
      &\eejJ\exists{k\in K_j}\Big(\cpredmatseq\Big)
        &&\text{by \dfnref{quant-conn}} \\
      &\hphantom{\eejJ}\;\cpredvecseq\Big) \monoidop \cpredscalarseq
                \monoidop \cpredscalarseq, \\
      %
      &\eejJ\exists{k\in K_j}\Big(\cpredmatseq\Big)
        &&\text{by \dfnref{prop-taut}} \\
      &\hphantom{\eejJ}\;\cpredvecseq\Big)
                \monoidop \cpredscalarseq.
        \tag*{\qedhere} \\
  \end{alignat*}
\end{proof}
\index{classification!composition|)}


\begin{lemma}[Classification Predicate Vacuity]\lemlabel{class-pred-vacu}
\index{classification!vacuity|(}
  Let $\Classify^c_\gamma\left(\Monoid\Bool\monoidop e,\emptyset,\emptyset,\emptyset\right)$
    be a classification by~\axmref{class-intro}.
  $\odot$ is a monoid by \corref{odot-monoid}.
  Then $c \equiv \gamma \equiv e$.
\end{lemma}
\begin{proof}
  First consider $c$.
  \begin{alignat*}{3}
    c &\equiv \Exists{j\in J}{\Exists{k}{e}\monoidop e} \monoidop e
        \qquad&&\text{by \dfnref{monoid-seq}} \label{p:cri-c} \\
      &\equiv \Exists{j\in J}{e \monoidop e} \monoidop e
        &&\text{by \dfnref{quant-elim}} \\
      &\equiv \Exists{j\in J}{e} \monoidop e
        &&\text{by \ref{eq:monoid-identity}} \\
      &\equiv e \monoidop e
        &&\text{by \dfnref{quant-elim}} \\
      &\equiv e.
        &&\text{by \ref{eq:monoid-identity}}
  \end{alignat*}

  For $\gamma$,
    we have $r=0$ by \axmref{class-yield},
    and so by similar steps as~$c$,
      $\gamma=\Gamma^r=e$.
  Therefore $c\equiv e$.
\end{proof}


\begin{figure}[ht]
  \begin{alignat*}{3}
    \begin{aligned}
      \xml{<classify }&\xml{as="always" yields="alwaysTrue"} \xmlnl
                      &\xml{desc="Always true" />}
    \end{aligned}
      \quad&=\quad
      \Classifyland^\texttt{always}_\texttt{alwaysTrue}
        &&\left(\emptyset,\emptyset,\emptyset\right). \\
    %
    \begin{aligned}
      \xml{<classify }&\xml{as="never" yields="neverTrue"} \xmlnl
                      &\xml{any="true"} \xmlnl
                      &\xml{desc="Never true" />}
    \end{aligned}
      \quad&=\quad
      \Classifylor^\texttt{never}_\texttt{neverTrue}
        &&\left(\emptyset,\emptyset,\emptyset\right).
  \end{alignat*}
  \caption{\tameclass{always} and \tameclass{never} from package
             \tamepkg{core/base}.}
  \label{fig:always-never}
\end{figure}

\spref{fig:always-never} demonstrates \lemref{class-pred-vacu} in the
  definitions of the classifications \tameclass{always} and
  \tameclass{never}.
These classifications are typically referenced directly for clarity rather
  than creating other vacuous classifications,
    encapsulating \lemref{class-pred-vacu}.
\index{classification!vacuity|)}


\begin{theorem}[Classification Rank Independence]\thmlabel{class-rank-indep}
\index{classification!rank|(}
  Let $\odot=\Monoid\Bool\monoidop e$.
  Then,
  \begin{equation}
    \Classify_\gamma\left(\odot,M,v,s\right)
      \equiv \Classify\left(
        \odot,
        \Classify_{\gamma'''}\left(\odot,M,\emptyset,\emptyset\right),
        \Classify_{\gamma''}\left(\odot,\emptyset,v,\emptyset\right),
        \Classify_{\gamma'}\left(\odot,\emptyset,\emptyset,s\right)
      \right).
  \end{equation}
\end{theorem}

\begin{proof}
  First,
    by \axmref{class-yield},
    observe these special cases following from \lemref{class-pred-vacu}:
  \begin{equation}
  \begin{alignedat}{3}
    \Gamma'''^2 &= \cpredmatseq, \qquad&&\text{assuming $v\union s=\emptyset$} \\
    \Gamma''^1 &= \cpredvecseq,        &&\text{assuming $M\union s=\emptyset$} \\
    \Gamma'^0 &= \cpredscalarseq.      &&\text{assuming $M\union v=\emptyset$}
  \end{alignedat}
  \end{equation}

  By \thmref{class-compose},
    we must prove
  \begin{multline}\label{eq:rank-indep-goal}
    \Exists{j\in J}{
        \Exists{k\in K_j}{\cpredmatseq}
        \monoidop \cpredvecseq
      }
      \monoidop \cpredscalarseq \\
    \equiv c \equiv
    \Exists{j\in J}{
        \Exists{k\in K_j}{\gamma'''_{j_k}}
        \monoidop \gamma''_j
      }
      \monoidop \gamma'.
  \end{multline}

  By \axmref{class-yield},
    we have $r'''=2$, $r''=1$, and $r'=0$,
    and so $\gamma'''=\Gamma'''^2$,
      $\gamma''=\Gamma''^1$,
      and $\gamma'=\Gamma'^0$.
  By substituting these values in~\ref{eq:rank-indep-goal},
    the theorem is proved.
\end{proof}
\index{classification!rank|)}

These definitions may also be used as a form of pattern matching to look up
  a corresponding variable.
For example,
  if we have $\Classify^\texttt{foo}$ and want to know its \xmlattr{yields},
    we can write~$\Classify^\texttt{foo}_\gamma$ to bind the
    \xmlattr{yields} to~$\gamma$.\footnote{%
      This is conceptually like a symbol table lookup in the compiler.}



\subsection{Matches}
A classification consists of a set of binary predicates called
  \emph{matches}.
Matches may reference any values,
  including the results of other classifications
    (as in \thmpref{class-compose}),
  allowing for the construction of complex abstractions over the data being
  classified.

Matches are intended to act intuitively across inputs of different ranks---%
  that is,
    one can match on any combination of matrix, vector, and scalar values.

\begin{axiom}[Match Input Translation]\axmlabel{match-input}
  Let $j$ and $k$ be free variables intended to be bound in the
    context of \axmref{class-pred}.
  Let $J$ and $K$ be defined by \axmref{class-intro}.
  Given some input~$x$,

  \begin{equation*}
    \varsub x =
      \begin{cases}
        x_{j_k} &\rank{x} = 2; \\
        x_j     &\rank{x} = 1; \\
        x       &\rank{x} = 0,
      \end{cases}
    \qquad\qquad
    \begin{aligned}
      j&\in J, \\
      k&\in K_j.
    \end{aligned}
  \end{equation*}
\end{axiom}

\begin{axiom}[Match Rank]\axmlabel{match-rank}
  Let~$\sim{} : \Real\times\Real\rightarrow\Real$ be some binary relation.
  Then,

  \begin{equation*}
    \rank{\varsub x \sim \varsub y} =
      \begin{cases}
        \rank{x} &\rank{x} \geq \rank{y}, \\
        \rank{y} &\text{otherwise}.
      \end{cases}
  \end{equation*}
\end{axiom}

\def\xyequivish{\varsub x\equivish \varsub y}

\begin{axiom}[Element-Wise Equivalence ($\equivish$)]
\indexsym\equivish{equivalence, element-wise}
\index{equivalence!element-wise (\ensuremath\equivish)}
  \begin{align*}
    \rank{\varsub x}=\rank{\varsub y}=2,\,
      (\xyequivish) &\infer \Forall{j,k}{x_{j_k} \equiv y_{j_k}}, \\
    \rank{\varsub x}=\rank{\varsub y}=1,\,
      (\xyequivish) &\infer \Forall{j}{x_j \equiv y_j}, \\
    \rank{\varsub x}=\rank{\varsub y}=0,\,
      (\xyequivish) &\infer (x\equiv y).
  \end{align*}
\end{axiom}


\index{package!core/match@\tamepkg{core/match}}
Matches are represented by \xmlnode{match} nodes in \tame{}.
Since the primitive is rather verbose,
  \tamepkg{core/match} also defines templates providing a more concise
    notation
      (\xmlnode{t:match-$\zeta$} below).

\index{classification!match@\xmlnode{match}}
\begin{axiom}[Match Introduction]\axmlabel{match-intro}
  \begin{alignat*}{2}
    \begin{aligned}[b]
      \xml{<t:match-$\zeta$ }&\xml{on="$x$"} \xmlnll
                             &\xml{value="$y$" />}
    \end{aligned}
    {}&\equivish{}
    \begin{aligned}
      &\xml{<match on="$x$">} \xmlnll
      &\quad \xml{<c:$\zeta$>} \xmlnll
      &\quad\quad \xml{<c:value-of name="$y$">} \xmlnll
      &\quad \xml{</c:$\zeta$>} \xmlnll
      &\xml{</match>}
    \end{aligned}
    \qquad
    \sim{} = \smash{\begin{cases}
             =    &\zeta=\xml{eq},  \\
             <    &\zeta=\xml{lt},  \\
             >    &\zeta=\xml{gt},  \\
             \leq &\zeta=\xml{leq}, \\
             \geq &\zeta=\xml{geq}.
           \end{cases}} \\
  &\equivish \varsub x \sim \varsub y,
  \end{alignat*}
\end{axiom}

\begin{axiom}[Match Equality Short Form]
  \begin{equation*}
    \xml{<match on="$x$" />}
      \equivish \xml{<match on="$x$" value="TRUE" />}.
  \end{equation*}
\end{axiom}

\todo{Define types and \xml{typedef}.}
\begin{axiom}[Match Membership]
  When $T$ is a type defined with \xmlnode{typedef},
  \begin{equation*}
    \xml{<match on="$x$" anyOf="$T$" />} \equivish \varsub x \in T.
  \end{equation*}
\end{axiom}

\begin{theorem}[Classification Match Element-Wise Binary Relation]
\thmlabel{class-match}
  Within the context of \axmref{class-pred},
    all \xmlnode{match} forms represent binary relations
      $\Real\times\Real\rightarrow\Bool$
    ranging over individual elements of all index sets $J$ and $K_j\in K$.
\end{theorem}
\begin{proof}
  First,
    observe that each of $=$, $<$, $>$, $\leq$, $\geq$, and $\in$
    have type $\Real\times\Real\rightarrow\Bool$.
  We must then prove that $\varsub x$ and $\varsub y$ are able to be
    interpreted as~$\Real$ within the context of \axmref{class-pred}.

  When $x,y\in\Real$,
    we have the trivial case $\varsub x=x\in\Real$ and $\varsub y=y\in\Real$
    by \axmref{match-input}.
  Otherwise,
    variables $j$ and $k$ are free.

  Consider $\rank{\varsub x \sim \varsub y} = 2$;
    then $\rank{\varsub x \sim \varsub y} \in\Matrices$ by \dfnref{rank},
      and so by \thmref{class-rank-indep} we have
  \begin{equation}\label{p:match-rel}
    \Forall{j\in J}{\Forall{k\in K_j}{\cpredmatseq}}
      \equiv
      \Forall{j\in J}{\Forall{k\in K_j}{\varsub x \sim \varsub y}},
  \end{equation}
  which binds $j$ and $k$ to the variables of their respective quantifiers.
  Proceed similarly for $\rank{\varsub x \sim \varsub y} = 1$ and observe that
    $j$ becomes bound.

  Assume $x\in\Matrices$;
    then $x_{j_k}\in\Real$ by \dfnref{matrix}.
  Assume $y\in\Vectors^\Real$;
    then $y_j\in\Real$ by \dfnref{vec}.
  Finally,
    observe that $j$ ranges over $J$ in \ref{p:match-rel},
      and $k$ over $K_j$.
\end{proof}

\thmref{class-match} is responsible for proving that matches range over each
  individual index.
More subtly,
  it also shows that matches work with any combination of rank.
\spref{f:ex:class-match-all-ranks} demonstrates a complete translation of
  source \tame{}~XML using all ranks.

\begin{figure}[ht]
\begin{align}
  &\begin{aligned}
    &\xml{<classify as="fullrank" desc="Example of all ranks">} \xmlnl
    &\quad\begin{aligned}
      &\xml{<match on="$A$" value="$u$" />}
        \quad&&\equivish \varsub A = \varsub u \\[-2mm]
      &\xml{<match on="$A$" value="$t$" />}
        \quad&&\equivish \varsub A = \varsub t \xmlnll
      &\xml{<match on="$u$" value="$t$" />}
        \quad&&\equivish \varsub u = \varsub t \xmlnll
      &\xml{<match on="$t$" />}
        \quad&&\equivish \varsub t = \true
    \end{aligned} \xmlnll
    &\xml{</classify>}
  \end{aligned}
    &\text{by \axmref{match-intro}} \\
  &= \Classifyland^\texttt{fullrank}\left(
       \Big(\left({A_j}_k = u_j\right),
             \left({A_j}_k = t \right)
       \Big),
       \left(u_j = t\right),
       t
     \right)
    &\text{by \axmref{class-intro}} \\
  &\equiv \Exists{j\in J}{
            \Exists*{k\in K_j}{\Big(
              \left({A_j}_k = u_j\right)
              \land \left({A_j}_k = t \right)
            \Big)}
            \land u_j = t
          }
          \land t.
    &\text{by \thmref{class-match}}.
\end{align}
\caption{Example demonstrating \thmref{class-match} using all ranks.}
\label{f:ex:class-match-all-ranks}
\end{figure}

Visually,
  the one-dimensional construction of \axmref{class-pred} does not lend
  itself well to how intuitive the behavior of the system actually is.
We therefore establish a relationship to the notation of linear algebra
  to emphasize the relationship between each of the inputs.

\newcommand\matseqsup[1]{%
  \begin{bmatrix}
    M^{#1}_{0_0} & \dots  & M^{#1}_{0_k} \\
    \vdots       & \ddots & \vdots \\
    M^{#1}_{j_0} & \dots  & M^{#1}_{j_k} \\
  \end{bmatrix}%
}
\newcommand\vecseqsup[1]{%
  \begin{bmatrix}
    v^{#1}_0 \\
    \vdots       \\
    v^{#1}_j \\
  \end{bmatrix}%
}

% This must be an axiom because it defines how the connectives operate; see
% the remark.
\index{classification!matrix notation}
\begin{axiom}[Classification Matrix Notation]\axmlabel{class-mat-not}
  Let $\Gamma^2$ be defined by \axmref{class-yield}.
  Then,
  \begin{equation*}
    \Gamma^2 =
    \matseqsup{0}\monoidops\matseqsup{l}
    \monoidop
    \vecseqsup{0}\monoidops\vecseqsup{m}
    \monoidop
    s^0\monoidops s^n,
  \end{equation*}
  from which $\Gamma^1$, $\Gamma^0$, and $\gamma$ can be derived.
\end{axiom}

\begin{remark}[Logical Connectives With Matrix Notation]
  From the definition of \axmref{class-mat-not},
    it should be clear that the logical connective $\monoidop$ necessarily
    acts like a Hadamard product\cite{wp:hadamard-product} with respect to
    how individual elements are combined.
\end{remark}

\index{classification!intuition}
\axmref{class-mat-not} makes it easy to visualize classification
  operations simply by drawing horizontal boxes across the predicates,
    as demonstrated by \spref{f:class-mat-boxes}.
This visualization helps to show intuitively how the classification system
  is intended to function,
    with matrices serving as higher-resolution vectors.\footnote{%
      For example,
        with insurance,
        one may have a vector of data by risk location,
          and a matrix of chosen class codes by location.
      Consequently,
        we expect $M_j$ to be the set of class codes associated with
        location~$j$ so that it can be easily matched against location-level
        data~$v_j$.}

% NB: Give this formatting extra attention if the document's formatting is
% substantially changed, since it's not exactly responsible with it's
% hard-coded units.
\begingroup
\begin{figure}[ht]
  \def\classmatraise#1{%
    \begin{aligned}
    #1 \\ {} \\ #1
    \end{aligned}
  }
  \def\classmateq{%
    \matseqsup{0}
      \classmatraise{\monoidop\cdots\monoidop}
    \matseqsup{l}
      \classmatraise\monoidop
    \vecseqsup{0}
      \classmatraise{\monoidop\cdots\monoidop}
    \vecseqsup{m}
      \classmatraise{%
        {}\monoidop s^0\monoidop\cdots\monoidop s^n%
      }
  }
  \def\classmatlines#1{%
    \begin{alignedat}{2}
      \Big( &M^0_{{#1}_0} \monoidops {}&&M^l_{{#1}_0} \Big)
        \monoidop
        v^0_{#1} \monoidops v^m_{#1}
        \monoidop
        s^0 \monoidops s^n \\
      &\quad\!\vdots &&\quad\!\vdots \\
      \Big( &M^0_{{#1}_k} \monoidops {}&&M^l_{{#1}_k} \Big)
        \monoidop
        v^0_{#1} \monoidops v^m_{#1}
        \monoidop
        s^0 \monoidops s^n
    \end{alignedat}
  }

  \begin{align*}
    &\quad\raisebox{-11mm}[0mm]{%
       \begin{turn}{45}
         $\equiv$
       \end{turn}%
     }\; \classmatlines{0} &\Gamma^2_0 \\[-2mm]
    &\fbox{\raisebox{0mm}[0mm][6mm]{\hphantom{$\classmateq$}}} \\[-8mm]
    %
    &\classmateq &\vdots\; \\[-10mm]
    %
    &\fbox{\raisebox{0mm}[0mm][6mm]{\hphantom{$\classmateq$}}} \\
    &\quad\raisebox{11mm}[0mm]{%
       \begin{turn}{-45}
         $\equiv$
       \end{turn}%
     }\; \classmatlines{j} &\Gamma^2_j
  \end{align*}
\caption{Visual interpretation of classification by \axmref{class-mat-not}.
         For each boxed row of the matrix notation there is an equivalence
           to the first-order logic of \thmref{class-compose}.}
\label{f:class-mat-boxes}
\end{figure}
\endgroup

\index{classification!as proposition|(}
\begin{lemma}[Match As Proposition]\lemlabel{match-prop}
  Matches can be represented using propositional logic provided that
    binary operators of \axmref{match-intro} are restricted to $\cbif\Bool$.
\end{lemma}
\begin{proof}
  \begin{alignat*}{4}
    x = \true  &\equiv x,               &&\quad=    &&: \cbif\Bool; \\
    x = \false &\equiv \neg x,          &&\quad=    &&: \cbif\Bool; \\
    x < y      &\equiv \neg x \land y,  &&\quad<    &&: \cbif\Bool; \\
    x > y      &\equiv x \land \neg y,  &&\quad>    &&: \cbif\Bool; \\
    x \leq y   &\equiv \neg x \lor y,   &&\quad\leq &&: \cbif\Bool; \\
    x \geq y   &\equiv x \lor \neg y,   &&\quad\geq &&: \cbif\Bool; \\
    x \in\Bool &\equiv \true,           &&\quad\in  &&: \cbif\Bool.\tag*{\qedhere}
  \end{alignat*}
\end{proof}

\begin{theorem}[Classification As Proposition]
\index{classification!as proposition|(}
  Classifications with either $M\union v=\emptyset$ or with constant index
    sets can be represented by propositional logic provided that the domains
    of the binary operators of \axmref{match-intro} are restricted to
    $\cbif\Bool$.
\end{theorem}
\begin{proof}
  Propositional logic does not include quantifiers or relations.
  Matches of the domain $\cbif\Bool$ are proved to be propositions by
    \lemref{match-prop}.
  Having eliminated relations,
    we must now eliminate quantifiers.

  Assume $M\union v=\emptyset$.
  By \thmref{class-rank-indep},

  \begin{align*}
    c &\equiv \cpredscalarseq,
  \end{align*}

  \noindent
  which is a propositional formula.

  Similarly,
    if we define our index set~$J$ to be constant,
      we are then able to eliminate existential quantification over~$J$
      as follows:
  \begin{equation}\label{eq:prop-vec}
  \begin{aligned}
    c &\equiv \Exists{j\in J}{\cpredvecseq}, \\
      &\equiv \left(v^0_0\monoidops v^m_0\right)
              \lor\cdots\lor
              \left(v^0_{|J|-1}\monoidops v^m_{|J|-1}\right),
  \end{aligned}
  \end{equation}
  which is a propositional formula.
  Similarly,
    for matrices,

  \begin{align*}
    c &\equiv \Exists{j\in J}{\Exists{k\in K_j}{\cpredmatseq}}, \nonumber\\
      &\equiv \Exists{j\in J}{
                \left({M^0_j}_0\monoidops{M^0_j}_{|K_j|-1}\right)
                \lor\cdots\lor
                \left({M^l_j}_0\monoidops{M^l_j}_{|K_j|-1}\right)
              },
  \end{align*}
  and then proceed as in~\ref{eq:prop-vec}.
\end{proof}
\index{classification!as proposition|)}