2021-05-19 09:55:54 -04:00
|
|
|
% The TAME Programming Language Notational Conventions
|
|
|
|
%
|
2023-01-17 23:09:25 -05:00
|
|
|
% Copyright (C) 2021 Ryan Specialty, LLC.
|
2021-05-19 09:55:54 -04:00
|
|
|
%
|
|
|
|
% Licensed under the Creative Commons Attribution-ShareAlike 4.0
|
|
|
|
% International License.
|
|
|
|
%%
|
2021-04-30 09:16:01 -04:00
|
|
|
|
|
|
|
\section{Notational Conventions}
|
|
|
|
This section provides a fairly terse overview of the foundational
|
|
|
|
mathematical concepts used in this paper.
|
|
|
|
While we try to reason about \tame{} in terms of algebra,
|
|
|
|
first-order logic;
|
|
|
|
and set theory;
|
|
|
|
notation varies even within those branches.
|
|
|
|
To avoid ambiguity,
|
|
|
|
especially while introducing our own notation,
|
|
|
|
core operators and concepts are explicitly defined below.
|
|
|
|
|
|
|
|
This section begins its numbering at~0.
|
|
|
|
This is not only a hint that \tame{} (and this paper) use 0-indexing,
|
|
|
|
but also because equations; definitions; theorems; corollaries; and the
|
|
|
|
like are all numbered relative to their section.
|
|
|
|
When you see any of these prefixed with ``0.'',
|
|
|
|
this sets those references aside as foundational mathematical concepts
|
|
|
|
that are not part of the theory and operation of \tame{} itself.
|
|
|
|
|
|
|
|
|
|
|
|
\subsection{Propositional Logic}
|
2021-05-11 11:33:12 -04:00
|
|
|
\index{logic!propositional}
|
2021-04-30 09:16:01 -04:00
|
|
|
We reproduce here certain axioms and corollaries of propositional logic for
|
|
|
|
convenience and to clarify our interpretation of certain concepts.
|
2021-05-13 15:50:13 -04:00
|
|
|
The use of the symbols $\land$, $\lor$, and~$\neg$ are standard.
|
2021-05-10 16:54:19 -04:00
|
|
|
\indexsym\infer{infer}
|
|
|
|
\index{infer (\ensuremath\infer)}
|
|
|
|
The symbol $\infer$ means ``infer''.
|
2021-04-30 09:16:01 -04:00
|
|
|
We use $\implies$ in place of $\rightarrow$ for implication,
|
|
|
|
since the latter is used to denote the mapping of a domain to a codomain
|
|
|
|
in reference to functions.
|
|
|
|
We further use $\equiv$ in place of $\leftrightarrow$ to represent material
|
|
|
|
equivalence.
|
|
|
|
|
2021-05-13 15:50:13 -04:00
|
|
|
\indexsym\land{conjunction}
|
|
|
|
\index{conjunction (\ensuremath{\land})}
|
2021-04-30 09:16:01 -04:00
|
|
|
\begin{definition}[Logical Conjunction]
|
2021-05-13 15:50:13 -04:00
|
|
|
$p,q \infer (p\land q)$.
|
2021-04-30 09:16:01 -04:00
|
|
|
\end{definition}
|
|
|
|
|
2021-05-13 15:50:13 -04:00
|
|
|
\indexsym\lor{disjunction}
|
|
|
|
\index{disjunction (\ensuremath{\lor})}
|
2021-04-30 09:16:01 -04:00
|
|
|
\begin{definition}[Logical Disjunction]
|
2021-05-13 15:50:13 -04:00
|
|
|
$p \infer (p\lor q)$ and $q \infer (p\lor q)$.
|
2021-04-30 09:16:01 -04:00
|
|
|
\end{definition}
|
|
|
|
|
2021-05-14 10:32:50 -04:00
|
|
|
\begin{definition}[$\land$-Associativity]\dfnlabel{conj-assoc}
|
|
|
|
$(p \land (q \land r)) \infer ((p \land q) \land r)$.
|
|
|
|
\end{definition}
|
|
|
|
|
|
|
|
\begin{definition}[$\lor$-Associativity]\dfnlabel{disj-assoc}
|
|
|
|
$(p \lor (q \lor r)) \infer ((p \lor q) \lor r)$.
|
|
|
|
\end{definition}
|
|
|
|
|
|
|
|
\begin{definition}[$\land$-Commutativity]\dfnlabel{conj-commut}
|
|
|
|
$(p \land q) \infer (q \land p)$.
|
|
|
|
\end{definition}
|
|
|
|
|
|
|
|
\begin{definition}[$\lor$-Commutativity]\dfnlabel{disj-commut}
|
|
|
|
$(p \lor q) \infer (q \lor p)$.
|
|
|
|
\end{definition}
|
|
|
|
|
|
|
|
\begin{definition}[$\land$-Simplification]\dfnlabel{conj-simpl}
|
|
|
|
$p \land q \infer p$.
|
|
|
|
\end{definition}
|
|
|
|
|
|
|
|
\begin{definition}[Double Negation]\dfnlabel{double-neg}
|
|
|
|
$\neg\neg p \infer p$.
|
|
|
|
\end{definition}
|
|
|
|
|
2021-05-11 11:33:12 -04:00
|
|
|
\indexsym\neg{negation}
|
|
|
|
\index{negation (\ensuremath{\neg})}
|
|
|
|
\index{law of excluded middle}
|
2021-04-30 09:16:01 -04:00
|
|
|
\begin{definition}[Law of Excluded Middle]
|
2021-05-13 15:50:13 -04:00
|
|
|
$\infer (p \lor \neg p)$.
|
2021-04-30 09:16:01 -04:00
|
|
|
\end{definition}
|
|
|
|
|
2021-05-11 11:33:12 -04:00
|
|
|
\index{law of non-contradiction}
|
2021-04-30 09:16:01 -04:00
|
|
|
\begin{definition}[Law of Non-Contradiction]
|
2021-05-13 15:50:13 -04:00
|
|
|
$\infer \neg(p \land \neg p)$.
|
2021-04-30 09:16:01 -04:00
|
|
|
\end{definition}
|
|
|
|
|
2021-05-11 11:33:12 -04:00
|
|
|
\index{De Morgan's theorem}
|
2021-05-14 10:32:50 -04:00
|
|
|
\begin{definition}[De Morgan's Theorem]\dfnlabel{demorgan}
|
2021-05-13 15:50:13 -04:00
|
|
|
$\neg(p \land q) \infer (\neg p \lor \neg q)$
|
|
|
|
and $\neg(p \lor q) \infer (\neg p \land \neg q)$.
|
2021-04-30 09:16:01 -04:00
|
|
|
\end{definition}
|
|
|
|
|
2021-05-10 16:50:30 -04:00
|
|
|
\indexsym\equiv{equivalence}
|
2021-04-30 09:16:01 -04:00
|
|
|
\index{equivalence!material (\ensuremath{\equiv})}
|
|
|
|
\begin{definition}[Material Equivalence]
|
2021-05-13 15:50:13 -04:00
|
|
|
$p\equiv q \infer \big((p \land q) \lor (\neg p \land \neg q)\big)$.
|
2021-04-30 09:16:01 -04:00
|
|
|
\end{definition}
|
|
|
|
|
|
|
|
$\equiv$ denotes a logical identity.
|
|
|
|
Consequently,
|
|
|
|
it'll often be used as a definition operator.
|
|
|
|
|
2021-05-11 11:33:12 -04:00
|
|
|
\indexsym{\!\!\implies\!\!}{implication}
|
|
|
|
\index{implication (\ensuremath{\implies})}
|
2021-05-21 16:10:44 -04:00
|
|
|
\begin{definition}[Implication]\dfnlabel{implication}
|
2021-05-13 15:50:13 -04:00
|
|
|
$p\implies q \infer (\neg p \lor q)$.
|
2021-04-30 09:16:01 -04:00
|
|
|
\end{definition}
|
|
|
|
|
2021-05-18 10:06:32 -04:00
|
|
|
\begin{definition}[Tautologies]\dfnlabel{prop-taut}
|
|
|
|
$p\equiv (p\land p)$ and $p\equiv (p\lor p)$.
|
|
|
|
\end{definition}
|
|
|
|
|
2021-05-11 11:33:12 -04:00
|
|
|
\indexsym{\true}{boolean, true}
|
|
|
|
\indexsym{\false}{boolean, false}
|
|
|
|
\index{boolean!FALSE@\tamefalse{} (\false)}%
|
|
|
|
\index{boolean!TRUE@\tametrue{} (\true)}%
|
2021-04-30 09:16:01 -04:00
|
|
|
\begin{definition}[Truth Values]\dfnlabel{truth-values}
|
2021-05-10 16:54:19 -04:00
|
|
|
$\infer\true$ and $\infer\neg\false$.
|
2021-04-30 09:16:01 -04:00
|
|
|
\end{definition}
|
|
|
|
|
2021-05-18 10:06:32 -04:00
|
|
|
\indexsym\Int{integer}
|
|
|
|
\index{integer (\Int)}%
|
|
|
|
\begin{definition}[Boolean/Integer Equivalency]\dfnlabel{bool-int}
|
|
|
|
$\Set{0,1}\in\Int, \false \equiv 0$ and $\true \equiv 1$.
|
|
|
|
\end{definition}
|
|
|
|
|
2021-04-30 09:16:01 -04:00
|
|
|
|
|
|
|
\subsection{First-Order Logic and Set Theory}
|
2021-05-11 11:33:12 -04:00
|
|
|
\index{logic!first-order}
|
|
|
|
\indexsym\emptyset{set empty}
|
|
|
|
\indexsym{\Set{}}{set}
|
|
|
|
\index{set!empty (\ensuremath{\emptyset, \{\}})}
|
2021-04-30 09:16:01 -04:00
|
|
|
The symbol $\emptyset$ represents the empty set---%
|
|
|
|
the set of zero elements.
|
|
|
|
We assume that the axioms of ZFC~set theory hold,
|
|
|
|
but define $\in$ here for clarity.
|
|
|
|
|
2021-05-11 16:50:11 -04:00
|
|
|
\todo{Introduce set-builder notation, $\union$, $\intersect$.}
|
2021-05-10 16:50:30 -04:00
|
|
|
\indexsym\in{set membership}
|
2021-05-11 11:33:12 -04:00
|
|
|
\indexsym\union{set, union}
|
|
|
|
\indexsym\intersect{set, intersection}
|
|
|
|
\index{set!membership@membership (\ensuremath\in)}
|
|
|
|
\index{set!union (\ensuremath\union)}
|
|
|
|
\index{set!intersection (\ensuremath\intersect)}
|
2021-04-30 09:16:01 -04:00
|
|
|
\begin{definition}[Set Membership]
|
2021-05-11 11:33:12 -04:00
|
|
|
$x \in S \equiv \Set{x} \intersect S \not= \emptyset.$
|
2021-04-30 09:16:01 -04:00
|
|
|
\end{definition}
|
|
|
|
|
2021-05-18 10:06:32 -04:00
|
|
|
\index{domain of discourse}
|
2021-04-30 09:16:01 -04:00
|
|
|
$\forall$ denotes first-order universal quantification (``for all''),
|
|
|
|
and $\exists$ first-order existential quantification (``there exists''),
|
2021-05-18 10:06:32 -04:00
|
|
|
over some domain of discourse.
|
2021-04-30 09:16:01 -04:00
|
|
|
|
2021-05-11 11:33:12 -04:00
|
|
|
\indexsym\exists{quantification, existential}
|
|
|
|
\index{quantification!existential (\ensuremath\exists)}
|
2021-04-30 09:16:01 -04:00
|
|
|
\begin{definition}[Existential Quantification]\dfnlabel{exists}
|
|
|
|
$\Exists{x\in X}{P(x)} \equiv
|
|
|
|
\true \in \Set{P(x) \mid x\in X}$.
|
|
|
|
\end{definition}
|
|
|
|
|
2021-05-11 11:33:12 -04:00
|
|
|
\indexsym\forall{quantification, universal}
|
|
|
|
\index{quantification!universal (\ensuremath\forall)}
|
2021-04-30 09:16:01 -04:00
|
|
|
\begin{definition}[Universal Quantification]\dfnlabel{forall}
|
|
|
|
$\Forall{x\in X}{P(x)} \equiv \neg\Exists{x\in X}{\neg P(x)}$.
|
|
|
|
\end{definition}
|
|
|
|
|
2021-05-11 11:33:12 -04:00
|
|
|
\index{quantification!vacuous truth}
|
2021-05-14 12:05:17 -04:00
|
|
|
\begin{remark}[Vacuous Truth]\remlabel{vacuous-truth}
|
2021-05-11 11:33:12 -04:00
|
|
|
By \dfnref{exists}, $\Exists{x\in\emptyset}P \equiv \false$
|
2021-04-30 09:16:01 -04:00
|
|
|
and by \dfnref{forall}, $\Forall{x\in\emptyset}P \equiv \true$.
|
2021-05-10 16:54:19 -04:00
|
|
|
And so we also have the tautologies $\infer \neg\Exists{x\in\emptyset}P$
|
|
|
|
and $\infer \Forall{x\in\emptyset}P$.
|
2021-05-18 10:06:32 -04:00
|
|
|
Empty domains lead to undesirable consequences---%
|
|
|
|
in particular,
|
|
|
|
we must carefully guard against them in \dfnref{quant-conn} and
|
|
|
|
\dfnref{quant-elim} to maintain soundness.
|
2021-04-30 09:16:01 -04:00
|
|
|
\end{remark}
|
|
|
|
|
2021-05-14 10:32:50 -04:00
|
|
|
We also have this shorthand notation:
|
|
|
|
|
|
|
|
\index{quantification!\ensuremath{\forall x,y,z}}
|
|
|
|
\index{quantification!\ensuremath{\exists x,y,z}}
|
|
|
|
\begin{align}
|
|
|
|
\Forall{x,y,z\in S}P \equiv
|
|
|
|
\Forall{x\in S}{\Forall{y\in S}{\Forall{z\in S}P}}, \\
|
|
|
|
\Exists{x,y,z\in S}P \equiv
|
|
|
|
\Exists{x\in S}{\Exists{y\in S}{\Exists{z\in S}P}}.
|
|
|
|
\end{align}
|
|
|
|
|
2021-05-18 10:06:32 -04:00
|
|
|
\begin{definition}[Quantifiers Over Connectives]\dfnlabel{quant-conn}
|
|
|
|
Assuming that $x$ is not free in $\varphi$,
|
|
|
|
\begin{alignat*}{3}
|
|
|
|
\varphi\land\Exists{x\in X}{P(x)}
|
|
|
|
&\equiv \Exists{x\in X}{\varphi\land P(x)}, \\
|
|
|
|
\varphi\lor\Exists{x\in X}{P(x)}
|
|
|
|
&\equiv \Exists{x\in X}{\varphi\lor P(x)}
|
|
|
|
\qquad&&\text{assuming $X\neq\emptyset$}.
|
|
|
|
\end{alignat*}
|
2021-04-30 09:16:01 -04:00
|
|
|
\end{definition}
|
|
|
|
|
2021-05-18 10:06:32 -04:00
|
|
|
\begin{definition}[Quantifier Elimination]\dfnlabel{quant-elim}
|
|
|
|
$\Exists{x\in X}{\varphi} \equiv \varphi$ assuming $X\neq\emptyset$
|
|
|
|
and $x$ is not free in~$\varphi$.
|
|
|
|
\end{definition}
|
2021-04-30 09:16:01 -04:00
|
|
|
|
|
|
|
|
|
|
|
\subsection{Functions}
|
2021-05-11 11:33:12 -04:00
|
|
|
\indexsym{f, g}{function}
|
|
|
|
\indexsym\mapsto{function, map}
|
|
|
|
\indexsym\rightarrow{function, domain map}
|
|
|
|
\index{function}
|
|
|
|
\index{function!map (\ensuremath\mapsto)}
|
|
|
|
\index{map|see {function}}
|
|
|
|
\index{function!domain}
|
|
|
|
\index{function!codomain}
|
|
|
|
\index{domain|see {function, domain}}
|
|
|
|
\index{function!domain map (\ensuremath\rightarrow)}
|
2021-04-30 09:16:01 -04:00
|
|
|
The notation $f = x \mapsto x' : A\rightarrow B$ represents a function~$f$
|
|
|
|
that maps from~$x$ to~$x'$,
|
|
|
|
where $x\in A$ (the domain of~$f$) and $x'\in B$ (the co-domain of~$f$).
|
|
|
|
|
2021-05-11 11:33:12 -04:00
|
|
|
\indexsym\times{set, Cartesian product}
|
|
|
|
\index{set!Cartesian product (\ensuremath\times)}
|
2021-04-30 09:16:01 -04:00
|
|
|
A function $A\rightarrow B$ can be represented as the Cartesian
|
|
|
|
product of its domain and codomain, $A\times B$.
|
|
|
|
For example,
|
|
|
|
$x\mapsto x^2 : \Int\rightarrow\Int$ is represented by the set of ordered
|
|
|
|
pairs $\Set{(x,x^2) \mid x\in\Int}$, which looks something like
|
|
|
|
|
|
|
|
\begin{equation*}
|
|
|
|
\Set{\ldots,\,(0,0),\,(1,1),\,(2,4),\,(3,9),\,\ldots}.
|
|
|
|
\end{equation*}
|
|
|
|
|
2021-05-11 11:33:12 -04:00
|
|
|
\indexsym{[\,]}{function, image}
|
|
|
|
\index{function!image (\ensuremath{[\,]})}
|
|
|
|
\index{function!as a set}
|
2021-05-18 12:16:11 -04:00
|
|
|
The set of values over which some function~$f$ ranges is its \dfn{image},
|
2021-04-30 09:16:01 -04:00
|
|
|
which is a subset of its codomain.
|
|
|
|
In the example above,
|
|
|
|
both the domain and codomain are the set of integers~$\Int$,
|
|
|
|
but the image is $\Set{x^2 \mid x\in\Int}$,
|
|
|
|
which is clearly a subset of~$\Int$.
|
|
|
|
|
|
|
|
We therefore have
|
|
|
|
|
|
|
|
\begin{align}
|
|
|
|
A \rightarrow B &\subset A\times B, \\
|
2021-05-10 16:54:19 -04:00
|
|
|
f : A \rightarrow B &\infer f \subset A\times B, \\
|
2021-04-30 09:16:01 -04:00
|
|
|
f = \alpha \mapsto \alpha' : A \rightarrow B
|
|
|
|
&= \Set{(\alpha,\alpha')
|
2021-05-13 15:50:13 -04:00
|
|
|
\mid \alpha\in A \land \alpha'\in B}, \\
|
2021-04-30 09:16:01 -04:00
|
|
|
f[D\subseteq A] &= \Set{f(\alpha) \mid \alpha\in D} \subset B, \\
|
|
|
|
f[] &= f[A].
|
|
|
|
\end{align}
|
|
|
|
|
2021-05-11 11:33:12 -04:00
|
|
|
\indexsym{()}{tuple}
|
|
|
|
\index{tuple (\ensuremath{()})}
|
|
|
|
\index{relation|see {function}}
|
2021-05-18 12:16:11 -04:00
|
|
|
An ordered pair $(x,y)$ is also called a \dfn{$2$-tuple}.
|
2021-04-30 09:16:01 -04:00
|
|
|
Generally,
|
2021-05-18 12:16:11 -04:00
|
|
|
an \dfn{$n$-tuple} is used to represent an $n$-ary function,
|
2021-04-30 09:16:01 -04:00
|
|
|
where by convention we have $(x)=x$.
|
|
|
|
So $f(x,y) = f((x,y)) = x+y$.
|
|
|
|
If we let $t=(x,y)$,
|
2021-05-10 14:08:11 -04:00
|
|
|
then we also have $f(x,y) = ft$,
|
|
|
|
which we'll sometimes write as a subscript~$f_t$ where disambiguation is
|
|
|
|
necessary and where parenthesis may add too much noise;
|
|
|
|
this notation is especially well-suited to indexes,
|
|
|
|
as in $f_1$.
|
2021-05-18 12:16:11 -04:00
|
|
|
Binary functions are often written using \dfn{infix} notation;
|
2021-04-30 09:16:01 -04:00
|
|
|
for example, we have $x+y$ rather than $+(x,y)$.
|
|
|
|
|
|
|
|
\begin{equation}
|
2021-05-10 14:08:11 -04:00
|
|
|
f_x = f(x) \in \Set{b \mid (x,b) \in f}
|
2021-04-30 09:16:01 -04:00
|
|
|
\end{equation}
|
|
|
|
|
|
|
|
|
|
|
|
\subsubsection{Binary Operations On Functions}
|
2021-05-11 11:33:12 -04:00
|
|
|
\indexsym{R}{relation}
|
2021-04-30 09:16:01 -04:00
|
|
|
Consider two unary functions $f$ and~$g$,
|
|
|
|
and a binary relation~$R$.
|
2021-05-11 11:33:12 -04:00
|
|
|
\indexsym{\bicomp{R}}{function, binary composition}
|
|
|
|
\index{function!binary composition (\ensuremath{\bicomp{R}})}
|
2021-04-30 09:16:01 -04:00
|
|
|
We introduce a notation~$\bicomp R$ to denote the composition of a binary
|
2021-05-11 11:33:12 -04:00
|
|
|
function with two unary functions.
|
2021-04-30 09:16:01 -04:00
|
|
|
|
|
|
|
\begin{align}
|
|
|
|
f &: A \rightarrow B \\
|
|
|
|
g &: A \rightarrow D \\
|
|
|
|
R &: B\times D \rightarrow F \\
|
2021-05-10 14:08:11 -04:00
|
|
|
f \bicomp{R} g &= \alpha \mapsto f_\alpha R g_\alpha : A \rightarrow F
|
2021-04-30 09:16:01 -04:00
|
|
|
\end{align}
|
|
|
|
|
2021-05-11 11:33:12 -04:00
|
|
|
\indexsym\circ{function, composition}
|
|
|
|
\index{function!composition (\ensuremath\circ)}
|
2021-04-30 09:16:01 -04:00
|
|
|
Note that $f$ and~$g$ must share the same domain~$A$.
|
|
|
|
In that sense,
|
|
|
|
this is the mapping of the operation~$R$ over the domain~$A$.
|
|
|
|
This is analogous to unary function composition~$f\circ g$.
|
|
|
|
|
2021-05-11 11:33:12 -04:00
|
|
|
\index{function!constant}
|
2021-04-30 09:16:01 -04:00
|
|
|
A scalar value~$x$ can be mapped onto some function~$f$ using a constant
|
|
|
|
function.
|
|
|
|
For example,
|
|
|
|
consider adding some number~$x$ to each element in the image of~$f$:
|
|
|
|
|
|
|
|
\begin{equation*}
|
2021-05-10 14:08:11 -04:00
|
|
|
f \bicomp+ (\_\mapsto x) = \alpha \mapsto f_\alpha + x.
|
2021-04-30 09:16:01 -04:00
|
|
|
\end{equation*}
|
|
|
|
|
2021-05-11 11:33:12 -04:00
|
|
|
\indexsym{\_}{variable, wildcard}
|
|
|
|
\index{variable!wildcard/hole (\ensuremath{\_})}
|
2021-05-11 12:47:28 -04:00
|
|
|
The symbol~$\_$ is used to denote a variable that matches anything but is
|
|
|
|
never referenced,
|
|
|
|
and is often referred to as a ``wildcard'' (since it matches anything)
|
|
|
|
or a ``hole'' (since its value goes nowhere).
|
2021-04-30 09:16:01 -04:00
|
|
|
|
|
|
|
Note that we consider the bracket notation for the image of a function
|
|
|
|
$(f:A\rightarrow B)[A]$ to itself be a binary function.
|
|
|
|
Given that, we have $f\bicomp{[]} = f\bicomp{[A]}$ for functions returning
|
2021-05-18 10:14:56 -04:00
|
|
|
functions (such as vectors of vectors in \secref{vec}).
|
2021-04-30 09:16:01 -04:00
|
|
|
|
|
|
|
|
2021-05-14 12:05:17 -04:00
|
|
|
\subsection{Monoids and Sequences}\seclabel{monoids}
|
2021-05-14 10:38:17 -04:00
|
|
|
\index{abstract algebra!monoid}
|
|
|
|
\index{monoid|see abstract algebra, monoid}
|
2021-05-14 10:32:50 -04:00
|
|
|
\begin{definition}[Monoid]\dfnlabel{monoid}
|
2021-05-26 10:38:36 -04:00
|
|
|
Let $S$ be some set. A \dfn{monoid} is a triple $\Monoid S\monoidop e$
|
2021-05-14 10:32:50 -04:00
|
|
|
with the axioms
|
|
|
|
|
|
|
|
\begin{align}
|
2021-05-26 10:38:36 -04:00
|
|
|
\monoidop &: S\times S \rightarrow S
|
2021-05-18 10:06:32 -04:00
|
|
|
\tag{Monoid Binary Closure} \\
|
2021-05-26 10:38:36 -04:00
|
|
|
\Forall{a,b,c\in S&}{
|
|
|
|
a\monoidop(b\monoidop c) = (a\monoidop b)\monoidop c)
|
|
|
|
}, \tag{Monoid Associativity} \\
|
|
|
|
\Exists{e\in S&}{\Forall{a\in S}{e\monoidop a = a\monoidop e = a}}.
|
2021-05-18 10:06:32 -04:00
|
|
|
\tag{Monoid Identity}\label{eq:monoid-identity}
|
2021-05-14 10:32:50 -04:00
|
|
|
\end{align}
|
|
|
|
\end{definition}
|
|
|
|
|
2021-05-14 10:38:17 -04:00
|
|
|
\index{abstract algebra}
|
|
|
|
\index{abstract algebra!semigroup}
|
2021-05-14 10:32:50 -04:00
|
|
|
Monoids originate from abstract algebra.
|
|
|
|
A monoid is a semigroup with an added identity element~$e$.
|
2021-05-18 12:13:32 -04:00
|
|
|
Only the identity element must be commutative,
|
2021-05-26 10:38:36 -04:00
|
|
|
but if the binary operation~$\monoidop$ is \emph{also} commutative,
|
2021-05-18 12:13:32 -04:00
|
|
|
then the monoid is a \dfn{commutative monoid}.\footnote{%
|
|
|
|
A commutative monoid is less frequently referred to as an
|
|
|
|
\dfn{abelian monoid},
|
|
|
|
related to the common term \dfn{abelian group}.}
|
2021-05-14 10:32:50 -04:00
|
|
|
|
|
|
|
Consider some sequence of operations
|
2021-05-26 10:38:36 -04:00
|
|
|
$x_0 \monoidops x_n \in S$.
|
2021-05-14 10:32:50 -04:00
|
|
|
Intuitively,
|
|
|
|
a monoid tells us how to combine that sequence into a single element
|
|
|
|
of~$S$.
|
|
|
|
When the sequence has one or zero elements,
|
|
|
|
we then use the identity element $e\in S$:
|
2021-05-26 10:38:36 -04:00
|
|
|
as $x_0 \monoidop e = x_0$ in the case of one element
|
|
|
|
or $e \monoidop e = e$ in the case of zero.
|
2021-05-14 10:32:50 -04:00
|
|
|
|
2021-05-14 10:38:17 -04:00
|
|
|
\indexsym\cdots{sequence}
|
|
|
|
\index{sequence}
|
2021-05-18 10:06:32 -04:00
|
|
|
\begin{definition}[Monoidic Sequence]\dfnlabel{monoid-seq}
|
2021-05-14 10:32:50 -04:00
|
|
|
Generally,
|
2021-05-26 10:38:36 -04:00
|
|
|
given some monoid $\Monoid S\monoidop e$ and a sequence $\Fam{x}jJ\in S$
|
2021-05-14 10:32:50 -04:00
|
|
|
where $n<|J|$,
|
|
|
|
we have
|
2021-05-26 10:38:36 -04:00
|
|
|
$x_0\monoidop x_1\monoidops x_{n-1}\monoidop x_n$
|
2021-05-14 10:32:50 -04:00
|
|
|
represent the successive binary operation on all indexed elements
|
|
|
|
of~$x$.
|
|
|
|
When it's clear from context that the index is increasing by a constant
|
|
|
|
of~$1$,
|
2021-05-26 10:38:36 -04:00
|
|
|
that notation is shortened to $x_0\monoidops x_n$ to save
|
2021-05-14 10:32:50 -04:00
|
|
|
space.
|
|
|
|
When $|J|=1$, then $n=0$ and we have the sequence $x_0$.
|
|
|
|
When $|J|=0$, then $n=-1$,
|
|
|
|
and no such sequence exists,
|
|
|
|
in which case we expand into the identity element~$e$.
|
2021-05-18 10:06:32 -04:00
|
|
|
\end{definition}
|
2021-05-14 10:32:50 -04:00
|
|
|
|
|
|
|
For example,
|
|
|
|
given the monoid~$\Monoid\Int+0$,
|
|
|
|
the sequence $1+2+\cdots+4+5$ can be shortened to
|
|
|
|
$1+\cdots+5$ and represents the arithmetic progression
|
|
|
|
$1+2+3+4+5=15$.
|
|
|
|
If $x=\Set{1,2,3,4,5}$,
|
|
|
|
$x_0+\cdots+x_n$ represents the same sequence.
|
|
|
|
If $x=\Set{1}$,
|
|
|
|
that sequence evaluates to $1=1$.
|
|
|
|
If $x=\Set{}$,
|
|
|
|
we have $0$.
|
|
|
|
|
2021-05-14 10:38:17 -04:00
|
|
|
\index{conjunction!monoid}
|
2021-05-18 10:06:32 -04:00
|
|
|
\begin{lemma}\lemlabel{monoid-land}
|
2021-05-18 12:13:32 -04:00
|
|
|
$\Monoid\Bool\land\true$ is a commutative monoid.
|
2021-05-14 10:32:50 -04:00
|
|
|
\end{lemma}
|
|
|
|
\begin{proof}
|
2021-05-18 12:13:32 -04:00
|
|
|
$\Monoid\Bool\land\true$ is associative by \dfnref{conj-assoc}
|
|
|
|
and commutative by \dfnref{conj-commut}.
|
|
|
|
The identity element is~$\true\in\Bool$ by \dfnref{conj-simpl}.
|
2021-05-14 10:32:50 -04:00
|
|
|
\end{proof}
|
|
|
|
|
2021-05-14 10:38:17 -04:00
|
|
|
\index{disjunction!monoid}
|
2021-05-18 10:06:32 -04:00
|
|
|
\begin{lemma}\lemlabel{monoid-lor}
|
2021-05-18 12:13:32 -04:00
|
|
|
$\Monoid\Bool\lor\false$ is a commutative monoid.
|
2021-05-14 10:32:50 -04:00
|
|
|
\end{lemma}
|
|
|
|
\begin{proof}
|
2021-05-18 12:13:32 -04:00
|
|
|
$\Monoid\Bool\lor\false$ is associative by \dfnref{disj-assoc}
|
|
|
|
and commutative by \dfnref{disj-commut}.
|
2021-05-14 10:32:50 -04:00
|
|
|
The identity $\false\in\Bool$ follows from
|
|
|
|
|
|
|
|
\begin{alignat*}{3}
|
|
|
|
\false \lor p &\equiv p \lor \false &&\text{by \dfnref{disj-commut}} \\
|
|
|
|
&\equiv \neg(\neg p \land \neg\false)\qquad
|
|
|
|
&&\text{by \dfnref{demorgan}} \\
|
|
|
|
&\equiv \neg(\neg p) &&\text{by \dfnref{conj-simpl}} \\
|
|
|
|
&\equiv p. &&\text{by \dfnref{double-neg}} \tag*\qedhere
|
|
|
|
\end{alignat*}
|
|
|
|
\end{proof}
|
|
|
|
|
|
|
|
|
2021-05-11 11:39:23 -04:00
|
|
|
\goodbreak% Fits well on its own page, if we're near a page boundary
|
2021-04-30 09:16:01 -04:00
|
|
|
\subsection{Vectors and Index Sets}\seclabel{vec}
|
|
|
|
\tame{} supports scalar, vector, and matrix values.
|
|
|
|
Unfortunately,
|
|
|
|
its implementation history leaves those concepts a bit tortured.
|
|
|
|
|
|
|
|
A vector is a sequence of values, defined as a function of
|
2021-05-21 16:10:44 -04:00
|
|
|
an index.
|
|
|
|
An \dfn{index~set} is a set that is used to index values from another set;
|
|
|
|
they are usually subscripts of another set.
|
|
|
|
A \dfn{family} is a set that is indexed by the same index set.
|
|
|
|
In this paper,
|
|
|
|
we assume that an index set represents a range of integer values from $0$
|
|
|
|
to some number.
|
|
|
|
|
|
|
|
\begin{definition}[Family and Index Set]
|
|
|
|
Let $S$ be a family indexed by index set~$J$.
|
|
|
|
Then,
|
|
|
|
|
|
|
|
\begin{align}
|
|
|
|
\Fam{S}jJ,\qquad J = \Set{0,1,\dots,\len{J}-1}\in\PSet\Int.
|
|
|
|
\end{align}
|
|
|
|
\end{definition}
|
|
|
|
|
|
|
|
\indexsym{\PSet{S}}{set, power set}
|
|
|
|
\index{set!power set (\ensuremath{\PSet{S}})}
|
|
|
|
$\PSet{S}$ denotes the \dfn{power set} of $S$---%
|
|
|
|
the set of all subsets of~$S$ including $\emptyset$ and $S$~itself.
|
2021-04-30 09:16:01 -04:00
|
|
|
|
2021-05-11 11:33:12 -04:00
|
|
|
% TODO: font changes in index, making langle unavailable
|
|
|
|
%\indexsym{\Vector{}}{vector}
|
|
|
|
\index{vector!definition (\ensuremath{\Vector{}})}
|
|
|
|
\index{sequence|see vector}
|
|
|
|
\indexsym\Vectors{vector}
|
|
|
|
\index{real number (\ensuremath\Real)}
|
|
|
|
\indexsym\Real{real number}
|
|
|
|
\indexsym{\Fam{a}jJ}{index set}
|
|
|
|
\index{family|see {index set}}
|
2021-05-19 10:48:35 -04:00
|
|
|
\index{index set!_@notation (\ensuremath{\Fam{a}jJ})}
|
2021-04-30 09:16:01 -04:00
|
|
|
\begin{definition}[Vector]\dfnlabel{vec}
|
|
|
|
Let $J\subset\Int$ represent an index set.
|
2021-05-18 12:16:11 -04:00
|
|
|
A \dfn{vector}~$v\in\Vectors^\Real$ is a totally ordered sequence of
|
2021-04-30 09:16:01 -04:00
|
|
|
elements represented as a function of an element of its index set:
|
|
|
|
\begin{equation}\label{vec}
|
|
|
|
v = \Vector{v_0,\ldots,v_j}^{\Real}_{j\in J}
|
|
|
|
= j \mapsto v_j : J \rightarrow \Real.
|
|
|
|
\end{equation}
|
|
|
|
\end{definition}
|
|
|
|
|
|
|
|
This definition means that $v_j = v(j)$,
|
|
|
|
making the subscript a notational convenience.
|
|
|
|
We may omit the superscript such that $\Vectors^\Real=\Vectors$
|
|
|
|
and $\Vector{\ldots}^\Real=\Vector{\ldots}$.
|
|
|
|
|
2021-05-21 16:10:44 -04:00
|
|
|
When appropriate,
|
|
|
|
a vector may also be styled in a manner similar to linear algebra,
|
|
|
|
noting that our indexes begin at $0$ instead of~$1$:
|
|
|
|
|
|
|
|
\begin{equation}
|
|
|
|
\Vector{v_0,\dots,v_j}^\Real_{j\in J} =
|
|
|
|
\begin{bmatrix}
|
|
|
|
v_0 \\
|
|
|
|
\vdots \\
|
|
|
|
v_j
|
|
|
|
\end{bmatrix}_{j\in J}
|
|
|
|
=
|
|
|
|
\begin{bmatrix}
|
|
|
|
v_0 \\
|
|
|
|
\vdots \\
|
|
|
|
v_j
|
|
|
|
\end{bmatrix}.
|
|
|
|
\end{equation}
|
|
|
|
|
|
|
|
\index{matrix@see {vector}}
|
2021-05-11 11:33:12 -04:00
|
|
|
\index{vector!matrix}
|
2021-04-30 09:16:01 -04:00
|
|
|
\begin{definition}[Matrix]\dfnlabel{matrix}
|
|
|
|
Let $J\subset\Int$ represent an index set.
|
2021-05-18 12:16:11 -04:00
|
|
|
A \dfn{matrix}~$M\in\Matrices$ is a totally ordered sequence of
|
2021-04-30 09:16:01 -04:00
|
|
|
elements represented as a function of an element of its index set:
|
|
|
|
\begin{equation}
|
|
|
|
M = \Vector{M_0,\ldots,M_j}^{\Vectors^\Real}_{j\in J}
|
|
|
|
= j \mapsto M_j : J \rightarrow \Vectors^\Real.
|
|
|
|
\end{equation}
|
|
|
|
\end{definition}
|
|
|
|
|
|
|
|
The consequences of \dfnref{matrix}---%
|
|
|
|
defining a matrix as a vector of independent vectors---%
|
|
|
|
are important.
|
|
|
|
This defines a matrix to be more like a multidimensional array,
|
|
|
|
with no requirement that the lengths of the vectors be equal.
|
|
|
|
|
|
|
|
\begin{corollary}[Matrix Row Length Variance]\corlabel{matrix-row-len}
|
2021-05-10 16:54:19 -04:00
|
|
|
$\infer \Exists{M\in\Matrices}{\neg\Forall*{j}{\Forall{k}{\len{M_j} = \len{M_k}}}}$.
|
2021-04-30 09:16:01 -04:00
|
|
|
\end{corollary}
|
|
|
|
|
|
|
|
\corref{matrix-row-len} can be read ``there exists some matrix~$M$ such that
|
|
|
|
not all row lengths of~$M$ are equal''.
|
|
|
|
In other words---%
|
|
|
|
the inner vectors of a matrix can vary in length.
|
2021-05-21 16:10:44 -04:00
|
|
|
However,
|
|
|
|
certain systems (such as that of \axmref{class-intro}) may place
|
|
|
|
restrictions by specifying the inner index set as a dependent type:
|
|
|
|
|
|
|
|
\begin{equation}
|
|
|
|
\MFam{M}jJkK : J \rightarrow K_j \rightarrow \Real, \quad K : J \rightarrow \PSet\Int.
|
|
|
|
\end{equation}
|
|
|
|
|
|
|
|
\index{vector!matrix!rectangular}
|
|
|
|
This makes $K$ a set of index sets.
|
|
|
|
When $\len{K[J]}=1$
|
|
|
|
(that is---all $K_j$ are the same index set),
|
|
|
|
the matrix is \dfn{rectangular},
|
|
|
|
and can be written in a manner similar to linear algebra,
|
|
|
|
noting that our indexes begin at $0$ instead of~$1$;
|
|
|
|
that we use double-subscripts
|
|
|
|
(since matrices are functions returning functions);
|
|
|
|
and that we use $j,k$ in place of~$m,n$.
|
|
|
|
|
|
|
|
\begin{equation}
|
|
|
|
\begin{bmatrix}
|
|
|
|
M_{0_0} & M_{0_1} & \dots & M_{0_k} \\
|
|
|
|
M_{1_0} & M_{0_1} & \dots & M_{0_k} \\
|
|
|
|
\vdots & \vdots & \ddots & \vdots \\
|
|
|
|
M_{j_0} & M_{j_1} & \dots & M_{j_k} \\
|
|
|
|
\end{bmatrix}_{\underset{k\in K_0}{j\in J}}
|
|
|
|
\qquad
|
|
|
|
\text{if $|K[J]|=1$}.
|
|
|
|
\end{equation}
|
|
|
|
We may optionally omit the domains as in the vector notation.
|
|
|
|
|
2021-05-26 13:04:55 -04:00
|
|
|
\indexsym\eleundef{undefined}
|
2021-05-21 16:10:44 -04:00
|
|
|
\index{undefined}
|
|
|
|
If a matrix is \emph{not} rectangular,
|
2021-05-26 13:04:55 -04:00
|
|
|
the symbol~$\eleundef$ can be used to explicitly denote that specific scalar
|
2021-05-21 16:10:44 -04:00
|
|
|
values are undefined;
|
|
|
|
this is useful when the matrix representation is desirable when
|
|
|
|
describing the transformation of non-rectangular data \emph{into}
|
|
|
|
rectangular data.
|
|
|
|
For example,
|
|
|
|
|
|
|
|
\begin{equation}
|
|
|
|
\begin{bmatrix}
|
|
|
|
0 & 1 & 2 \\
|
2021-05-26 13:04:55 -04:00
|
|
|
3 & 4 & \eleundef \\
|
|
|
|
5 & \eleundef & \eleundef
|
2021-05-21 16:10:44 -04:00
|
|
|
\end{bmatrix}_{\underset{k\in K_j}{j\in J}}
|
|
|
|
=
|
|
|
|
\Vector{\Vector{0,1,2},\Vector{3,4},\Vector{5}},
|
|
|
|
\qquad
|
|
|
|
\begin{aligned}
|
|
|
|
J &= \Set{0,1,2}, \\
|
|
|
|
K &= \Set{(0,\Set{0,1,2}),\,
|
|
|
|
(1,\Set{0,1}),\,
|
|
|
|
(2,\Set{0})}.
|
|
|
|
\end{aligned}
|
|
|
|
\end{equation}
|
|
|
|
|
2021-04-30 09:16:01 -04:00
|
|
|
|
2021-05-19 12:58:20 -04:00
|
|
|
% TODO: symbol does not render properly in index
|
2021-05-20 10:45:44 -04:00
|
|
|
\begin{definition}[Rank]\dfnlabel{rank}
|
2021-05-19 12:58:20 -04:00
|
|
|
\index{rank}
|
|
|
|
The \dfn{rank} of some variable~$x$ is an integer value
|
|
|
|
\begin{equation*}
|
2021-05-20 15:28:10 -04:00
|
|
|
\rank{x} =
|
2021-05-19 12:58:20 -04:00
|
|
|
\begin{cases}
|
|
|
|
2 &x\in\Matrices, \\
|
|
|
|
1 &x\in\Vectors^\Real, \\
|
|
|
|
0 &x\in\Real.
|
|
|
|
\end{cases}
|
|
|
|
\end{equation*}
|
|
|
|
\end{definition}
|
|
|
|
|
|
|
|
Intuitively, the rank represents the number of dimensions of some variable~$x$.
|
|
|
|
A scalar has zero dimensions (a point);
|
|
|
|
a vector has one (a line);
|
|
|
|
and a matrix has two (a plane).
|
|
|
|
\index{dimensions@see {rank}}
|
|
|
|
\index{rank!dimensions}
|
|
|
|
In \tame{},
|
|
|
|
the rank is referred to as \dfn{dimensions} using the attribute
|
|
|
|
\xmlattr{dim}.
|
|
|
|
|
2021-04-30 09:16:01 -04:00
|
|
|
|
|
|
|
\subsection{XML Notation}
|
2021-05-11 11:33:12 -04:00
|
|
|
\indexsym{\xml{<>}}{XML}
|
|
|
|
\index{XML!notation (\xml{<>})}
|
2021-04-30 09:16:01 -04:00
|
|
|
The grammar of \tame{} is XML.
|
|
|
|
Equivalence relations will be used to map source expressions to an
|
|
|
|
underlying mathematical expression.
|
|
|
|
For example,
|
|
|
|
|
|
|
|
\begin{equation*}
|
2021-05-19 13:06:40 -04:00
|
|
|
\xml{<foo bar="$x$" baz="$y$" />} \equiv x = y
|
2021-04-30 09:16:01 -04:00
|
|
|
\end{equation*}
|
|
|
|
|
|
|
|
\noindent
|
2021-05-19 13:06:40 -04:00
|
|
|
defines that pattern of \xmlnode{foo} expression to be materially
|
2021-04-30 09:16:01 -04:00
|
|
|
equivalent to~$x=y$---%
|
|
|
|
anywhere an equality relation appears,
|
|
|
|
you could equivalently replace it with that XML representation without
|
|
|
|
changing the meaning of the mathematical expression.
|
2021-05-19 13:06:40 -04:00
|
|
|
|
|
|
|
Variables may also bind to literals in an XML expression.
|
|
|
|
For example,
|
|
|
|
|
|
|
|
\begin{equation*}
|
|
|
|
\xml{<quux $\alpha$ />},\qquad\alpha\in\Set{\emptystr, \xml{bar="baz"}}
|
|
|
|
\end{equation*}
|
|
|
|
|
|
|
|
\noindent
|
|
|
|
can represent either \xml{<quux />} or \xml{<quux bar="baz" />}.
|
|
|
|
\index{empty string}
|
|
|
|
$\emptystr$~represents the empty string.
|
|
|
|
Any text typeset in \texttt{typewriter} represents a literal
|
|
|
|
string of characters.
|