diff --git a/.gitignore b/.gitignore index 7a432f50..4221f3e0 100644 --- a/.gitignore +++ b/.gitignore @@ -10,12 +10,12 @@ /bin/dslc /build-aux/install-sh /build-aux/missing -confdefs.h -Makefile.in -Makefile -aclocal.m4 -*.cache/ -configure +/confdefs.h +/Makefile.in +/Makefile +/aclocal.m4 +/*.cache/ +/configure /config.* # should be added using autoreconf -i diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 41cde868..b0ac9f2b 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -27,12 +27,25 @@ build: - tamer/target expire_in: 30 min +build:doc:tpl: + image: $BUILD_IMAGE_TEXLIVE + stage: build + script: + - cd design/tpl/ + - make + artifacts: + paths: + - design/tpl/tpl.pdf + expire_in: 30 min + pages: stage: deploy script: - mkdir -p public/doc - mv doc/tame.html/* doc/tame.pdf doc/tame.info public/ - mv tamer/target/doc public/tamer/ + - mkdir -p public/design + - mv design/tpl/tpl.pdf public/design/ artifacts: paths: - public/ diff --git a/design/tpl/.gitignore b/design/tpl/.gitignore new file mode 100644 index 00000000..480e7bd9 --- /dev/null +++ b/design/tpl/.gitignore @@ -0,0 +1,26 @@ +# Ignored files for The TAME Programming Language Git repository + +# Targets +*.pdf +*.dvi + +# (La)TeX +*.aux +*.fls +*.log +*.out +*.toc + +# Glossary +*.glg +*.glo +*.gls +*.ist + +# Index +*.idx +*.ilg +*.ind + +# latexmk +*.fdb_latexmk diff --git a/design/tpl/.latexmkrc b/design/tpl/.latexmkrc new file mode 100644 index 00000000..287faec1 --- /dev/null +++ b/design/tpl/.latexmkrc @@ -0,0 +1,12 @@ + +add_cus_dep('glo', 'gls', 0, 'run_makeglossaries'); +add_cus_dep('acn', 'acr', 0, 'run_makeglossaries'); + +sub run_makeglossaries { + if ( $silent ) { + system "makeglossaries -q '$_[0]'"; + } + else { + system "makeglossaries '$_[0]'"; + }; +} diff --git a/design/tpl/Makefile b/design/tpl/Makefile new file mode 100644 index 00000000..7e31131d --- /dev/null +++ b/design/tpl/Makefile @@ -0,0 +1,14 @@ + +inputs := tpl.tex tpl.sty glossary.tex \ + $(wildcard sec/*.tex) + + +.DEFAULT: pdf + +.PHONY: pdf +pdf: tpl.pdf +tpl.pdf: tpl.tex $(inputs) + latexmk --pdf $< + +clean: + latexmk -c diff --git a/design/tpl/README.md b/design/tpl/README.md new file mode 100644 index 00000000..3af84944 --- /dev/null +++ b/design/tpl/README.md @@ -0,0 +1,18 @@ +# The TAME Programming Language: Design and Implementation + +This is a living document providing a formal definition of the TAME +programming language. + +## Dependencies +See [`tpl.sty`](tpl.sty) for the specific LaTeX packages that are +needed. If you use a Debian-based system, the following command should be +sufficient to install all necessary dependencies: + +``` +$ apt install --no-recommends \ + make latexmk \ + texlive-latex-extra texlive-fonts-extra texlive-science +``` + +## Building +Simply run `make`. The output is `tpl.pdf`. diff --git a/design/tpl/glossary.tex b/design/tpl/glossary.tex new file mode 100644 index 00000000..8cc692d3 --- /dev/null +++ b/design/tpl/glossary.tex @@ -0,0 +1,169 @@ +% The TAME Programming Language glossary +% +% Copyright (C) 2021 Ryan Specialty Group, LLC. +% +% Licensed under the Creative Commons Attribution-ShareAlike 4.0 +% International License. +%% + +\makeglossaries + +\newacronym{tamer}{\textsc{Tamer}}{\tame{} in Rust} + +\newglossaryentry{classification} +{ + name={classification}, + description={TODO} +} + +\newglossaryentry{free variable} +{ + name={free variable}, + description={a variable that is not a \gls{bound variable}} +} + +\newglossaryentry{bound variable} +{ + name={bound variable}, + description={} +} + +\newglossaryentry{predicate} +{ + name={predicate}, + description={} +} + +\newglossaryentry{boolean} +{ + name={boolean}, + description={a value of \gls{true} or \gls{false}}, + symbol={\Bool}, +} + +\newglossaryentry{true} +{ + name={true}, + description={boolean value representing ``true''}, + symbol={\true}, +} + +\newglossaryentry{false} +{ + name={false}, + description={boolean value representing ``false''}, + symbol={\false}, +} + +\newglossaryentry{conjunction} +{ + name={conjunction}, + description={logical conjunction (``and'')}, + symbol={\ensuremath{\logand}}, +} +\newglossaryentry{disjunction} +{ + name={disjunction}, + description={logical disjunction (``or'')}, + symbol={\ensuremath{\logor}}, +} + +\newglossaryentry{cardinality} +{ + name={cardinality}, + description={number of elements in some set~$S$}, + symbol={\ensuremath{|S|}} +} + +\newglossaryentry{family} +{ + name={family}, + description={a set sharing the same \gls{index set}}, + symbol={\ensuremath{\{A_j\}_{j\in J}}} +} + +\newglossaryentry{index set} +{ + name={index set}, + description={a set whose members index members of another set; see also + \gls{family}}, +} + +\newglossaryentry{castable} +{ + name={castable}, + description={type $A$ is castable to type $B$ if there exists some + \gls{surjective} function $A\rightarrow B$} +} + +\newglossaryentry{surjective} +{ + name={surjective}, + description={$\forall y\in Y : \exists x\in X : f(x) = y$}, +} + +\newglossaryentry{equivalent} +{ + name={equivalent}, + description={an equivalence relation is a reflexive, symmetric, and + transitive binary operation}, +} + +\newglossaryentry{logical equivalence} +{ + name={logical equivalence}, + description={$p$ and $q$ are logically equivalent ($p\equiv q$) \gls{iff} + both $q$ and~$p$ are~\true or both are~\false}, + symbol={\ensuremath{\equiv}}, +} + +\newglossaryentry{logical implication} +{ + name={logical implication}, + description={}, + symbol={\ensuremath{\implies}}, +} + +\newglossaryentry{iff} +{ + name={iff}, + description={if and only if}, + symbol={\ensuremath{\iff}}, +} + +\newglossaryentry{forall} +{ + name={universal quantification}, + description={expresses a predicate that must be satisfied for every + element in a \gls{domain}}, + symbol={\ensuremath{\forall}}, +} + +\newglossaryentry{exists} +{ + name={existential quantification}, + description={expresses a predicate that must be satisfied for some + element in a \gls{domain}}, + symbol={\ensuremath{\exists}}, +} + +\newglossaryentry{domain} +{ + name={domain of discourse}, + description={set of elements over which variables of interest may range}, + symbol={\ensuremath{\mathbb{D}}}, +} + +\newglossaryentry{integer} +{ + name={integer}, + description={set of all integers}, + symbol={\ensuremath{\mathbb{Z}}}, +} + +\newglossaryentry{empty set} +{ + name={empty set}, + description={set of zero elements}, + symbol={\ensuremath{\emptyset}} +} diff --git a/design/tpl/sec/class.tex b/design/tpl/sec/class.tex new file mode 100644 index 00000000..2413c406 --- /dev/null +++ b/design/tpl/sec/class.tex @@ -0,0 +1,132 @@ + +\section{Classification System}\seclabel{class} +\index{classification} +A \gls{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 \emph{first-order sentences}---% + that is, + they contain no \glspl{free variable}. +Intuitively, + this means that all variables within a~classification are + \emph{tightly coupled} to the classification itself. +This limitation is mitigated through use of the template system. + +For example, + consider the following classification \tameclass{cost-exceeded}. +Let~\tameparam{cost} be a scalar parameter. + +\index{classification!classify@\xmlnode{classify}} +\begin{lstlisting} + + + +\end{lstlisting} + +\noindent +is then equivalent to the proposition + +\begin{equation*} + \tameclass{cost-exceeded} \equiv \tameparam{cost} > 100.00. +\end{equation*} + +\index{classification!domain} +A classification is either \glssymbol{true} or~\glssymbol{false}. +Let $\tameparam{cost}=150.00$. +Then, + +\begin{align*} + \tameclass{cost-exceeded} & \equiv \tameparam{cost} > 100.00 \\ + & \equiv 150.00 > 100.00 \\ + & \equiv \true. +\end{align*} + +Each \xmlnode{match} of a classification is a~\gls{predicate}. +Multiple predicates are by default joined by \gls{conjunction}: + +\begin{lstlisting} + + + + +\end{lstlisting} + +\noindent +is equivalent to the proposition + +\begin{equation*} + \tameclass{pool-hazard} \equiv \tameparam{diving\_board} + \logand \tameparam{pool\_depth\_ft} < 8. +\end{equation*} + +\index{classification!universal} +\begin{definition}[Universal Classification]\dfnlabel{classu} + A classification~$c$ by default performs \gls{conjunction} on its match + expressions $M_0\ldots M_n$. + + \begin{alignat*}{2} + &\xml{} \\ + &\quad M_0 \\ + &\quad \vdots \\ + &\quad M_n \\ + &\xml{} + &&\equiv c\in\Bool \\ + & &&\equiv \exists\left( M_0 \logand \ldots \logand M_n \right). + \end{alignat*} +\end{definition} + +\index{classification!existential} +\begin{definition}[Existential Classification]\dfnlabel{classe} + A classification~$c$ with the attribute \xpath{@any="true"} performs + \gls{disjunction} on its match expressions $M_0\ldots M_n$. + + \begin{alignat*}{2} + &\xml{} \\ + &\quad M_0 \\ + &\quad \vdots \\ + &\quad M_n \\ + &\texttt{} + &&\equiv c\in\Bool \\ + & &&\equiv \exists\left( M_0 \logor \ldots \logor M_n \right). + \end{alignat*} +\end{definition} + + +\subsection{Matches} +\begin{definition}[Match Equality] + \begin{equation*} + \xml{} \equiv x = y. + \end{equation*} +\end{definition} + +\begin{definition}[Match Equality Short Form] + \begin{equation*} + \xml{} + \equiv \xml{}. + \end{equation*} +\end{definition} + +\begin{definition}[Match Equality Long Form] + \begin{alignat*}{2} + \xml{} + &\equiv {}&&\xml{} \\ + & &&\quad \xml{} \\ + & &&\quad\quad \xml{} \\ + & &&\quad \xml{} \\ + & &&\xml{} \\ + &\equiv {}&&\xml{}. + \end{alignat*} +\end{definition} + +\begin{definition}[Match Membership Equivalence] + When $T$ is a type defined with \xmlnode{typedef}, + + \begin{equation*} + \xml{} \equiv x \in T. + \end{equation*} +\end{definition} diff --git a/design/tpl/sec/notation.tex b/design/tpl/sec/notation.tex new file mode 100644 index 00000000..74a4a4d1 --- /dev/null +++ b/design/tpl/sec/notation.tex @@ -0,0 +1,319 @@ + +\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} +\index{boolean!false@\false{}}% +\index{boolean!true@\true{}}% +\index{boolean!FALSE@\tamefalse{}}% +\index{boolean!TRUE@\tametrue{}}% +\index{integer (\Int)}% +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 symbol $\vdash$ means ``infer''. +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. + +\begin{definition}[Logical Conjunction] + $p,q \vdash (p\logand q)$. +\end{definition} + +\begin{definition}[Logical Disjunction] + $p \vdash (p\logor q)$ and $q \vdash (p\logor q)$. +\end{definition} + +\begin{definition}[Law of Excluded Middle] + $\vdash (p \logor \neg p)$. +\end{definition} + +\begin{definition}[Law of Non-Contradiction] + $\vdash \neg(p \logand \neg p)$. +\end{definition} + +\begin{definition}[De Morgan's Theorem] + $\neg(p \logand q) \vdash (\neg p \logor \neg q)$ + and $\neg(p \logor q) \vdash (\neg p \logand \neg q)$. +\end{definition} + +\index{equivalence!material (\ensuremath{\equiv})} +\begin{definition}[Material Equivalence] + $p\equiv q \vdash \big((p \logand q) \logor (\neg p \logand \neg q)\big)$. +\end{definition} + +$\equiv$ denotes a logical identity. +Consequently, + it'll often be used as a definition operator. + +\begin{definition}[Logical Implication] + $p\implies q \vdash (\neg p \logor q)$. +\end{definition} + +\begin{definition}[Truth Values]\dfnlabel{truth-values} + $\vdash\true$ and $\vdash\neg\false$. +\end{definition} + + +\subsection{First-Order Logic and Set Theory} +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. + +\index{set!membership@membership (\ensuremath{\in})} +\begin{definition}[Set Membership] + $x \in S \equiv \Set{x} \cap S \not= \emptyset.$ +\end{definition} + +\index{quantification|see {fist-order logic}} +\index{first-order logic!quantification (\ensuremath{\forall, \exists})} +$\forall$ denotes first-order universal quantification (``for all''), + and $\exists$ first-order existential quantification (``there exists''), + over some \gls{domain}. + +\index{disjunction|see {first-order logic}} +\index{first-order logic!disjunction (\ensuremath{\logor})} +\begin{definition}[Existential Quantification]\dfnlabel{exists} + $\Exists{x\in X}{P(x)} \equiv + \true \in \Set{P(x) \mid x\in X}$. +\end{definition} + +\index{conjunction|see {first-order logic}} +\index{first-order logic!conjunction (\ensuremath{\logand})} +\begin{definition}[Universal Quantification]\dfnlabel{forall} + $\Forall{x\in X}{P(x)} \equiv \neg\Exists{x\in X}{\neg P(x)}$. +\end{definition} + +\index{set!empty (\ensuremath{\emptyset, \{\}})} +\begin{remark}[Vacuous Truth] + By Definition~7, $\Exists{x\in\emptyset}P \equiv \false$ + and by \dfnref{forall}, $\Forall{x\in\emptyset}P \equiv \true$. + And so we also have the tautologies $\vdash \neg\Exists{x\in\emptyset}P$ + and $\vdash \Forall{x\in\emptyset}P$. +\end{remark} + +\begin{definition}[Boolean/Integer Equivalency]\dfnlabel{bool-int} + $\Set{0,1}\in\Int, \false \equiv 0$ and $\true \equiv 1$. +\end{definition} + +\tamefalse{} and~\tametrue{} are constants in \tame{} mapping to the + \gls{integer} values $\{0,1\}\in\Int$. +\dfnref{bool-int} relates these constants to their + \gls{boolean} counterparts so that they may be used in numeric contexts + and vice-versa. + + +\subsection{Functions} +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$). + +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*} + +The set of values over which some function~$f$ ranges is its \emph{image}, + 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, \\ + f : A \rightarrow B &\vdash f \subset A\times B, \\ + f = \alpha \mapsto \alpha' : A \rightarrow B + &= \Set{(\alpha,\alpha') + \mid \alpha\in A \logand \alpha'\in B}, \\ + f[D\subseteq A] &= \Set{f(\alpha) \mid \alpha\in D} \subset B, \\ + f[] &= f[A]. +\end{align} + +And ordered pair $(x,y)$ is also called a \emph{$2$-tuple}. +Generally, + an \emph{$n$-tuple} is used to represent an $n$-ary function, + where by convention we have $(x)=x$. +So $f(x,y) = f((x,y)) = x+y$. +If we let $t=(x,y)$, + then we also have $f(x,y) = ft$. +Binary functions are often written using \emph{infix} notation; + for example, we have $x+y$ rather than $+(x,y)$. + +\begin{equation} + fx \in \Set{b \mid (x,b) \in f} +\end{equation} + + +\subsubsection{Binary Operations On Functions} +Consider two unary functions $f$ and~$g$, + and a binary relation~$R$. +We introduce a notation~$\bicomp R$ to denote the composition of a binary + function with two unary functions.\footnote{% + The notation originates from~$\circ$ to denote ordinary function + composition, + as in $(f\circ g)(x) = f(g(x))$.} + +\begin{align} + f &: A \rightarrow B \\ + g &: A \rightarrow D \\ + R &: B\times D \rightarrow F \\ + f \bicomp{R} g &= \alpha \mapsto f(\alpha)Rg(\alpha) : A \rightarrow F +\end{align} + +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$. + +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*} + f \bicomp+ (\_\mapsto x) = \alpha \mapsto f(\alpha) + x. +\end{equation*} + +The symbol~$\_$ is used to denote a variable that is never referenced. + +For convenience, + we also define $\bicompi{R}$, + which recursively handles combinations of function and scalar values. +This notation is used to simplify definitions of the classification system + (see \secpref{class}) + when dealing with vectors + (see \secref{vec}). + +\begin{equation}\label{eq:bicompi} + \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),\\ + \gamma \mapsto \alpha(\gamma) \bicompi{R} (\_ \mapsto \beta) + &\text{if } (\alpha : A\rightarrow B) \logand (\beta \in\Real),\\ + \alpha R \beta &\text{otherwise}. + \end{cases} +\end{equation} + +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 + functions (such as vectors of vectors in \secref{vec}), + noting that $\bicompi{[]}$ is \emph{not} a sensible construction. + + +\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 + an~\gls{index set}. + +\begin{definition}[Vector]\dfnlabel{vec} + Let $J\subset\Int$ represent an index set. + A \emph{vector}~$v\in\Vectors^\Real$ is a totally ordered sequence of + 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}$. + +\begin{definition}[Matrix]\dfnlabel{matrix} + Let $J\subset\Int$ represent an index set. + A \emph{matrix}~$M\in\Matrices$ is a totally ordered sequence of + 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} + $\vdash \Exists{M\in\Matrices}{\neg\Forall*{j}{\Forall{k}{\len{M_j} = \len{M_k}}}}$. +\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. + +Since a vector is a function, + a vector or matrix can be converted into a set of unique elements like so: + +\begin{alignat*}{2} + \bigcup\Vector{\Vector{0,1},\Vector{2,2},\Vector{2,0}}\!\bicomp{[]} + &\mapsto &&\bigcup\Vector{\Vector{0,1}\![],\Vector{2,2}\![],\Vector{2,0}[]}\![] \\ + &\mapsto &&\bigcup\Vector{\Set{0,1},\Set{2},\Set{2,0}}\![] \\ + &\mapsto &&\bigcup\Set{\Set{0,1},\Set{2},\Set{2,0}} \\ + &= &&\Set{0,1,2}. +\end{alignat*} + +We can also add two vectors, and scale them: + +\begin{align*} + 1 \bicomp{+} \Vector{1,2,3} \bicomp{+} \Vector{4,5,6} + &= \Vector{1+1,\, 2+1,\, 3+1} \bicomp{+} \Vector{4,5,6} \\ + &= \Vector{2,3,4} \bicomp{+} \Vector{4,5,6} \\ + &= \Vector{2+4,\, 3+5,\, 4+6} \\ + &= \Vector{6, 8, 10}. +\end{align*} + + +\subsection{XML Notation} +\index{XML} +The grammar of \tame{} is XML. +Equivalence relations will be used to map source expressions to an + underlying mathematical expression. +For example, + +\begin{equation*} + \xml{} \equiv x = y +\end{equation*} + +\noindent +defines that pattern of \xmlnode{match} expression to be materially + 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. diff --git a/design/tpl/tpl.sty b/design/tpl/tpl.sty new file mode 100644 index 00000000..47b7f2b3 --- /dev/null +++ b/design/tpl/tpl.sty @@ -0,0 +1,125 @@ +% The TAME Programming Language glossary +% +% Copyright (C) 2021 Ryan Specialty Group, LLC. +% +% Licensed under the Creative Commons Attribution-ShareAlike 4.0 +% International License. +%% + +% Concrete Mathematics fonts +\usepackage[amsfonts,amssymb]{concmath} + +\usepackage{makeidx} +\usepackage[toc]{glossaries} + +% Note that we force draft=false so hyperlinks always appear +\usepackage[colorlinks=true,linkcolor=href,draft=false]{hyperref} + +% For displaying source code (e.g. XML) +\usepackage{listings} + +% Definitions, theorems, proofs, etc +\usepackage{amsthm} + +% Line spacing instead of indentation for paragraphs +%\usepackage[parfill]{parskip} + +\usepackage{xcolor} + +% To aid in defining star commands +\usepackage{suffix} + +% Creating custom symbols +\usepackage{stackengine} + +% Colors from Tango Icon Theme +% https://en.wikipedia.org/wiki/Tango_Desktop_Project +\definecolor{href}{HTML}{204a87} + +% TAME is typeset in smallcaps +\newcommand{\tame}{\textsc{Tame}} +\newcommand{\tamer}{\gls{tamer}} + +% TODO: highlighting +\lstset{ + language=XML, + basicstyle=\ttfamily, + columns=fullflexible, + keepspaces=true, + showstringspaces=false, +} + + +\newcommand\xpath[1]{\texttt{#1}} +\newcommand\xmlnode[1]{\texttt{#1}} +\newcommand\xmlattr[1]{@\texttt{#1}} + +\newcommand\tameparam[1]{\texttt{#1}} +\newcommand\tameclass[1]{\texttt{#1}} +\newcommand\tameconst[1]{\texttt{#1}} + +\newcommand\true{\ensuremath{\top}} +\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}} + +\newcommand\Int{\ensuremath{\mathbb{Z}}} +\newcommand\Real{\ensuremath{\mathbb{R}}} + +\newcommand\Set[1]{\ensuremath{\left\{#1\right\}}} +\newcommand\Fam[3]{\ensuremath{\left\{#1_{#2}\right\}_{#2\in #3}}} + +\newcommand\Vectors{\ensuremath{\mathcal{V}}} +\newcommand\Vector[1]{\ensuremath{\left\langle#1\right\rangle}} +\newcommand\VFam[3]{\ensuremath{\Vector{#1_{#2}}_{#2\in #3}}} +\newcommand\Matrices{\ensuremath{\Vectors^{\Vectors^\Real}}} + +\let\union\cup + +\newcommand\len[1]{\ensuremath{\left|#1\right|}} + +\numberwithin{equation}{section} + +% Allows us to switch between styles, if need be +% (e.g. I used the colon style before adopting notation from type theory +% where the colon became ambiguous) +\newcommand\Forall{\@ifstar\@Forallstar\@Forall} +\newcommand\@Forall[2]{\forall #1\left(#2\right)} +\newcommand\@Forallstar[2]{\forall #1 #2} + +\newcommand\Exists{\@ifstar\@Existsstar\@Exists} +\newcommand\@Exists[2]{\exists #1\left(#2\right)} +% Without \left and \right. You'll also need this if you use `&' in an +% `align' environment within an argument. +\newcommand\@Existsstar[2]{\exists #1 #2} + +\theoremstyle{definition} +\newtheorem{definition}{Definition}[section] +\newcommand\dfnlabel[1]{\label{dfn:#1}} +\newcommand\dfnref[1]{Definition~\ref{dfn:#1}} +\newcommand\dfnpref[1]{Definition~\pref{dfn:#1}} + +\theoremstyle{plain} +\newtheorem{corollary}{Corollary}[section] +\newcommand\corlabel[1]{\label{cor:#1}} +\newcommand\corref[1]{Corollary~\ref{cor:#1}} +\newcommand\corpref[1]{Corollary~\pref{cor:#1}} + +\theoremstyle{remark} +\newtheorem{remark}{Remark}[section] + +\newcommand\pref[1]{\ref{#1} on page~\pageref{#1}} +\newcommand\seclabel[1]{\label{sec:#1}} +\newcommand\secref[1]{Section~\ref{sec:#1}} +\newcommand\secpref[1]{Section~\pref{sec:#1}} + +% Binary function composition +\newcommand\bicomp[1]{\ensurestackMath{\stackon[1pt]{#1}{{}_\circ}}} +\newcommand\bicompi[1]{\ensurestackMath{\stackon[1pt]{#1}{{}_\bullet}}} + +\let\xml\texttt diff --git a/design/tpl/tpl.tex b/design/tpl/tpl.tex new file mode 100644 index 00000000..eed2e813 --- /dev/null +++ b/design/tpl/tpl.tex @@ -0,0 +1,65 @@ +% The TAME Programming Language Living Document +% +% Copyright (C) 2021 Ryan Specialty Group, LLC. +% +% Licensed under the Creative Commons Attribution-ShareAlike 4.0 +% International License. +%% + +\documentclass[draft,toc=index]{scrartcl} +\usepackage[draft=false]{scrlayer-scrpage} +\usepackage{tpl} + +\title{The TAME Programming Language} +\subtitle{Design and Implementation (Living Document)} + +\author{Mike Gerwitz} +\date{April 2021}% TODO dynamic + +% Copyright notice for bottom of first page +\cfoot[% + \tiny Copyright \textcopyright{} 2021 Ryan Specialty Group, LLC. + CC-BY-SA 4.0.]{\thepage} + +% Begin section numbering at 0 to emphasize that it's foundational material +% not directly related to TAME itself +\setcounter{section}{-1} + +\makeindex +\input{glossary.tex} + +\begin{document} + +\maketitle + +\begin{abstract} + \tame{} is The Algebraic Metalanguage, a programming language and + collection of tools designed to aid in the development, understanding, + and maintenance of systems performing numerous calculations on a + complex graph of dependencies, conditions, and a large number of + inputs. \tame{} has existed for over a decade, and while its initial + design was successful and still in active use today, it does suffer + from inconsistencies and tradeoffs that introduce certain impediments + to users of the language, and compromise future optimizations and + language evolution. It also lacks documentation not just of the + language itself, but also of the underlying principles and + implementation. + + This document is an attempt to formally consider certain parts of + \tame{} as it undergoes redesign and reimplementation as part of the + \tamer{} project. It is considered a living document---it is not + likely to ever be a finished work. +\end{abstract} + + +\tableofcontents + +\input{sec/notation.tex} +\input{sec/class.tex} + +\clearpage +\printglossary[style=altlong4col] +\printindex + +\end{document} +