tame/design/tpl/sec/class.tex

784 lines
26 KiB
TeX
Raw Blame History

This file contains invisible Unicode characters!

This file contains invisible Unicode characters that may be processed differently from what appears below. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to reveal hidden characters.

% 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|)}