[asl reference] establish consistent function/relation notations

Author: Roman-Manevich

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\\
@@ -145,10 +145,17 @@ \section{Mathematical Definitions and Notations\label{sec:Mathematical Definitio
 and the reflexive-transitive closure of $E$ by $\graphtransitivereflexive{E}$.
 \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.
@@ -191,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:
 \[
@@ -206,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$.
@@ -282,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}
@@ -318,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:
 \[
@@ -328,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.
@@ -337,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\\
@@ -366,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:
 \[
@@ -381,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:
 \[
@@ -398,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:
 \[
@@ -415,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:
 \[
@@ -441,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:
 \[
@@ -453,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:
 \[
@@ -466,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}
@@ -1106,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

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$.
 

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.

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,13 +393,13 @@ \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 \{\nomatch\}
+\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:
@@ -408,7 +408,7 @@ \section{Lexical Analysis\label{sec:LexicalAnalysis}}
 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 $\nomatch$ for all pairs in $R$), then $R'$ is the empty list.
 
@@ -674,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:

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}

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

asllib/doc/SymbolicEquivalenceTesting.tex

@@ -188,7 +188,7 @@ \section{Symbolic Expressions\label{sec:symbolicexpressions}}
 \TypingRuleDef{AddPolynomialList}
 The overloaded function
 \[
-  \addpolynomials : \KleeneStar{\polynomial} \rightarrow \polynomial
+  \addpolynomials(\KleeneStar{\polynomial}) \rightarrow \polynomial
 \]
 adds a list of polynomials.
 

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}.

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.
-
-

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
 }{