employer
/
tame
1
0
Fork 0
Code Packages Releases Activity

design/tpl: \{log=>l}{and,or} 

Don't I feel silly.
master
Mike Gerwitz 2021-05-13 15:50:13 -04:00
parent 63b502b7df
commit 060a7d0e6c
3 changed files with 22 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -19,13 +19,13 @@ This limitation is mitigated through use of the template system.
\todo{$\Classify$ itself has not yet been defined.}
\index{classification!conjunctive}
\begin{definition}[\logand-Classification]\dfnlabel{classu}
\begin{definition}[$\land$-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$,
$\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,
@ -40,12 +40,12 @@ This limitation is mitigated through use of the template system.
&\quad \vdots \\
&\quad M_n \\
&\xml{</classify>}
\equiv \Classify^c_\gamma M_0 \logand \ldots \logand M_n.
\equiv \Classify^c_\gamma M_0 \land \ldots \land M_n.
\end{align*}
\end{definition}
\index{classification!disjunctive}
\begin{definition}[\logor-Classification]\dfnlabel{classe}
\begin{definition}[$\lor$-Classification]\dfnlabel{classe}
A disjunctive classification~$d$ with \xpath{@any="true"}
performs disjunction on its match expressions
$M_0\ldots M_n$.\footnote{%
@ -63,7 +63,7 @@ This limitation is mitigated through use of the template system.
&\quad \vdots \\
&\quad M_n \\
&\texttt{</classify>}
\equiv \Classify^d_\gamma M_0 \logor \ldots \logor M_n.
\equiv \Classify^d_\gamma M_0 \lor \ldots \lor M_n.
\end{align*}
\end{definition}
@ -112,7 +112,7 @@ is equivalent to the proposition
\begin{equation*}
\tameclass{pool-hazard} \equiv \tameparam{diving\_board}
\logand \tameparam{pool\_depth\_ft} < 8.
\land \tameparam{pool\_depth\_ft} < 8.
\end{equation*}

32
design/tpl/sec/notation.tex
View File

@ -23,7 +23,7 @@ When you see any of these prefixed with ``0.'',
\index{logic!propositional}
We reproduce here certain axioms and corollaries of propositional logic for
convenience and to clarify our interpretation of certain concepts.
The use of the symbols $\logand$, $\logor$, and~$\neg$ are standard.
The use of the symbols $\land$, $\lor$, and~$\neg$ are standard.
\indexsym\infer{infer}
\index{infer (\ensuremath\infer)}
The symbol $\infer$ means ``infer''.
@ -33,40 +33,40 @@ We use $\implies$ in place of $\rightarrow$ for implication,
We further use $\equiv$ in place of $\leftrightarrow$ to represent material
equivalence.
\indexsym\logand{conjunction}
\index{conjunction (\ensuremath{\logand})}
\indexsym\land{conjunction}
\index{conjunction (\ensuremath{\land})}
\begin{definition}[Logical Conjunction]
$p,q \infer (p\logand q)$.
$p,q \infer (p\land q)$.
\end{definition}
\indexsym\logor{disjunction}
\index{disjunction (\ensuremath{\logor})}
\indexsym\lor{disjunction}
\index{disjunction (\ensuremath{\lor})}
\begin{definition}[Logical Disjunction]
$p \infer (p\logor q)$ and $q \infer (p\logor q)$.
$p \infer (p\lor q)$ and $q \infer (p\lor q)$.
\end{definition}
\indexsym\neg{negation}
\index{negation (\ensuremath{\neg})}
\index{law of excluded middle}
\begin{definition}[Law of Excluded Middle]
$\infer (p \logor \neg p)$.
$\infer (p \lor \neg p)$.
\end{definition}
\index{law of non-contradiction}
\begin{definition}[Law of Non-Contradiction]
$\infer \neg(p \logand \neg p)$.
$\infer \neg(p \land \neg p)$.
\end{definition}
\index{De Morgan's theorem}
\begin{definition}[De Morgan's Theorem]
$\neg(p \logand q) \infer (\neg p \logor \neg q)$
and $\neg(p \logor q) \infer (\neg p \logand \neg q)$.
$\neg(p \land q) \infer (\neg p \lor \neg q)$
and $\neg(p \lor q) \infer (\neg p \land \neg q)$.
\end{definition}
\indexsym\equiv{equivalence}
\index{equivalence!material (\ensuremath{\equiv})}
\begin{definition}[Material Equivalence]
$p\equiv q \infer \big((p \logand q) \logor (\neg p \logand \neg q)\big)$.
$p\equiv q \infer \big((p \land q) \lor (\neg p \land \neg q)\big)$.
\end{definition}
$\equiv$ denotes a logical identity.
@ -76,7 +76,7 @@ Consequently,
\indexsym{\!\!\implies\!\!}{implication}
\index{implication (\ensuremath{\implies})}
\begin{definition}[Implication]
$p\implies q \infer (\neg p \logor q)$.
$p\implies q \infer (\neg p \lor q)$.
\end{definition}
\indexsym{\true}{boolean, true}
@ -191,7 +191,7 @@ We therefore have
f : A \rightarrow B &\infer f \subset A\times B, \\
f = \alpha \mapsto \alpha' : A \rightarrow B
&= \Set{(\alpha,\alpha')
\mid \alpha\in A \logand \alpha'\in B}, \\
\mid \alpha\in A \land \alpha'\in B}, \\
f[D\subseteq A] &= \Set{f(\alpha) \mid \alpha\in D} \subset B, \\
f[] &= f[A].
\end{align}
@ -273,9 +273,9 @@ This notation is used to simplify definitions of the classification system
\alpha \bicompi{R} \beta =
\begin{cases}
\gamma \mapsto \alpha_\gamma \bicompi{R} \beta_\gamma
&\text{if } (\alpha : A\rightarrow B) \logand (\beta : A\rightarrow D),\\
&\text{if } (\alpha : A\rightarrow B) \land (\beta : A\rightarrow D),\\
\gamma \mapsto \alpha_\gamma \bicompi{R} (\_ \mapsto \beta)
&\text{if } (\alpha : A\rightarrow B) \logand (\beta \in\Real),\\
&\text{if } (\alpha : A\rightarrow B) \land (\beta \in\Real),\\
\alpha R \beta &\text{otherwise}.
\end{cases}
\end{equation}

3
design/tpl/tpl.sty
View File

@ -65,9 +65,6 @@
\newcommand\false{\ensuremath{\bot}}
\newcommand\Bool{\ensuremath{\{\false,\true\}}}
\newcommand\logand{\ensuremath{\wedge}}
\newcommand\logor{\ensuremath{\vee}}
\newcommand\tametrue{\tameconst{TRUE}}
\newcommand\tamefalse{\tameconst{FALSE}}