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}
\INCOMPLETE{This section is a work-in-progress.}

\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~$\bullet$
            (see \secref{monoids})
          and~$\odot$ looks vaguely like~$(\bullet)$,
            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}
  \odot^\land &= \Monoid\Bool\land\true, \\
  \odot^\lor &= \Monoid\Bool\lor\false.
\end{aligned}
\end{equation}


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


\begin{axiom}[Classification-Predicate Equivalence]\axmlabel{class-pred}
\index{classification!as predicate}
  Let $\Classify^c_\gamma\left(\Monoid\Bool\bullet 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\bullet\cpredvecseq}
        \bullet\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\bullet 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} \\
    \exists{j\in J}\Big(\exists{k\in K_j}\Big(
      \Gamma^2_{j_k} &= \cpredmatseq\bullet\cpredvecseq\bullet\cpredscalarseq
    \Big)\Big), \\
    %
    \exists{j\in J}\Big(
      \Gamma^1_j &= \cpredvecseq\bullet\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}}
               \bullet \Gamma^1_j
             }
             \bullet \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}}
              \bullet \Gamma^1_j
            \Big)
            \bullet \Gamma^0
        &&\text{by \axmref{class-yield}} \\
      %
      &\eejJ\exists{k\in K_j}\Big(
              \cpredmatseq \bullet \cpredvecseq \bullet \cpredscalarseq
            \Big) \\
      &\hphantom{\eejJ}\;\cpredvecseq \bullet \cpredscalarseq \Big)
                \bullet \cpredscalarseq, \\
      %
      &\eejJ\exists{k\in K_j}\Big(\cpredmatseq\Big)
            \bullet \cpredvecseq \bullet \cpredscalarseq \\
      &\hphantom{\eejJ}\;\cpredvecseq \bullet \cpredscalarseq \Big)
                \bullet \cpredscalarseq,
        &&\text{by \dfnref{quant-conn}} \\
      %
      &\eejJ\exists{k\in K_j}\Big(\cpredmatseq\Big)
        &&\text{by \dfnref{prop-taut}} \\
      &\hphantom{\eejJ}\;\cpredvecseq \bullet \cpredscalarseq \Big)
                \bullet \cpredscalarseq, \\
      %
      &\eejJ\exists{k\in K_j}\Big(\cpredmatseq\Big)
        &&\text{by \dfnref{quant-conn}} \\
      &\hphantom{\eejJ}\;\cpredvecseq\Big) \bullet \cpredscalarseq
                \bullet \cpredscalarseq, \\
      %
      &\eejJ\exists{k\in K_j}\Big(\cpredmatseq\Big)
        &&\text{by \dfnref{prop-taut}} \\
      &\hphantom{\eejJ}\;\cpredvecseq\Big)
                \bullet \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\bullet 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}\bullet e} \bullet e
        \qquad&&\text{by \dfnref{monoid-seq}} \label{p:cri-c} \\
      &\equiv \Exists{j\in J}{e \bullet e} \bullet e
        &&\text{by \dfnref{quant-elim}} \\
      &\equiv \Exists{j\in J}{e} \bullet e
        &&\text{by \ref{eq:monoid-identity}} \\
      &\equiv e \bullet 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}[h]\label{fig:always-never}
  \begin{alignat*}{3}
    \begin{aligned}
      \xml{<classify }&\xml{as="always" yields="alwaysTrue"} \xmlnl
                      &\xml{desc="Always true" />}
    \end{aligned}
      \quad&=\quad
      \Classify^\texttt{always}_\texttt{alwaysTrue}
        &&\left(\odot^\land,\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
      \Classify^\texttt{never}_\texttt{neverTrue}
        &&\left(\odot^\lor,\emptyset,\emptyset,\emptyset\right).
  \end{alignat*}
  \caption{\tameclass{always} and \tameclass{never} from package
             \tamepkg{core/base}.}
\end{figure}

Figure~\ref{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\bullet 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}
        \bullet \cpredvecseq
      }
      \bullet \cpredscalarseq \\
    \equiv c \equiv
    \Exists{j\in J}{
        \Exists{k\in K_j}{\gamma'''_{j_k}}
        \bullet \gamma''_j
      }
      \bullet \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}
\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} &\|x\| = 2; \\
        x_j     &\|x\| = 1; \\
        x       &\|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*}
    \|\varsub x \sim \varsub y\| =
      \begin{cases}
        \|x\| &\|x\| \geq \|y\|, \\
        \|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*}
    \|\varsub x\|=\|\varsub y\|=2,\,
      (\xyequivish) &\infer \Forall{j,k}{x_{j_k} \equiv y_{j_k}}, \\
    \|\varsub x\|=\|\varsub y\|=1,\,
      (\xyequivish) &\infer \Forall{j}{x_j \equiv y_j}, \\
    \|\varsub x\|=\|\varsub y\|=0,\,
      (\xyequivish) &\infer (x\equiv y).
  \end{align*}
\end{axiom}

\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 $\|\varsub x \sim \varsub y\| = 2$;
    then $\|\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}

  \noindent
  which binds $j$ and $k$ to the variables of their respective quantifiers.
  Proceed similarly for $\|\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}

\todo{Example.}
\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.
This is perhaps best illustrated with an example.

\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\bullet\cdots\bullet v^m_0\right)
              \lor\cdots\lor
              \left(v^0_{|J|-1}\bullet\cdots\bullet 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\bullet\cdots\bullet{M^0_j}_{|K_j|-1}\right)
                \lor\cdots\lor
                \left({M^l_j}_0\bullet\cdots\bullet{M^l_j}_{|K_j|-1}\right)
              },
  \end{align*}
  and then proceed as in~\ref{eq:prop-vec}.
\end{proof}
\index{classification!as proposition|)}