diff --git a/asllib/aslspec/builtins.spec b/asllib/aslspec/builtins.spec
index 60b2f01224..7b03ecbd5f 100644
--- a/asllib/aslspec/builtins.spec
+++ b/asllib/aslspec/builtins.spec
@@ -16,9 +16,6 @@ variadic operator cond_op[T](cases: list1(T)) -> T
   prose_application = "\begin{itemize}{cases}\end{itemize}",
 };
 
-// This constant is for internal use only.
-constant bot { "bottom", math_macro = \bot };
-
 constant None {
   "the  \hyperlink{constant-None}{empty} \optionalterm{}"
 };
diff --git a/asllib/aslspec/spec.ml b/asllib/aslspec/spec.ml
index 4e4b2bfde4..7c1ff7e824 100644
--- a/asllib/aslspec/spec.ml
+++ b/asllib/aslspec/spec.ml
@@ -3459,7 +3459,7 @@ let make_spec_with_builtins ast =
   {
     ast;
     id_to_defining_node;
-    bottom_constant = get_constant "bot";
+    bottom_constant = Constant.make "bot" None None [];
     bottom_term = Label "bot";
     none_constant = get_constant "None";
     empty_set = get_constant "empty_set";
@@ -3475,6 +3475,19 @@ let make_spec_with_builtins ast =
     field_to_containing_variant = make_field_to_containing_variant ast;
   }
 
+(** [remove_bottom_constant spec] removes the bottom constant from [spec], since
+    it is only used for typechecking and should not be rendered. *)
+let remove_bottom_constant spec =
+  let ast =
+    List.filter
+      (function
+        | Elem_Constant { Constant.name; _ } when String.equal name "bot" ->
+            false
+        | _ -> true)
+      spec.ast
+  in
+  { spec with ast }
+
 let from_ast ast =
   let spec = make_spec_with_builtins ast in
   let () = Check.check_no_undefined_ids spec in
@@ -3489,4 +3502,5 @@ let from_ast ast =
   let spec = ExtendNames.extend spec in
   let () = Check.CheckRules.check spec in
   let spec = add_default_rule_renders spec in
+  let spec = remove_bottom_constant spec in
   spec
diff --git a/asllib/aslspec/tests.t/hello.expected b/asllib/aslspec/tests.t/hello.expected
index 86067c490c..7b820776cb 100644
--- a/asllib/aslspec/tests.t/hello.expected
+++ b/asllib/aslspec/tests.t/hello.expected
@@ -16,8 +16,6 @@
 % Macros for elements
 % -------------------
 
-\DefineConstant{bot}{\texthypertarget{constant-bot}$\bot$} % EndDefineConstant
-
 \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
 
 \DefineConstant{empty_set}{\texthypertarget{constant-emptyset}$\emptyset$} % EndDefineConstant
diff --git a/asllib/aslspec/tests.t/operators.expected b/asllib/aslspec/tests.t/operators.expected
index c8241ef64e..08f0b58ad2 100644
--- a/asllib/aslspec/tests.t/operators.expected
+++ b/asllib/aslspec/tests.t/operators.expected
@@ -15,8 +15,6 @@
 % Macros for elements
 % -------------------
 
-\DefineConstant{bot}{\texthypertarget{constant-bot}$\bot$} % EndDefineConstant
-
 \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
 
 \DefineConstant{empty_set}{\texthypertarget{constant-emptyset}$\emptyset$} % EndDefineConstant
@@ -52,8 +50,8 @@ The relation
 \DefineProse{f}{
 \AllApply
   \begin{itemize}
-    \item the sum of all numbers in  (1) \texttt{a}, and  (2) \texttt{b} is equal to \texttt{c};
-    \item define \texttt{d} as: if \texttt{a} is in \texttt{S} then \texttt{b} else \texttt{c};
+    \item the sum of \texttt{a} and \texttt{b} is equal to \texttt{c}
+    \item define \texttt{d} as: if \texttt{a} is in \texttt{S} then \texttt{b} else \texttt{c}
     \item \textbf{the result is:} \texttt{d}.
   \end{itemize}
 } % EndDefineProse
diff --git a/asllib/aslspec/tests.t/relations.expected b/asllib/aslspec/tests.t/relations.expected
index 491e1e44eb..447aa61720 100644
--- a/asllib/aslspec/tests.t/relations.expected
+++ b/asllib/aslspec/tests.t/relations.expected
@@ -23,8 +23,6 @@
 % Macros for elements
 % -------------------
 
-\DefineConstant{bot}{\texthypertarget{constant-bot}$\bot$} % EndDefineConstant
-
 \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
 
 \DefineConstant{empty_set}{\texthypertarget{constant-emptyset}$\emptyset$} % EndDefineConstant
diff --git a/asllib/aslspec/tests.t/rule.expected b/asllib/aslspec/tests.t/rule.expected
index 160c8b2fc6..087bcffd83 100644
--- a/asllib/aslspec/tests.t/rule.expected
+++ b/asllib/aslspec/tests.t/rule.expected
@@ -17,8 +17,6 @@
 % Macros for elements
 % -------------------
 
-\DefineConstant{bot}{\texthypertarget{constant-bot}$\bot$} % EndDefineConstant
-
 \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
 
 \DefineConstant{empty_set}{\texthypertarget{constant-emptyset}$\emptyset$} % EndDefineConstant
