employer
/
tame
1
0
Fork 0
Code Packages Releases Activity

design/tpl: Introduce \Classify mathop 

This will be used as an IR of sorts to eliminate the XML, which will be far
too verbose to use in proofs.  It also allows us to attach behavior to the
operator, which will end up defining two values for @as and @yields.
master
Mike Gerwitz 2021-05-11 16:37:08 -04:00
parent d78186461f
commit 9d9535a1b8
4 changed files with 159 additions and 54 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

92
design/tpl/sec/appendix-typesetting.tex 100644
View File

@ -0,0 +1,92 @@
\section{Meta: Typesetting}
This appendix is a meta-document describing typographic considerations for
this document.
It is intended to be included in debug/developer builds,
not to be included as official documentation for the software.
\subsection{$\Classify$}
\index{classification!\ensuremath{\Classify} design}
The symbol representing classification is defined in \secref{class}.
It uses the capital Fraktur letter~`C',
typeset as~$\Classify\!\!$.
Compare this side-by-side with the summation operator Sigma:
\def\EXSUM{\sum_k^n k}
\def\EXCLASS{\Classify^\texttt{as}_\texttt{yields} P}
\begin{equation*}
\EXSUM \mspace{50mu} \EXCLASS.
\end{equation*}
These are both written inline, respectively, as
$\EXSUM$ and $\EXCLASS$.
Classifications are canonically referred to by their \xmlattr{as}~name,
which makes for a bit of an awkward-looking construction when the
superscript is provided but not the subscript.
For example, consider the classification $\tameclass{foo-bar}$ inline,
compared to~$\Classify_\texttt{foo-bar}$.
Now compare the display style
\begin{equation*}
\tameclass{foo-bar}
\mspace{25mu}\text{vs.}\mspace{25mu}
\Classify_\texttt{foo-bar}.
\end{equation*}
Of course,
referring to the \xmlattr{yields}~name will use the subscript,
which (at least to the author) feels more natural.
Why not swap them, then?
The superscript always denotes a scalar Boolean value.
The subscript,
however,
has a more complex type that's dependent on the predicates of the classification.
Let's say we wanted to denote a classification with a dimensionality of~$2$:
$\Classify^\texttt{foo-bar}_{\texttt{fooBar}^2}$ versus
$\Classify_\texttt{foo-bar}^{\texttt{fooBar}^2}$,
typeset in display style as
\begin{equation*}
\Classify^\texttt{foo-bar}_{\texttt{fooBar}^2}
\mspace{25mu}\text{vs.}\mspace{25mu}
\Classify_\texttt{foo-bar}^{\texttt{fooBar}^2}.
\end{equation*}
The amount of vertical space taken up by the first style is unchanged by the
superscript on the subscript,
but that's not true of the second style.
The final consideration is that the subscript of the summation,
when the superscript is omitted,
denotes the range or set of values for the sum.
For example,
one may have $\sum_{0\leq k \leq n}$ or
$\sum_{a\in A}$.
Having the subscript of $\Classify$ represent the more complex set of values
is therefore more analogous to the sum,
and better fits readers' intuitive notational expectations.
It is also worth noting that the distinction between the two is historical---%
\xmlattr{as} used to represent an accumulator,
which is a long-removed feature;
references to~\xmlattr{as} in \tame{} today end up resolving
to~\xmlattr{yields} anyway.
If that name is repurposed,
one potential option is to have it take the place of~\xmlattr{yields},
in which case the superscript in~$\Classify$ goes away and the
notational awkwardness is removed.
A final note on the choice of character:
Admittedly, $\Classify$ does look a bit threatening,
but one could also interpret it as ``bold and distinguished''.
$\mathcal{C}$ was considered,
but it looks too childish (and perhaps Comic Sans-like) when typeset large:
\begin{equation*}
\displaystyle\mathop{\hbox{\huge$\mathcal{C}$}}^\texttt{rejected}_\texttt{style}.
\end{equation*}
It's easy enough to change in the future if we change our minds.

104
design/tpl/sec/class.tex
View File

@ -17,8 +17,58 @@ Intuitively,
\emph{tightly coupled} to the classification itself.
This limitation is mitigated through use of the template system.
\index{classification!conjunctive}
\begin{definition}[\logand-Classification]\dfnlabel{classu}
A conjunctive\footnote{%
Conjunctive and disjunctive classifications used to be referred to,
respectively,
as \emph{universal} and \emph{existential},
referring to fact that
$\forall\Set{a_0,\ldots,a_n}(a) \equiv a_0\logand\ldots\logand 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.
}
classification~$c$ performs conjunction on its match expressions
$M_0\ldots M_n$.
\begin{align*}
&\xml{<classify as="$c$" yields="$\gamma$" desc="$\ldots$">} \\
&\quad M_0 \\
&\quad \vdots \\
&\quad M_n \\
&\xml{</classify>}
\equiv \Classify^c_\gamma M_0 \logand \ldots \logand M_n.
\end{align*}
\end{definition}
\index{classification!disjunctive}
\begin{definition}[\logor-Classification]\dfnlabel{classe}
A disjunctive classification~$d$ with \xpath{@any="true"}
performs disjunction on its match expressions
$M_0\ldots M_n$.\footnote{%
It is notationally convenient that~$c$ is a common prefix for both
\underline{c}lassification \emph{and} \underline{c}onjunction,
and also that~$d$ happens to follow~$c$ \emph{and} be the prefix for
\underline{d}isjunction.
This notation will only be used where such a distinction is relevant,
and $c$~will otherwise refer generically to any type of
classification.}
\begin{align*}
&\xml{<classify as="$d$" yields="$\gamma$" any="true" desc="$\ldots$">} \\
&\quad M_0 \\
&\quad \vdots \\
&\quad M_n \\
&\texttt{</classify>}
\equiv \Classify^d_\gamma M_0 \logor \ldots \logor M_n.
\end{align*}
\end{definition}
\todo{$\Classify$ itself has not yet been defined.}
For example,
consider the following classification \tameclass{cost-exceeded}.
consider the following classification $\Classify^\texttt{cost-exceeded}$.
Let~\tameparam{cost} be a scalar parameter.
\index{classification!classify@\xmlnode{classify}}
@ -64,58 +114,6 @@ is equivalent to the proposition
\logand \tameparam{pool\_depth\_ft} < 8.
\end{equation*}
\goodbreak
\index{classification!conjunctive}
\begin{definition}[\logand-Classification]\dfnlabel{classu}
A conjunctive\footnote{%
Conjunctive and disjunctive classifications used to be referred to,
respectively,
as \emph{universal} and \emph{existential},
referring to fact that
$\forall\Set{a_0,\ldots,a_n}(a) \equiv a_0\logand\ldots\logand 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.
}
classification~$c$ performs conjunction on its match expressions
$M_0\ldots M_n$.
\begin{alignat*}{2}
&\xml{<classify as="}&&c\xml{" desc="$\ldots$">} \\
&\quad M_0 \\
&\quad \vdots \\
&\quad M_n \\
&\xml{</classify>}
&&\equiv c\in\Bool \\
& &&\equiv M_0 \logand \ldots \logand M_n.
\end{alignat*}
\end{definition}
\index{classification!disjunctive}
\begin{definition}[\logor-Classification]\dfnlabel{classe}
A disjunctive classification~$d$ with \xpath{@any="true"}
performs disjunction on its match expressions
$M_0\ldots M_n$.\footnote{%
It is notationally convenient that~$c$ is a common prefix for both
\underline{c}lassification \emph{and} \underline{c}onjunction,
and also that~$d$ happens to follow~$c$ \emph{and} be the prefix for
\underline{d}isjunction.
This notation will only be used where such a distinction is relevant,
and $c$~will otherwise refer generically to any type of
classification.}
\begin{alignat*}{2}
&\xml{<classify as="} &&d\xml{" any="true" desc="$\ldots$">} \\
&\quad M_0 \\
&\quad \vdots \\
&\quad M_n \\
&\texttt{</classify>}
&&\equiv d\in\Bool \\
& &&\equiv M_0 \logor \ldots \logor M_n.
\end{alignat*}
\end{definition}
\subsection{Matches}
\begin{definition}[Match Equality]

9
design/tpl/tpl.sty
View File

@ -52,7 +52,7 @@
\newcommand\xpath[1]{\texttt{#1}}
\newcommand\xmlnode[1]{\texttt{#1}}
\newcommand\xmlattr[1]{@\texttt{#1}}
\newcommand\xmlattr[1]{{@\texttt{#1}}}
\newcommand\tameparam[1]{\texttt{#1}}
\newcommand\tameclass[1]{\texttt{#1}}
@ -129,4 +129,11 @@
% Symbols appear at the beginning of the index
\newcommand\indexsym[2]{\index{__sym_#2@{\ensuremath{#1}}|see {#2}}}
\DeclareMathOperator*\Classify{%
\mathchoice{\vcenter{\hbox{\huge$\mathfrak{C}$}}}
{\vcenter{\hbox{\Large$\mathfrak{C}$}}}
{\frak{C}}
{\frak{C}}
}
\newcommand\todo[1]{\marginnote{\underline{\textsc{Todo:}}\\ \textsl{#1}}}

8
design/tpl/tpl.tex
View File

@ -56,6 +56,14 @@
\input{sec/notation.tex}
\input{sec/class.tex}
% Flag is on for now
\let\WITHAPPENDIX1
\ifx\WITHAPPENDIX1
\appendix
\input{sec/appendix-typesetting.tex}
\fi
% Ensure Copyright line does not show for Index
\cfoot[\thepage]{\thepage}
\clearpage