% The TAME Programming Language Classification System
%
% Copyright (C) 2021 Ryan Specialty, 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{}\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{}
% 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{}
\end{aligned}
\quad&=\quad
\Classifyland^\texttt{always}_\texttt{alwaysTrue}
&&\left(\emptyset,\emptyset,\emptyset\right). \\
%
\begin{aligned}
\xml{}
\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{}
\end{aligned}
{}&\equivish{}
\begin{aligned}
&\xml{} \xmlnll
&\quad \xml{} \xmlnll
&\quad\quad \xml{} \xmlnll
&\quad \xml{} \xmlnll
&\xml{}
\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{}
\equivish \xml{}.
\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{} \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{} \xmlnl
&\quad\begin{aligned}
&\xml{}
\quad&&\equivish \varsub A = \varsub u \\[-2mm]
&\xml{}
\quad&&\equivish \varsub A = \varsub t \xmlnll
&\xml{}
\quad&&\equivish \varsub u = \varsub t \xmlnll
&\xml{}
\quad&&\equivish \varsub t = \true
\end{aligned} \xmlnll
&\xml{}
\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|)}