@@ -79,10 +77,10 @@ The relation
 \DefineProse{r}{
 \AllApply
   \begin{itemize}
-    \item define \texttt{res} as  (1) if \texttt{a} is equal to \texttt{b} holds then \texttt{a},  (2) if \texttt{a} is greater than \texttt{b} holds then the sum of  (1) \texttt{a}, and  (2) \texttt{b}, and  (3) if \texttt{a} is less than \texttt{b} holds then \texttt{b};
-    \item define \texttt{y} as the rec record with $\Fieldf$ value \texttt{a} and $\Fieldg$ value \texttt{b};
-    \item define \texttt{r\_f} as the sum of  (1) the field $\FIELDf$ of \texttt{r}, and  (2) the field $\FIELDg$ of \texttt{r};
-    \item define \texttt{r'} as \texttt{r} with $\FIELDf$ updated to \texttt{res};
-    \item \textbf{the result is:} the pair consisting of \texttt{res} (for the output variable \texttt{c}) and \texttt{r'}.
+    \item define \texttt{res} as \begin{itemize}\item \texttt{a} if \texttt{a} is equal to \texttt{b}, \item the sum of \texttt{a} and \texttt{b} if \texttt{a} is greater than \texttt{b}, and \item \texttt{b} if \texttt{a} is less than \texttt{b}\end{itemize}
+    \item define \texttt{y} as the rec record with $\Fieldf$ value \texttt{a} and $\Fieldg$ value \texttt{b}
+    \item define \texttt{r\_f} as the sum of the field $\FIELDf$ of \texttt{r} and the field $\FIELDg$ of \texttt{r}
+    \item define \texttt{r'} as \texttt{r} with $\FIELDf$ updated to \texttt{res}
+    \item \textbf{the result is:} the pair consisting of \texttt{res} (for the output variable \texttt{c}) and \texttt{r'} (for the output variable \texttt{r'}).
   \end{itemize}
 } % EndDefineProse
diff --git a/asllib/aslspec/tests.t/run.t b/asllib/aslspec/tests.t/run.t
index 5a2f36137a..8d696e2f9c 100644
--- a/asllib/aslspec/tests.t/run.t
+++ b/asllib/aslspec/tests.t/run.t
@@ -7,27 +7,8 @@
   Generated LaTeX macros into generated_macros.tex
   $ aslspec rule.spec --render; diff -w generated_macros.tex rule.expected; rm -f generated_macros.tex
   Generated LaTeX macros into generated_macros.tex
-  82,86c82,86
-  <     \item define \texttt{res} as \begin{itemize}\item \texttt{a} if \texttt{a} is equal to \texttt{b}, \item the sum of \texttt{a} and \texttt{b} if \texttt{a} is greater than \texttt{b}, and \item \texttt{b} if \texttt{a} is less than \texttt{b}\end{itemize}
-  <     \item define \texttt{y} as the rec record with $\Fieldf$ value \texttt{a} and $\Fieldg$ value \texttt{b}
-  <     \item define \texttt{r\_f} as the sum of the field $\FIELDf$ of \texttt{r} and the field $\FIELDg$ of \texttt{r}
-  <     \item define \texttt{r'} as \texttt{r} with $\FIELDf$ updated to \texttt{res}
-  <     \item \textbf{the result is:} the pair consisting of \texttt{res} (for the output variable \texttt{c}) and \texttt{r'} (for the output variable \texttt{r'}).
-  ---
-  >     \item define \texttt{res} as  (1) if \texttt{a} is equal to \texttt{b} holds then \texttt{a},  (2) if \texttt{a} is greater than \texttt{b} holds then the sum of  (1) \texttt{a}, and  (2) \texttt{b}, and  (3) if \texttt{a} is less than \texttt{b} holds then \texttt{b};
-  >     \item define \texttt{y} as the rec record with $\Fieldf$ value \texttt{a} and $\Fieldg$ value \texttt{b};
-  >     \item define \texttt{r\_f} as the sum of  (1) the field $\FIELDf$ of \texttt{r}, and  (2) the field $\FIELDg$ of \texttt{r};
-  >     \item define \texttt{r'} as \texttt{r} with $\FIELDf$ updated to \texttt{res};
-  >     \item \textbf{the result is:} the pair consisting of \texttt{res} (for the output variable \texttt{c}) and \texttt{r'}.
   $ aslspec operators.spec --render; diff -w generated_macros.tex operators.expected; rm -f generated_macros.tex
   Generated LaTeX macros into generated_macros.tex
-  55,56c55,56
-  <     \item the sum of \texttt{a} and \texttt{b} is equal to \texttt{c}
-  <     \item define \texttt{d} as: if \texttt{a} is in \texttt{S} then \texttt{b} else \texttt{c}
-  ---
-  >     \item the sum of all numbers in  (1) \texttt{a}, and  (2) \texttt{b} is equal to \texttt{c};
-  >     \item define \texttt{d} as: if \texttt{a} is in \texttt{S} then \texttt{b} else \texttt{c};
-
   $ aslspec type_name.bad
   Syntax Error: illegal element-defining identifier: t2 around type_name.bad line 1 column 41
   [1]
diff --git a/asllib/aslspec/tests.t/typedefs.expected b/asllib/aslspec/tests.t/typedefs.expected
index b25b175d65..1403bde240 100644
--- a/asllib/aslspec/tests.t/typedefs.expected
+++ b/asllib/aslspec/tests.t/typedefs.expected
@@ -27,8 +27,6 @@
 % Macros for elements
 % -------------------
 
-\DefineConstant{bot}{\texthypertarget{constant-bot}$\bot$} % EndDefineConstant
-
 \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
 
 \DefineConstant{empty_set}{\texthypertarget{constant-emptyset}$\emptyset$} % EndDefineConstant
diff --git a/asllib/doc/ASLFormal.tex b/asllib/doc/ASLFormal.tex
index 561b4d28f5..aca431c8f4 100644
--- a/asllib/doc/ASLFormal.tex
+++ b/asllib/doc/ASLFormal.tex
@@ -97,7 +97,7 @@ \section{Mathematical Definitions and Notations\label{sec:Mathematical Definitio
 \hypertarget{constant-equalsign}{}
 \RenderType{Sign}
 
-The function $\sign : \overname{\Q}{\vq} \rightarrow \overname{\Sign}{\vs}$ returns the sign of $\vq$:
+The function $\sign(\overname{\Q}{\vq}) \rightarrow \overname{\Sign}{\vs}$ returns the sign of $\vq$:
 \[
 \sign(\vq) \triangleq \begin{cases}
   \positivesign & \text{if }\vq > 0\\
@@ -141,18 +141,21 @@ \section{Mathematical Definitions and Notations\label{sec:Mathematical Definitio
 \hypertarget{def-graphtransitive}{}
 \hypertarget{def-graphtransitivereflexive}{}
 \begin{definition}[Transitive Closure of a Relation]
-We denote the transitive closure of a relation $E = V \cartimes V$ by $\graphtransitive{E}$
+We denote the transitive closure of a relation $E \subseteq V \cartimes V$ by $\graphtransitive{E}$
 and the reflexive-transitive closure of $E$ by $\graphtransitivereflexive{E}$.
 \end{definition}
 
-\begin{definition}[Bottom Value]
-We use the symbol \RenderConstant{bot} to denote an undefined, or missing, value.
-\end{definition}
+\paragraph{Function and Relation Notations}
+We use a non-standard notation for functions and relations, which is more succinct.
+Specifically, we write $f(T_1,\ldots,T_n) \rightarrow R$ to denote a function from
+the argument types $T_1,\ldots,T_n$ to the result type $R$.
+%
+We write $f(T_1,\ldots,T_n) \aslrel{} R$ to denote a relation between the argument types $T_1,\ldots,T_n$ and the result type $R$.
 
 \hypertarget{def-partialfunc}{}
 \hypertarget{def-dom}{}
 \begin{definition}[Partial Function\label{def:PartialFunction}]
-  A \emph{partial function}, denoted $f : A \partialto B$, is a function from a \underline{subset} of $A$ to $B$.
+  A \emph{partial function}, denoted $f(A) \partialto B$, is a function from a \underline{subset} of $A$ to $B$.
   The \emph{domain} of a partial function $f$, denoted $\dom(f)$, is the subset of $A$ for which it is defined.
   We use expressions like $x \in \dom(f)$ and $x \not\in \dom(f)$ to check whether $x$ is in the domain of $f$
   or not in the domain of $f$, respectively.
@@ -195,7 +198,7 @@ \section{Mathematical Definitions and Notations\label{sec:Mathematical Definitio
 
 \begin{definition}[Function Restriction]
 \hypertarget{def-restrictfunc}{}
-The \emph{restriction} of a function $f : X \rightarrow Y$ to a subset of its domain
+The \emph{restriction} of a function $f(X) \rightarrow Y$ to a subset of its domain
 $A \subseteq \dom(f)$, denoted as $\restrictfunc{f}{A}$, is defined
 in terms of the set of input-output pairs:
 \[
@@ -210,7 +213,7 @@ \section{Mathematical Definitions and Notations\label{sec:Mathematical Definitio
 the expressions corresponding to the arguments.
 For example,
 \[
-\sign : \overname{\Q}{\vq} \rightarrow \overname{\Sign}{\vs}
+\sign(\overname{\Q}{\vq}) \rightarrow \overname{\Sign}{\vs}
 \]
 defines a function type and lets us refer to its argument as $\vq$
 and to the result as $\vs$.
@@ -286,7 +289,7 @@ \subsection{Lists}
 
 \hypertarget{relation-concat}{}
 \begin{definition}[List Concatenation]
-The parametric function $\concat : \KleeneStar{T} \cartimes \KleeneStar{T} \rightarrow \KleeneStar{T}$ concatenates two lists:
+The parametric function $\concat(\KleeneStar{T}, \KleeneStar{T}) \rightarrow \KleeneStar{T}$ concatenates two lists:
 \[
   L \concat{} M \triangleq
   \begin{cases}
@@ -322,7 +325,7 @@ \subsection{Lists}
 \begin{definition}[Equating List Lengths]
 The parametric function
 \[
-  \equallength : \overname{\KleeneStar{A}}{a} \cartimes \overname{\KleeneStar{B}}{b} \rightarrow \Bool
+  \equallength(\overname{\KleeneStar{A}}{a}, \overname{\KleeneStar{B}}{b}) \rightarrow \Bool
 \]
 compares the length of two lists:
 \[
@@ -332,7 +335,7 @@ \subsection{Lists}
 
 \hypertarget{def-listprefix}{}
 \begin{definition}[List Prefix]
-The parametric function $\listprefixname : \overname{\KleeneStar{T}}{\vlone} \cartimes \overname{\KleeneStar{T}}{\vltwo} \rightarrow \Bool$ checks whether
+The parametric function $\listprefixname(\overname{\KleeneStar{T}}{\vlone}, \overname{\KleeneStar{T}}{\vltwo}) \rightarrow \Bool$ checks whether
 the list $\vlone$ is a \emph{prefix} of the list $\vltwo$:
 \[
 \listprefixname(\vlone, \vltwo) \triangleq \exists \vlthree.\ \vltwo = \vlone \concat \vlthree \enspace.
@@ -341,7 +344,7 @@ \subsection{Lists}
 
 \hypertarget{def-listrange}{}
 \begin{definition}[Indices of a List]
-The parametric function $\listrange : \KleeneStar{T} \rightarrow \KleeneStar{\N}$ returns the ($1$-based) list of indices for a given list:
+The parametric function $\listrange(\KleeneStar{T}) \rightarrow \KleeneStar{\N}$ returns the ($1$-based) list of indices for a given list:
 \[
     \begin{array}{rcl}
         \listrange(\emptylist) &\triangleq& \emptylist\\
@@ -370,7 +373,7 @@ \subsection{Lists}
 \begin{definition}[Extracting the First Components from a List of Pairs]
 The\\ parametric function
 \[
-\listfstname : \KleeneStar{(T_1 \cartimes T_2)} \rightarrow \KleeneStar{T_1}
+\listfstname(\KleeneStar{(T_1 \cartimes T_2)}) \rightarrow \KleeneStar{T_1}
 \]
 transforms a list of pairs into a lists of elements containing the first components of each pair:
 \[
@@ -385,7 +388,7 @@ \subsection{Lists}
 \begin{definition}[Unzipping a List of Pairs]
 The parametric function
 \[
-\unziplist : \KleeneStar{(T_1 \cartimes T_2)} \rightarrow (\KleeneStar{T_1} \cartimes \KleeneStar{T_2})
+\unziplist(\KleeneStar{(T_1 \cartimes T_2)}) \rightarrow (\KleeneStar{T_1} \cartimes \KleeneStar{T_2})
 \]
 transforms a list of pairs into the corresponding pair of lists:
 \[
@@ -402,7 +405,7 @@ \subsection{Lists}
 \begin{definition}[Unzipping a List of Triples]
 The parametric function
 \[
-\unziplistthree : \KleeneStar{(T_1 \cartimes T_2 \cartimes T_3)} \rightarrow (\KleeneStar{T_1} \cartimes \KleeneStar{T_2} \cartimes \KleeneStar{T_3})
+\unziplistthree(\KleeneStar{(T_1 \cartimes T_2 \cartimes T_3)}) \rightarrow (\KleeneStar{T_1} \cartimes \KleeneStar{T_2} \cartimes \KleeneStar{T_3})
 \]
 transforms a list of triples into the corresponding triple of lists:
 \[
@@ -419,7 +422,7 @@ \subsection{Lists}
 \texthypertarget{relation-listcross}
 The parametric function
 \[
-\listcrossop : \KleeneStar{T_1} \cartimes \KleeneStar{T_2} \aslto \KleeneStar{(T_1 \cartimes T_2)}
+\listcrossop(\KleeneStar{T_1}, \KleeneStar{T_2}) \rightarrow \KleeneStar{(T_1 \cartimes T_2)}
 \]
 computes the cross-product of two lists:
 \[
@@ -445,7 +448,7 @@ \subsection{Lists}
 The parametric function
 \hypertarget{def-unionlist}{}
 \[
-\unionlist : \KleeneStar{\pow{T}} \rightarrow \pow{T}
+\unionlist(\KleeneStar{\pow{T}}) \rightarrow \pow{T}
 \]
 takes the union of a list of sets:
 \[
@@ -457,7 +460,7 @@ \subsection{Lists}
 The parametric function
 \hypertarget{def-intersectionlist}{}
 \[
-\intersectionlist : \KleeneStar{\pow{T}} \rightarrow \pow{T}
+\intersectionlist(\KleeneStar{\pow{T}}) \rightarrow \pow{T}
 \]
 takes the intersection of a list of sets:
 \[
@@ -470,13 +473,13 @@ \subsection{Lists}
 
 \subsection{Strings}
 \hypertarget{relation-stringconcat}{}
-The function $\concatstrings : \Strings \cartimes \Strings \rightarrow \Strings$
+The function $\concatstrings(\Strings, \Strings) \rightarrow \Strings$
 concatenates two strings. %
 We slightly abuse notation by using the same symbol $\concat$ for concatenating
 a string $S$ and an integer $n$, separated by a hyphen, for example, \verb|return-42|.
 
 \hypertarget{relation-stringofint}{}
-The function $\stringofintname : \Z \rightarrow \Strings$ converts an integer number
+The function $\stringofintname(\Z) \rightarrow \Strings$ converts an integer number
 to the corresponding decimal string.
 
 \subsection{OCaml-style Notations}
@@ -1110,10 +1113,10 @@ \subsection{Judgments Over Optional Data Types}
 Optional data types are prevalent in the AST.
 To facilitate transition judgments over optional data types,
 we introduce the following parametric relation,
-which accepts a one-argument relation (or function) $f : A \aslrel B$
+which accepts a one-argument relation (or function) $f(A) \aslrel B$
 and applies it to an optional value:
 \[
-\mapopt{\cdot} : \overname{\Option{A}}{\vvopt} \aslrel \overname{\Option{B}}{\vvoptnew}
+\mapopt{\cdot}(\overname{\Option{A}}{\vvopt}) \aslrel \overname{\Option{B}}{\vvoptnew}
 \]
 
 \ProseParagraph
diff --git a/asllib/doc/ASLmacros.tex b/asllib/doc/ASLmacros.tex
index bcb0a15fde..411e2c7514 100644
--- a/asllib/doc/ASLmacros.tex
+++ b/asllib/doc/ASLmacros.tex
@@ -266,8 +266,6 @@
 \let\OldTriangleq\triangleq
 \let\OldEmptyset\emptyset
 \renewcommand\emptyset[0]{\hyperlink{constant-emptyset}{\OldEmptyset}}
-\let\OldBot\bot
-\renewcommand\bot[0]{\hyperlink{constant-bot}{\OldBot}}
 \renewcommand\triangleq[0]{\hyperlink{def-triangleq}{\OldTriangleq}}
 \newcommand\cartimes[0]{\hyperlink{def-cartimes}{\times}}
 
@@ -1112,6 +1110,7 @@
 \newcommand\aslscan[0]{\hyperlink{def-aslscan}{\textfunc{scan}}} % NO_SPECIFICATION_REQUIRED
 \newcommand\Proseaslscan[3]{\hyperlink{def-aslscan}{applying lexical analysis} to #1 with the lexical specification #2 yields the list of tokens #3}
 \newcommand\maxmatches[0]{\hyperlink{def-maxmatch}{\textfunc{max\_matches}}} % NO_SPECIFICATION_REQUIRED
+\newcommand\nomatch[0]{\hyperlink{def-nomatch}{\textfunc{no\_match}}} % NO_SPECIFICATION_REQUIRED
 \newcommand\remaxmatch[0]{\hyperlink{def-rematch}{\textfunc{re\_max\_match}}} % NO_SPECIFICATION_REQUIRED
 \newcommand\Token[0]{\hyperlink{def-token}{\mathbb{T}\mathbb{O}\mathbb{K}\mathbb{E}\mathbb{N}}}
 \newcommand\discard[0]{\hyperlink{def-discard}{\textfunc{discard}}} % NO_SPECIFICATION_REQUIRED
diff --git a/asllib/doc/AbstractSyntax.tex b/asllib/doc/AbstractSyntax.tex
index 38b958892e..26e6e696cd 100644
--- a/asllib/doc/AbstractSyntax.tex
+++ b/asllib/doc/AbstractSyntax.tex
@@ -442,7 +442,7 @@ \section{Building Parameterized Productions\label{sec:BuildingParameterizedProdu
 \[
 \buildlist[b](\overname{N}{\vsyms}) \;\aslrel\; \overname{A}{\vsymasts}
 \]
-which is parameterized by an AST building relation $b : E \aslrel A$,
+which is parameterized by an AST building relation $b(E) \aslrel A$,
 takes a parse node that represents a possibly-empty list of $E$ values --- $\vsyms$ --- and returns the result of applying $b$
 to each of them --- $\vsymasts$.
 
@@ -470,7 +470,7 @@ \section{Building Parameterized Productions\label{sec:BuildingParameterizedProdu
 \[
 \buildclist[b](\overname{N}{\vsyms}) \;\aslrel\; \overname{A}{\vsymasts}
 \]
-which is parameterized by an AST building relation $b : E \aslrel A$,
+which is parameterized by an AST building relation $b(E) \aslrel A$,
 takes a parse node that represents a possibly-empty comma-separated list of $E$ values --- $\vsyms$ --- and returns the result of applying $b$
 to each of them --- $\vsymasts$.
 
@@ -497,7 +497,7 @@ \section{Building Parameterized Productions\label{sec:BuildingParameterizedProdu
 \[
 \buildplist[b](\overname{N}{\vsyms}) \;\aslrel\; \overname{A}{\vsymasts}
 \]
-which is parameterized by an AST building relation $b : E \aslrel A$,
+which is parameterized by an AST building relation $b(E) \aslrel A$,
 takes a parse node that represents a parenthesized comma-separated list of $E$ values --- $\vsyms$ --- and returns the result of applying $b$
 to each of them --- $\vsymasts$.
 
@@ -515,7 +515,7 @@ \section{Building Parameterized Productions\label{sec:BuildingParameterizedProdu
 \[
 \buildtclist[b](\overname{N}{\vsyms}) \;\aslrel\; \overname{A}{\vsymasts}
 \]
-which is parameterized by an AST building relation $b : E \aslrel A$,
+which is parameterized by an AST building relation $b(E) \aslrel A$,
 takes a parse node that represents a non-empty comma-separated trailing list of $E$ values --- $\vsyms$ --- and returns the result of applying $b$
 to each of them --- $\vsymasts$.
 
@@ -542,7 +542,7 @@ \section{Building Parameterized Productions\label{sec:BuildingParameterizedProdu
 \[
 \buildoption[b](\overname{N}{\vsym}) \;\aslrel\; \overname{\Option{A}}{\vsymast}
 \]
-which is parameterized by an AST building relation $b : N \aslrel A$,
+which is parameterized by an AST building relation $b(N) \aslrel A$,
 takes a parse node that represents an optional $N$ value $\vsym$, and returns the result of applying $b$
 to the value if it exists --- $\vsymasts$.
 
diff --git a/asllib/doc/AssignableExpressions.tex b/asllib/doc/AssignableExpressions.tex
index 99f5793ae2..b3e32d8701 100644
--- a/asllib/doc/AssignableExpressions.tex
+++ b/asllib/doc/AssignableExpressions.tex
@@ -49,7 +49,7 @@ \chapter{Assignable Expressions\label{chap:AssignableExpressions}}
 \paragraph{Viewing Assignable Expressions as Right-hand-side Expressions:}
 Some of the typing rules and semantics rules require viewing \assignableexpressions\
 as \rhsexpressions.
-The correspondence is given by the function $\torexpr : \lexpr \rightarrow \expr$, defined in \secref{LeftToRight}.
+The correspondence is given by the function $\torexpr(\lexpr) \rightarrow \expr$, defined in \secref{LeftToRight}.
 %
 For example, \SemanticsRuleRef{LESetField}
 needs to evaluate the record subexpression $\rerecord$, which is an \assignableexpression.
diff --git a/asllib/doc/LexicalStructure.tex b/asllib/doc/LexicalStructure.tex
index 9c8e3f36e2..90d5949e12 100644
--- a/asllib/doc/LexicalStructure.tex
+++ b/asllib/doc/LexicalStructure.tex
@@ -332,7 +332,7 @@ \section{Lexical Analysis\label{sec:LexicalAnalysis}}
 Lexical analysis, which is also referred to as \emph{scanning}, is defined via the function
 \hypertarget{def-aslscan}{}
 \[
-\aslscan : \LexSpec \cartimes \KleeneStar{\REasciichar} \aslto (\KleeneStar{\Token} \cup \{\LexicalErrorConfig\})
+\aslscan(\LexSpec, \KleeneStar{\REasciichar}) \aslto (\KleeneStar{\Token} \cup \{\LexicalErrorConfig\})
 \]
 \hypertarget{def-lexicalerrorresult}{}
 which takes a \emph{lexical specification} (explained soon), an ASL specification string
@@ -393,23 +393,24 @@ \section{Lexical Analysis\label{sec:LexicalAnalysis}}
 \begin{definition}[Lexical Specification]
 A \emph{lexical specification} consists of a list of pairs $[(r_1,a_1),\ldots,(r_k,a_k)] \in \LexSpec$
 where each pair $(r_i,a_i)$ consists of a lexical regular expression $r_i$
-and a \emph{lexeme action} $a_i : \Strings\cartimes\Strings \aslto \KleeneStar{\Token}$.
+and a \emph{lexeme action} $a_i(\Strings, \Strings) \aslto \KleeneStar{\Token}$.
 \end{definition}
 
 \hypertarget{def-rematch}{}
 The function
 \[
-\remaxmatch : \overname{\RegExp}{e} \cartimes \overname{\Strings}{s} \aslto (\overname{\Strings}{s_1} \cartimes \overname{\Strings}{s_2}) \cup \{\bot\}
+\remaxmatch(\overname{\RegExp}{e}, \overname{\Strings}{s}) \aslto (\overname{\Strings}{s_1} \cartimes \overname{\Strings}{s_2}) \cup \{\nomatch\}
 \]
 returns the \emph{longest} match of a regular expression $e$ for a prefix of a string $s$.
 More precisely:
 $\remaxmatch(e, s) = (s_1,s_2)$ means that $s_1\in\Lang{e}$ and $s = s_1 \concat s_2$.
-If no match exists, it is indicated by returning $\bot$.
+\texthypertarget{def-nomatch}
+If no match exists, it is indicated by returning $\nomatch$.
 
 \hypertarget{def-maxmatch}{}
-The function $\maxmatches : \overname{\LexSpec}{R} \cartimes \overname{\Strings}{s} \aslto \overname{\LexSpec}{R'}$
+The function $\maxmatches(\overname{\LexSpec}{R}, \overname{\Strings}{s}) \aslto \overname{\LexSpec}{R'}$
 returns the sublist of $R$ consisting of pairs whose maximal matches for $s$ are equal. Importantly, the result sublist $R'$ maintains
-the order of pairs in $R$. If all expressions in $R$ do not match (that is $\remaxmatch$ returns $\bot$ for all pairs in $R$), then $R'$ is the empty list.
+the order of pairs in $R$. If all expressions in $R$ do not match (that is $\remaxmatch$ returns $\nomatch$ for all pairs in $R$), then $R'$ is the empty list.
 
 The function $\aslscan$ is constructively defined via the following inference rules:
 
@@ -673,7 +674,7 @@ \subsection{Scanning Strings}
 To scan string literals, we define the following specialized scanning function.
 The function
 \[
-\scanstring : \overname{\KleeneStar{\REasciichar}}{\buff} \cartimes \overname{\KleeneStar{\REasciichar}}{s} \aslto (\KleeneStar{\Token} \cup \{\LexicalErrorConfig\})
+\scanstring(\overname{\KleeneStar{\REasciichar}}{\buff}, \overname{\KleeneStar{\REasciichar}}{s}) \aslto (\KleeneStar{\Token} \cup \{\LexicalErrorConfig\})
 \]
 scans string with the $\specstring$ specification while building the final string literal in $\buff$.
 It is defined via the following rules:
diff --git a/asllib/doc/RelationsOnTypes.tex b/asllib/doc/RelationsOnTypes.tex
index a4dd47d8fa..e338a5eb8d 100644
--- a/asllib/doc/RelationsOnTypes.tex
+++ b/asllib/doc/RelationsOnTypes.tex
@@ -229,7 +229,7 @@ \section{Relations Over Types\label{sec:RelationsOnTypes}}
   \supers(\tenv, \vt) \triangleq
   \begin{cases}
     \{\vt\} \cup \supers(\vs) & \text{ if }\tenv.\staticenvsG.\subtypes(\vt) = \vs\\
-    \{\vt\}  & \text{ otherwise } (\text{that is, }\tenv.\staticenvsG.\subtypes(\vt) = \bot)\\
+    \{\vt\}  & \text{ otherwise } (\text{that is, }\vt \not\in\dom(\tenv.\staticenvsG.\subtypes))\\
   \end{cases}
 \]
 
diff --git a/asllib/doc/Specifications.tex b/asllib/doc/Specifications.tex
index 44df78b3f1..744d8c3269 100644
--- a/asllib/doc/Specifications.tex
+++ b/asllib/doc/Specifications.tex
@@ -51,7 +51,7 @@ \section{Formal Relations for Global Declarations\label{sec:Formal Relations for
 Global declarations are generated by the relation
 \hypertarget{build-decl}{}
 \[
-  \builddecl : \overname{\parsenode{\Ndecl}}{\vparsednode} \;\aslrel\; \overname{\KleeneStar{\decl}}{\vastnode}
+  \builddecl(\overname{\parsenode{\Ndecl}}{\vparsednode}) \;\aslrel\; \overname{\KleeneStar{\decl}}{\vastnode}
 \]
 transforms a parse node $\vparsednode$ into an AST node $\vastnode$.
 
@@ -99,12 +99,11 @@ \section{Abstract Syntax of Specifications\label{sec:Abstract Syntax of Specific
 \hypertarget{build-ast}{}
 The relation
 \[
-  \buildast : \overname{\parsenode{\Nspec}}{\vparsednode} \;\aslrel\; \overname{\spec}{\vastnode}
+  \buildast(\overname{\parsenode{\Nspec}}{\vparsednode}) \;\aslrel\; \overname{\spec}{\vastnode}
 \]
 transforms an $\Nspec$ node $\vparsednode$ into an AST specification node $\vastnode$.
 } % END_OF_UNIMPORTED_RELATION
 
-
 We define this function for subprogram declarations, type declarations, and global storage declarations in the corresponding chapters.
 
 \begin{mathpar}
diff --git a/asllib/doc/SubprogramDeclarations.tex b/asllib/doc/SubprogramDeclarations.tex
index 2e72cc7cc5..162984df8b 100644
--- a/asllib/doc/SubprogramDeclarations.tex
+++ b/asllib/doc/SubprogramDeclarations.tex
@@ -212,7 +212,7 @@ \section{Accessors\label{sec:Accessors}}
 \hypertarget{build-accessorbody}{}
 The relation
 \[
-  \buildaccessorbody : \overname{\parsenode{\Naccessorbody}}{\vparsednode} \;\aslrel\; \overname{\accessorpair}{\vaccessorpair}
+  \buildaccessorbody(\overname{\parsenode{\Naccessorbody}}{\vparsednode}) \;\aslrel\; \overname{\accessorpair}{\vaccessorpair}
 \]
 transforms a parse node $\vparsednode$ into an $\accessorpair$.
 } % END_OF_UNIMPORTED_RELATION
@@ -1010,7 +1010,7 @@ \section{Accessors\label{sec:Accessors}}
 In this case, there is no ordering between these two subprograms.
 Assuming $I$ is processed before $R$, adding $I$ to the
 \staticenvironmentterm{}, the \staticenvironmentterm{} has
-$\overloadedsubprograms(\addten) = \bot$
+$\addten \not\in \dom(\overloadedsubprograms)$
 and is then updated by binding $\addten$ to $\{\addten\}$ in $\overloadedsubprograms$.
 Then, processing $R$, results in
 binding $\addten$ to
diff --git a/asllib/doc/SymbolicEquivalenceTesting.tex b/asllib/doc/SymbolicEquivalenceTesting.tex
index d512ae131c..1aeb22411a 100644
--- a/asllib/doc/SymbolicEquivalenceTesting.tex
+++ b/asllib/doc/SymbolicEquivalenceTesting.tex
@@ -171,7 +171,6 @@ \section{Symbolic Expressions\label{sec:symbolicexpressions}}
     \begin{array}{ll}
       \vfone(\vm) & \text{if } \vm \in \dom(\vfone) \setminus \dom(\vftwo)\\
       \vftwo(\vm) & \text{if } \vm \in \dom(\vftwo) \setminus \dom(\vfone)\\
-      \bot        & \text{if } \vm \in \dom(\vfone) \cap \dom(\vftwo) \text{ and } \vfone(\vm)+\vftwo(\vm) = 0\\
       \vfone(\vm)+\vftwo(\vm) & \text{if } \vm \in \dom(\vfone) \cap \dom(\vftwo) \text{ and } \vfone(\vm)+\vftwo(\vm) \neq 0\\
     \end{array}
     \right.
@@ -181,11 +180,15 @@ \section{Symbolic Expressions\label{sec:symbolicexpressions}}
   \addpolynomials(\overname{\vfone}{\vpone}, \overname{\vftwo}{\vptwo}) \typearrow \overname{\vf}{\vp}
 }
 \end{mathpar}
+Notice that if $\vfone$ and $\vftwo$ map the same monomial $\vm$ to factors that sum to zero
+(that is, $\vm \in \dom(\vfone) \cap \dom(\vftwo)$ and $\vfone(\vm) + \vftwo(\vm) = 0$),
+then $\vf$ does not map $\vm$ to any factor, which corresponds to the fact that the monomial
+$\vm$ does not appear in the resulting polynomial.
 
 \TypingRuleDef{AddPolynomialList}
 The overloaded function
 \[
-  \addpolynomials : \KleeneStar{\polynomial} \rightarrow \polynomial
+  \addpolynomials(\KleeneStar{\polynomial}) \rightarrow \polynomial
 \]
 adds a list of polynomials.
 
diff --git a/asllib/doc/Syntax.tex b/asllib/doc/Syntax.tex
index 71b8eda498..1140a576c0 100644
--- a/asllib/doc/Syntax.tex
+++ b/asllib/doc/Syntax.tex
@@ -704,7 +704,7 @@ \section{Parse Trees\label{sec:ParseTrees}}
 \hypertarget{def-aslparse}{}
 A parser is a function
 \[
-\aslparse : (\KleeneStar{\Token} \setminus \{\Terror\}) \aslto \parsenode{\Nspec} \cup \{\ParseErrorConfig\}
+\aslparse(\KleeneStar{\Token} \setminus \{\Terror\}) \aslto \parsenode{\Nspec} \cup \{\ParseErrorConfig\}
 \]
 \hypertarget{def-parseerror}{}
 where $\ParseErrorConfig$ stands for a \emph{parse error}.
diff --git a/asllib/doc/TypeDomains.tex b/asllib/doc/TypeDomains.tex
index c35a69a2c6..7e0f27cf17 100644
--- a/asllib/doc/TypeDomains.tex
+++ b/asllib/doc/TypeDomains.tex
@@ -54,7 +54,7 @@ \subsection{The Dynamic Domain of a Type\label{sec:DynDomain}}
 As part of the definition, we also associate dynamic domains to integer constraints
 by overloading $\dynamicdomain$:
 \[
-  \dynamicdomain : \overname{\envs}{\env} \cartimes \overname{\intconstraint}{\vc}
+  \dynamicdomain(\overname{\envs}{\env}, \overname{\intconstraint}{\vc})
   \partialto \overname{\pow{\nativevalue}}{\vd}
 \]
 
@@ -441,5 +441,3 @@ \subsection{The Dynamic Domain of a Type\label{sec:DynDomain}}
 the native integer value $c$,
 which is assigned to \texttt{N} by a given dynamic environment. The static domain of that parameter
 is the infinite set of all native integer values.
-
-
diff --git a/asllib/doc/TypeSystemUtilities.tex b/asllib/doc/TypeSystemUtilities.tex
index 00e93fa7cb..41bcd1ab71 100644
--- a/asllib/doc/TypeSystemUtilities.tex
+++ b/asllib/doc/TypeSystemUtilities.tex
@@ -96,7 +96,7 @@ \chapter{Type System Utility Rules\label{chap:TypeSystemUtilityRules}}
 \hva\and
 \inferrule[two\_or\_more]{
   \listlen{\vlone} = n\\
-  f : 1..n \rightarrow 1..n \text{ is a bijection}\\
+  f(1..n) \rightarrow 1..n \text{ is a bijection}\\
   \vltwo \eqdef [\ i=1..n: \vlone[f(i)]\ ]\\
   i=1..n-1: \compare(\vltwo[i], \vltwo[i+1]) \geq 0
 }{
diff --git a/asllib/doc/reference-review-worklist.md b/asllib/doc/reference-review-worklist.md
new file mode 100644
index 0000000000..85bd859950
--- /dev/null
+++ b/asllib/doc/reference-review-worklist.md
@@ -0,0 +1,60 @@
+# ASL Reference Review Worklist
+
+Source order: [ASLReference.tex](/Users/romman01/arm/herdtools7-master/asllib/doc/ASLReference.tex)
+
+Status legend: `pending`, `in_progress`, `blocked`, `done`
+
+| # | File | Status | Notes |
+|---|------|--------|-------|
+| 1 | `notice.tex` | done | Skipped per user instruction. |
+| 2 | `disclaimer.tex` | done | Skipped per user instruction. |
+| 3 | `introduction.tex` | done | No blocking issue found before reaching `ASLFormal.tex`. |
+| 4 | `ASLFormal.tex` | blocked | Verified fix for transitive closure. New issue: `Listing a Set` gives malformed relation signature `\\listset{\\pow{T}} \\cartimes \\KleeneStar{T}`; it needs an explicit symbol/type form, likely a function signature. |
+| 5 | `LexicalStructure.tex` | pending | |
+| 6 | `Syntax.tex` | pending | |
+| 7 | `AbstractSyntax.tex` | pending | |
+| 8 | `TypeChecking.tex` | pending | |
+| 9 | `Semantics.tex` | pending | |
+| 10 | `Literals.tex` | pending | |
+| 11 | `PrimitiveOperations.tex` | pending | |
+| 12 | `Types.tex` | pending | |
+| 13 | `Slicing.tex` | pending | |
+| 14 | `Bitfields.tex` | pending | |
+| 15 | `Expressions.tex` | pending | |
+| 16 | `PatternMatching.tex` | pending | |
+| 17 | `AssignableExpressions.tex` | pending | |
+| 18 | `LocalStorageDeclarations.tex` | pending | |
+| 19 | `Statements.tex` | pending | |
+| 20 | `BlockStatements.tex` | pending | |
+| 21 | `CatchingExceptions.tex` | pending | |
+| 22 | `SubprogramCalls.tex` | pending | |
+| 23 | `GlobalStorageDeclarations.tex` | pending | |
+| 24 | `TypeDeclarations.tex` | pending | |
+| 25 | `SubprogramDeclarations.tex` | pending | |
+| 26 | `GlobalPragmas.tex` | pending | |
+| 27 | `Specifications.tex` | pending | |
+| 28 | `TopLevel.tex` | pending | |
+| 29 | `SideEffects.tex` | pending | |
+| 30 | `StaticEvaluation.tex` | pending | |
+| 31 | `SymbolicSubsumptionTesting.tex` | pending | |
+| 32 | `SymbolicEquivalenceTesting.tex` | pending | |
+| 33 | `TypeSystemUtilities.tex` | pending | |
+| 34 | `SemanticsUtilities.tex` | pending | |
+| 35 | `RuntimeEnvironment.tex` | pending | |
+| 36 | `ErrorCodes.tex` | pending | |
+| 37 | `StandardLibrary.tex` | pending | |
+
+## Learnings
+
+- Render order is driven by [ASLReference.tex](/Users/romman01/arm/herdtools7-master/asllib/doc/ASLReference.tex).
+- `generated_macros.tex` is included in the preamble but is not part of the rendered chapter/section worklist.
+- `notice.tex` and `disclaimer.tex` are out of scope for the review.
+- When a `\Render...` macro appears in a `.tex` file, review it against the corresponding definition in [asl.spec](/Users/romman01/arm/herdtools7-master/asllib/doc/asl.spec). If the mapping is unclear, ask the user before proceeding.
+- Fixed: [ASLFormal.tex](/Users/romman01/arm/herdtools7-master/asllib/doc/ASLFormal.tex) now states transitive closure over `E \\subseteq V \\cartimes V`.
+- New blocking issue in [ASLFormal.tex](/Users/romman01/arm/herdtools7-master/asllib/doc/ASLFormal.tex): `Listing a Set` uses a malformed signature expression instead of an explicit function/relation signature.
+
+## Current Review State
+
+- Current file: `ASLFormal.tex`
+- Current status: `blocked`
+- Waiting on user fix: repair the `Listing a Set` signature around the definition of `\\listset`, likely to something like `\\listset : \\pow{T} \\rightarrow \\KleeneStar{T}`