639 lines
22 KiB
TeX
639 lines
22 KiB
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~$\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} \\
|
|
\displaybreak[0]
|
|
\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}[ht]
|
|
\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}.}
|
|
\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\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} &\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{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}} \\
|
|
&= \Classify^\texttt{fullrank}\left(
|
|
\odot^\land,
|
|
\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}
|
|
|
|
\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|)} |