From 6c808bdf4e8b60d8a5a46566995ecc54737ed443 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 14 Sep 2021 15:00:15 -0500
Subject: [PATCH 01/17] Minor fix

---
 language/sygus.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/language/sygus.tex b/language/sygus.tex
index 462d0af..53bac85 100644
--- a/language/sygus.tex
+++ b/language/sygus.tex
@@ -1134,7 +1134,7 @@ \subsection{Asserting Synthesis Constraints and Assumptions}%
 
 This command adds $t$ to the set of assumptions.
 Like constraints,
-this command is well formed if $t$ is a well-sorted term of sort $\sbool$.
+this command is well formed if $t$ is a well-sorted term of sort $\sbool$,
 and is allowed based on the restrictions of the current logic.
 
 \item $\paren{\constraintinvkwd\mbox{ }S\mbox{ }S_{pre}\mbox{ }S_{trans}\mbox{ }S_{post}}$

From b5b32e40de160d307331bedb6e59958d33a00596 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 5 Oct 2021 09:06:56 -0500
Subject: [PATCH 02/17] More

---
 tableTheory/macros.tex      |   3 +
 tableTheory/tableTheory.tex | 207 +++++++++++++++++++++++-------------
 2 files changed, 137 insertions(+), 73 deletions(-)

diff --git a/tableTheory/macros.tex b/tableTheory/macros.tex
index f967235..f114632 100644
--- a/tableTheory/macros.tex
+++ b/tableTheory/macros.tex
@@ -143,3 +143,6 @@
 
 
 \global\long\def\paren#1{{\tt (}#1{\tt )}}
+
+\global\long\def\abstype#1{?#1}
+\global\long\def\abstypebase{?}
diff --git a/tableTheory/tableTheory.tex b/tableTheory/tableTheory.tex
index 01832ca..9c3445d 100644
--- a/tableTheory/tableTheory.tex
+++ b/tableTheory/tableTheory.tex
@@ -65,7 +65,7 @@
 
 \section{Theory of Tables}
 
-This document describes a SMT-LIB theory of tables $\thtable$.
+This document describes an SMT-LIB theory of tables $\thtable$.
 We provide its signature $\sigtable$ in two parts,
 first describing its sorts and then its function symbols.
 We assume that $\sigtable$ includes the symbols of the core theory, 
@@ -109,6 +109,8 @@ \subsection{Tuple Sorts}
 \end{align*}
 for all sorts $\syntax{T_1, ..., T_k}$.
 This sort denotes tuples taking arguments of sorts $\syntax{T_1, ..., T_k}$.
+Furthermore, the sort $\syntax{Tuple}$ (with no arguments) denotes
+the empty tuple.
 
 \subsection{Bag Sorts}
 The signature $\sigtable$ includes all sorts of the form:
@@ -124,12 +126,15 @@ \subsection{Bag Sorts}
 %The elements of a bag are unordered.
 
 \paragraph{Notes}
-A table is bag whose elements are tuples.
+A table is a bag whose elements are tuples.
 We write $\syntax{ (Table\ T_1 ...\ T_k)}$ as shorthand for 
 the sort $\syntax{ (Bag\ (Tuple\ T_1\ ...\ T_k)) }$ 
 in the remainder of the document.
-We refer to $\syntax{T_1}, \ldots, \syntax{T_k}$ as the \emph{columns} of table sort above,
+We refer to $\syntax{T_1}, \ldots, \syntax{T_k}$ as the \emph{columns} of the table sort above,
 and the elements of a given table as its \emph{rows}.
+Notice that the columns of the table are \emph{not} given explicit names.
+The sort $\syntax{Table}$ with no arguments denotes the table sort with
+no columns.
 
 \section{Function Symbols}
 
@@ -163,7 +168,7 @@ \subsection{Functions}
 where $\syntax{t}$ is a term,
 and $\syntax{x_1\ ...\ x_n}$ are bound variables.
 It has sort $\syntax{(->\ T_1\ ...\ T_n\ T)}$
-when $\syntax{t}$ has sort $\syntax{T}$.
+where $\syntax{t}$ has sort $\syntax{T}$.
 It denotes the anonymous function
 returning $t$ for input arguments $\syntax{x_1}, \ldots, \syntax{x_n}$.
 %The term 
@@ -191,20 +196,26 @@ \subsubsection{Tuple Construction}
 \end{verbatim}
 The term $\syntax{(tuple\ u_1\ ...\ u_n)}$ is
 interpreted as the tuple comprised of 
-the (ordered) list of elements $\syntax{u_1,\ ...\ u_n}$. 
+the (ordered) list of elements $\syntax{u_1,\ ...\ u_n}$.
+\paragraph{Notes}
+\begin{itemize}
+\item
+The list of arguments provided to the tuple constructor can be empty.
+The term $\syntax{tuple}$, when applied to no arguments, denotes the empty tuple,
+i.e. the tuple with zero components.
+\end{itemize}
 
 \subsubsection{Tuple Selection}
 The signature $\sigtable$ includes 
-all indexed function symbols of the form
-$\syntax{ 
-(\_\ sel\ n)
-}$
-where $\syntax{n}$ is a numeral.
-Its sort definition is
+the polymorphic function symbol $\syntax{tuple\_select}$.
+Its sort definition is parametrized on $j$ sorts:
 \begin{verbatim}
 (par (X_1 ... X_j) 
-  ((_ sel n)
-  
+  (tuple_select
+    
+    ; The index we are selecting 
+    Int
+    
     ; The tuple we are selecting from
     (Tuple X_1 ... X_j)
     
@@ -213,23 +224,39 @@ \subsubsection{Tuple Selection}
   )
 )
 \end{verbatim}
-where $1 \leq \syntax{n} \leq \syntax{j}$.
-The term $\syntax{((\_\ sel\ n)\ t)}$ is
+When $1 \leq n \leq j$,
+the term $\syntax{(tuple\_select\ n\ t)}$ is
 interpreted as the $\syntax{n}^{th}$ argument of the tuple $\syntax{t}$.
+When $n$ is out of bounds, e.g. $1 \leq n \leq j$ does not hold,
+then the value of $\syntax{(tuple\_select\ n\ t)}$ is unspecified.
+
+\paragraph{Notes}
+\begin{itemize}
+\item Like other operators with partially specified semantics,
+the symbol $\syntax{tuple\_select}$ behaves like a function, meaning
+that $\syntax{(tuple\_select\ n_1\ t_1)}$ and  $\syntax{(tuple\_select\ n_2\ t_2)}$
+must have the same value when $n_1, t_1$ pairwise have the same value as $n_2, t_2$,
+even when $n_1$ and $n_2$ are out of bounds.
+\item When $n$ is a numeral, the indexed function
+$\syntax{(\_\ tuple\_select\ n)}$ is syntactic sugar for the function
+$\syntax{(tuple\_select\ n)}$, meaning that $\syntax{((\_\ tuple\_select\ n)\ t)}$
+and $\syntax{(tuple\_select\ n\ t)}$ specify the same term.
+The former may be used to make it is explicit the index to a tuple selection
+not allowed to be symbolic.
+\end{itemize}
 
 \subsubsection{Tuple Projection}
 \label{sec:tup-project}
 The signature $\sigtable$ includes 
-all indexed function symbols of the form
-$
-\syntax{ 
-(\_\ project\ n_1\ ...\ n_k)
-}$
-where $\syntax{n_1}, \ldots, \syntax{n_k}$ are numerals.
-Its sort definition is:
+the function symbol $\syntax{tuple\_project}$.
+Its sort definition includes an unbounded number of integer arguments, followed
+by a tuple:
 \begin{verbatim}
 (par (X_1 ... X_j) 
-  ((_ project n_1 ... n_k)
+  (tuple_project
+    
+    ; the components to project
+    Int ... Int
   
     ; The table to project
     (Tuple X_1 ... X_j)
@@ -239,22 +266,33 @@ \subsubsection{Tuple Projection}
   )
 )
 \end{verbatim}
-where for each $i = 1, \ldots, k$,
-$1 \leq n_i \leq j$.
 The term
-$\syntax{((\_\ project\ n_1\ ...\ n_k)\ t)}$
-returns the tuple obtained by concatenating the
+$\syntax{(tuple\_project\ n_1\ ...\ n_k\ t)}$
+returns the tuple obtained by collecting the
 values from $t$ at positions $n_1 \ldots n_k$.
-In other words, this term is equivalent to the
-term $\syntax{(tuple\ ((\_\ sel\ n_1)\ t)\ ...\ ((\_\ sel\ n_k)\ t))}$.
+In other words, this term is equivalent to:
+\begin{align*}
+\syntax{(tuple\ (tuple\_select\ n_1\ t)\ ...\ (tuple\_select\ n_k\ t))}
+\end{align*}
+Notice that if any $n_i$ in the above term is out of bounds, the value of
+that component of the returned tuple is unspecified.
+%If for each $i = 1, \ldots, k$,
+%$1 \leq n_i \leq j$,
 
 \paragraph{Notes}
 \begin{itemize}
 \item
-The function
-$\syntax{project}$ (without indices)
-denotes the operator above where $k=0$, which always returns the empty
-tuple.
+The indices $n_1, \ldots, n_k$ do not need to be ordered such that $n_1 < \ldots < n_k$.
+Moreover, it may be the case that $n_i = n_j$ for some $i \neq j$ in which
+case the component of the original is duplicated in the return value of the projection.
+\item
+The list of integer arguments to tuple projection can be empty.
+The function application
+$\syntax{(tuple\_project\ t)}$ always returns the empty tuple for any input $t$.
+\item Similar to the indexed syntax for tuple selection,
+when $n_1, \ldots, n_k$ are numerals,
+$\syntax{((\_\ tuple\_project\ n_1\ ...\ n_k)\ t)}$ is syntax sugar for the term
+$\syntax{(tuple\_project\ n_1\ ...\ n_k\ t)}$.
 \end{itemize}
 
 \subsection{Bags}
@@ -458,7 +496,7 @@ \subsubsection{Bag Fold}
 (c\ u_n\ ...\ (c\ u_2\ (c\ u_1\ i))\ ...\ )
 }
 $.
-In other words, given a start value $\syntax{b}$,
+In other words, given a start value $\syntax{i}$,
 we apply the combining function $\syntax{c}$, taking these elements
 as first arguments in order.
 
@@ -466,7 +504,7 @@ \subsubsection{Bag Fold}
 \begin{itemize}
 \item
 The semantics above impose no restrictions on the ordering $\preceq$,
-which determines in which the tuples $\syntax{u_1}, \ldots, \syntax{u_n}$
+which determines the order in which the tuples $\syntax{u_1}, \ldots, \syntax{u_n}$
 are passed to the combining function $\syntax{c}$.
 Moreover, 
 we do not provide syntax to specify such an ordering.
@@ -528,8 +566,7 @@ \subsubsection{Bag Partition}
 This ensures that a partition with the above properties
 can be computed.
 The semantics of applications of $\syntax{partition}$ for relations $\syntax{r}$
-that are not equivalence relations
-are undefined.
+that are not equivalence relations is undefined.
 \item
 If $\syntax{u}$ occurs with some multiplicity $n$ in $\syntax{t}$,
 then $\syntax{u}$ occurs with the same multiplicity $n$ in some $\syntax{t_i}$.
@@ -539,20 +576,19 @@ \subsection{Tables}
 
 \subsubsection{Table Projection}
 The signature $\sigtable$ includes 
-all indexed functions symbols of the form
-\begin{align*}
-\syntax{ 
-(\_\ project\ n_1\ ...\ n_k)
-}
-\end{align*}
-where $n_1, \ldots, n_k$ are numerals.
-Note this operator is overloaded,
-as a separate projection function (of the same name)
-is also defined for tuples in Section~\ref{sec:tup-project}.
-Its sort definition is:
+the functions symbol of the form
+$\syntax{tuple\_project}$.
+%Note this operator is overloaded,
+%as a separate projection function (of the same name)
+%is also defined for tuples in Section~\ref{sec:tup-project}.
+Its sort definition includes an unbounded number of integer arguments, followed
+by a tuple:
 \begin{verbatim}
 (par (X_1 ... X_j) 
-  ((_ project n_1 ... n_k)
+  (table_project
+  
+    ; The columns to project
+    Int ... Int
   
     ; The table to project
     (Table X_1 ... X_j)
@@ -563,41 +599,43 @@ \subsubsection{Table Projection}
 )
 \end{verbatim}
 where for each $i = 1, \ldots, j$,
-$1 \leq n_i \leq j$. 
-Note that
-$\syntax{project}$ without indices
-denotes the operator above where $k=0$.
+$1 \leq n_i \leq j$.
 
 \paragraph{Semantics}
 
-A projection operator keeps (copies) of the given columns
+A projection operator for tables keeps (copies) of the given columns
 in each (tuple) element of its argument.
 In other words,
-let $p$ be the projection operator denoted by $\syntax{(\_\ project\ n_1\ ...\ n_k)}$
-and let $t$ be a table.
-Then, $p(t)$
-is the table containing a tuple of the form
-$(u_{n_1}, \ldots, u_{n_k})$
-for each tuple $(u_1, \ldots, u_j)$ from $t$.
-
-\paragraph{Notes}
-\begin{itemize}
-\item
-The term $\syntax{((\_\ project\ n_1\ ...\ n_k)\ t)}$
+consider the term $\syntax{(table\_project\ n_1\ ...\ n_k\ t)}$
+where $t$ is a table and $n_1, \ldots, n_k$ are integers.
+%The value of this term is the table containing a tuple of the form
+%$(u_{n_1}, \ldots, u_{n_k})$
+%for each tuple $(u_1, \ldots, u_j)$ from $t$.
+%More precisely,
+%the term $\syntax{((table\_project\ n_1\ ...\ n_k\ t)}$
+This term
 can be seen as syntax sugar for $\syntax{(map\ p\ t)}$ where $\syntax{p}$
-is a function that
-applies the tuple projection on tuples $\syntax{(Tuple\ X_1\ ...\ X_j)}$
-to obtain tuples $\syntax{(Tuple\ X_{n_1}\ ...\ X_{n_k})}$:
+is the function:
 \begin{verbatim}
-(lambda ((t (Tuple X_1 ... X_j))) ((_ project n_1 ... n_k) t))
+(lambda ((u (Tuple X_1 ... X_j))) (tuple_project n_1 ... n_k u))
 \end{verbatim}
+In other words, table projection
+applies the tuple projection on all tuples in its table argument $\syntax{t}$
+to obtain tuples in the returned table.
+
+\paragraph{Notes}
+\begin{itemize}
 \item
 It may be the case that $\syntax{n_i} = \syntax{n_j}$ for some $i \neq j$,
 in which case two (or more) copies of the column at that position
 are in the result of the projection.
 \item
-The cardinality of $\syntax{((\_\ project\ n_1\ ...\ n_k)\ t)}$ is
-same as the cardinality of $\syntax{t}$.
+The cardinality of $\syntax{(table\_project\ n_1\ ...\ n_k\ t)}$ is
+the same as the cardinality of $\syntax{t}$.
+\item
+For any table $t$,
+the application taking no integer arguments $\syntax{(table\_project\ t)}$ 
+returns a table with no columns whose cardinality is the same as that of $\syntax{t}$.
 \end{itemize}
 
 \subsubsection{Table Join}
@@ -640,7 +678,7 @@ \subsubsection{Table Join}
 the predicate:
 \begin{verbatim}
 (lambda ((t_1 (Tuple X_1 ... X_j)) (t_2 (Tuple Y_1 ... Y_l)))
-  (= ((_ project n_1 ... n_k) t_1) ((_ project m_1 ... m_k) t_2))
+  (= ((_ tuple_project n_1 ... n_k) t_1) ((_ tuple_project m_1 ... m_k) t_2))
 )
 \end{verbatim}
 In other words,
@@ -708,7 +746,7 @@ \subsubsection{Table Aggregation}
 when tuples are equivalent for indices $\syntax{n_1}, \ldots, \syntax{n_k}$:
 \begin{verbatim}
 (lambda ((t_1 (Tuple X_1 ... X_j)) (t_2 (Tuple X_1 ... X_j)))
-  (= ((_ project n_1 ... n_k) t_1) ((_ project n_1 ... n_k) t_2))
+  (= ((_ tuple_project n_1 ... n_k) t_1) ((_ tuple_project n_1 ... n_k) t_2))
 )
 \end{verbatim}
 Above, notice that 
@@ -768,6 +806,29 @@ \subsubsection{Table Aggregation}
 fold computation described above unchanged.
 \end{comment}
 
+\section{Extensions}
+
+In this section, we provide an extended syntax for representing
+\emph{abstract} sorts and function symbols.
+We provide an extended type system for type checking terms over these symbols.
+
+\subsection{Abstract Sorts}
+We write
+$\syntax{\abstype{Tuple}}$ and $\syntax{\abstype{Bag}}$
+to denote the abstract tuple type and the abstract bag type respectively.
+These types take no parameters.
+When a term $t$ is annotated with an abstract tuple type,
+conceptually the type of $t$ is some tuple type,
+but the parameters of that type is not given.
+We write $\syntax{\abstype{Table}}$ as shorthand for $\syntax{( Bag\ \abstype{Tuple})}$,
+that is, bags of tuples whose parameters are not given.
+Furthermore, we write $\syntax{\abstypebase}$ to denote
+the abstract type.
+An annotation of the abstract type on a term $t$ gives no information about the type of $t$.
+
+\subsection{Abstract Table Operators}
+
+
 \section{Examples}
 
 

From e36a7f228346d743e75a5d251867e841540b82c7 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 5 Oct 2021 09:23:16 -0500
Subject: [PATCH 03/17] More

---
 tableTheory/tableTheory.tex | 90 ++++++++++++++++++++++---------------
 1 file changed, 54 insertions(+), 36 deletions(-)

diff --git a/tableTheory/tableTheory.tex b/tableTheory/tableTheory.tex
index 9c3445d..a93fadc 100644
--- a/tableTheory/tableTheory.tex
+++ b/tableTheory/tableTheory.tex
@@ -640,18 +640,16 @@ \subsubsection{Table Projection}
 
 \subsubsection{Table Join}
 The signature $\sigtable$ includes 
-all indexed functions symbols of the form
-\begin{align*}
-\syntax{ 
-(\_\ join\ n_1\ m_1\ ...\ n_k\ m_k)
-}
-\end{align*}
-where $n_1, m_1, \ldots, n_k, m_k$ are numerals.
+the function symbol $\syntax{table\_join}$
+%where $n_1, m_1, \ldots, n_k, m_k$ are numerals.
 Its sort definition is:
 
 \begin{verbatim}
 (par (X_1 ... X_j Y_1 ... Y_l)
-  ((_ join n_1 m_1 ... n_k m_k)
+  (table_join
+    
+    ; the pairs of columns to join
+    Int Int ... Int Int
   
     ; The tables to join
     (Table X_1 ... X_j)
@@ -662,54 +660,64 @@ \subsubsection{Table Join}
   )
 )
 \end{verbatim}
-where for all $i = 1, \ldots k$,
-we have that $1 \leq \syntax{n_i} \leq \syntax{j}$, $1 \leq \syntax{m_i} \leq \syntax{l}$
-and $X_{n_i}$ is the same type as $Y_{m_i}$.
-Note that
-$\syntax{join}$ (without numeral indices) denotes the above operator where $\syntax{k}$ is $0$.
+%where for all $i = 1, \ldots k$,
+%we have that $1 \leq \syntax{n_i} \leq \syntax{j}$, $1 \leq \syntax{m_i} \leq \syntax{l}$
+%and $X_{n_i}$ is the same type as $Y_{m_i}$.
+%Note that
+%$\syntax{join}$ (without numeral indices) denotes the above operator where $\syntax{k}$ is $0$.
 
 \paragraph{Semantics}
-When $\syntax{k}=0$, we have that $\syntax{(join\ t_1\ t_2)}$
+When the join operator takes no integer arguments,
+we have that $\syntax{(table\_join\ t_1\ t_2)}$
 denotes the table containing a tuple corresponding to the concatentation
 of tuples $u_1$ and $u_2$
 for each $u_1 \in \syntax{t_1}$ and $u_2 \in \syntax{t_2}$.
-When $\syntax{k}>0$, $\syntax{((\_\ join\ n_1\ m_1\ ...\ n_k\ m_k)\ t_1\ t_2)}$
-is syntax sugar for $\syntax{(filter\ P\ (join\ t_1\ t_2))}$ where $\syntax{P}$ is
+For any $\syntax{k}>0$, $\syntax{(table\_join\ n_1\ m_1\ ...\ n_k\ m_k\ t_1\ t_2)}$
+is syntax sugar for $\syntax{(filter\ P\ (table\_join\ t_1\ t_2))}$ where $\syntax{P}$ is
 the predicate:
 \begin{verbatim}
 (lambda ((t_1 (Tuple X_1 ... X_j)) (t_2 (Tuple Y_1 ... Y_l)))
-  (= ((_ tuple_project n_1 ... n_k) t_1) ((_ tuple_project m_1 ... m_k) t_2))
+  (= (tuple_project n_1 ... n_k t_1) (tuple_project m_1 ... m_k t_2))
 )
 \end{verbatim}
 In other words,
 the join keeps only concatenations of tuples $u_1 \in \syntax{t_1}$ and
 $u_2 \in \syntax{t_2}$ 
 that match on each of the pairs of argument indices (columns) specified by
-the indices of the operator,
+the given indices,
 where $n_1\ ...\ n_k$ are indices corresponding to arguments of $u_1$
 and $m_1\ ...\ m_k$ are indices corresponding to arguments of $u_2$.
 
 \paragraph{Notes}
 \begin{itemize}
-\item The cardinality of $\syntax{(join\ t_1\ t_2)}$
+\item
+In common usage,
+the indices provided to this operator specify columns that are in bounds.
+When the indices are out of bounds,
+the semantics of the join are the same as above, 
+which however rely on the semantics of tuple projection for out of bound indices.
+\item 
+The cardinality of $\syntax{(join\ t_1\ t_2)}$
 is the cardinality of $\syntax{t_1}$ times the cardinality of $\syntax{t_2}$.
+\item 
+When $n_1, \ldots, n_k, m_1, \ldots, m_k$ are numerals,
+$\syntax{((\_\ join\ n_1\ m_1\ ...\ n_k\ m_k)\ t_1\ t_2)}$
+is syntax sugar for the term
+$\syntax{(join\ n_1\ m_1\ ...\ n_k\ m_k\ t_1\ t_2)}$.
 \end{itemize}
 
 
 \subsubsection{Table Aggregation}
 The signature $\sigtable$ includes 
-all indexed function symbols of the form
-$
-\syntax{ 
-(\_\ aggr\ n_1\ ...\ n_k)
-}
-$
-where $\syntax{n_1}, \ldots, \syntax{n_k}$ are numerals,
-called \emph{table aggregation operations}. Their sort definition is:
+the function symbol $\syntax{table\_aggr}$
+called \emph{table aggregation operator}. Its sort definition is:
 
 \begin{verbatim}
 (par (X_1 ... X_j X) 
-  ((_ aggr n_1 ... n_k)
+  (table_aggr
+  
+    ; The columns to aggregate
+    Int ... Int
     
     ; The "combining function"
     (-> (Tuple X_1 ... X_j) X X)
@@ -725,17 +733,15 @@ \subsubsection{Table Aggregation}
   )
 )
 \end{verbatim}
-where for all $i = 1, \ldots k$,
-we have that $1 \leq \syntax{n_i} \leq \syntax{j}$. 
 
 \paragraph{Semantics}
-Let $\syntax{((\_\ aggr\ n_1\ ...\ n_k)\ c\ i\ t)}$
+Let $\syntax{(table\_aggr\ n_1\ ...\ n_k\ c\ i\ t)}$
 be a well-sorted term for
 combining function $\syntax{c}$, 
 initial value $\syntax{i}$,
 and table-to-aggregate $\syntax{t}$.
 Assume that $\syntax{c}$ is \emph{order-agnostic} (see Section~\ref{sec:fold}).
-The application $\syntax{((\_\ aggr\ n_1\ ...\ n_k)\ c\ i\ t)}$ is
+The application $\syntax{(table\_aggr\ n_1\ ...\ n_k\ c\ i\ t)}$ is
 the union of elements computed via a fold operation involving $\syntax{c}$ and $\syntax{i}$
 that run over elements in a partition of the table $\syntax{t}$.
 In particular, this application of an aggregation function is syntax sugar for:
@@ -746,7 +752,7 @@ \subsubsection{Table Aggregation}
 when tuples are equivalent for indices $\syntax{n_1}, \ldots, \syntax{n_k}$:
 \begin{verbatim}
 (lambda ((t_1 (Tuple X_1 ... X_j)) (t_2 (Tuple X_1 ... X_j)))
-  (= ((_ tuple_project n_1 ... n_k) t_1) ((_ tuple_project n_1 ... n_k) t_2))
+  (= (tuple_project n_1 ... n_k t_1) (tuple_project n_1 ... n_k t_2))
 )
 \end{verbatim}
 Above, notice that 
@@ -754,6 +760,21 @@ \subsubsection{Table Aggregation}
 function which takes a $\syntax{(Bag\ (Tuple\ X_1\ ...\ X_j))}$
 and returns a term of type $\syntax{X}$.
 
+\paragraph{Notes}
+\begin{itemize}
+\item
+In common usage,
+the indices provided to this operator specify columns that are in bounds.
+When the indices are out of bounds,
+the semantics of the aggregation are the same as above, 
+which however rely on the semantics of tuple projection for out of bound indices.
+\item
+When $n_1, \ldots, n_k$ are numerals,
+$\syntax{((\_\ table\_aggr\ n_1\ ...\ n_k)\ c\ i\ t)}$
+is syntax sugar for the term
+$\syntax{(table\_aggr\ n_1\ ...\ n_k\ c\ i\ t)}$.
+\end{itemize}
+
 \begin{comment}
 In detail,
 let $\{ t_1, \ldots, t_n \}$ be a partition of table $t$
@@ -826,9 +847,6 @@ \subsection{Abstract Sorts}
 the abstract type.
 An annotation of the abstract type on a term $t$ gives no information about the type of $t$.
 
-\subsection{Abstract Table Operators}
-
-
 \section{Examples}
 
 

From f54f4dce6027027db6f17188e6230d4fd8181e8d Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 5 Oct 2021 09:36:00 -0500
Subject: [PATCH 04/17] More

---
 tableTheory/tableTheory.tex | 38 +++++++++++++++++++++----------------
 1 file changed, 22 insertions(+), 16 deletions(-)

diff --git a/tableTheory/tableTheory.tex b/tableTheory/tableTheory.tex
index a93fadc..9369df8 100644
--- a/tableTheory/tableTheory.tex
+++ b/tableTheory/tableTheory.tex
@@ -237,12 +237,11 @@ \subsubsection{Tuple Selection}
 that $\syntax{(tuple\_select\ n_1\ t_1)}$ and  $\syntax{(tuple\_select\ n_2\ t_2)}$
 must have the same value when $n_1, t_1$ pairwise have the same value as $n_2, t_2$,
 even when $n_1$ and $n_2$ are out of bounds.
-\item When $n$ is a numeral, the indexed function
-$\syntax{(\_\ tuple\_select\ n)}$ is syntactic sugar for the function
-$\syntax{(tuple\_select\ n)}$, meaning that $\syntax{((\_\ tuple\_select\ n)\ t)}$
-and $\syntax{(tuple\_select\ n\ t)}$ specify the same term.
-The former may be used to make it is explicit the index to a tuple selection
-not allowed to be symbolic.
+\item When $n$ is a numeral such that $1 \leq n \leq j$,
+$\syntax{((\_\ tuple\_select\ n)\ t)}$ is syntax sugar for the term
+$\syntax{(tuple\_select\ n\ t)}$.
+The former may be used to make it is explicit the index to a tuple selector
+is within bounds, and is not allowed to be symbolic.
 \end{itemize}
 
 \subsubsection{Tuple Projection}
@@ -290,7 +289,7 @@ \subsubsection{Tuple Projection}
 The function application
 $\syntax{(tuple\_project\ t)}$ always returns the empty tuple for any input $t$.
 \item Similar to the indexed syntax for tuple selection,
-when $n_1, \ldots, n_k$ are numerals,
+when $n_1, \ldots, n_k$ are numerals in the range $[1, j]$,
 $\syntax{((\_\ tuple\_project\ n_1\ ...\ n_k)\ t)}$ is syntax sugar for the term
 $\syntax{(tuple\_project\ n_1\ ...\ n_k\ t)}$.
 \end{itemize}
@@ -598,8 +597,8 @@ \subsubsection{Table Projection}
   )
 )
 \end{verbatim}
-where for each $i = 1, \ldots, j$,
-$1 \leq n_i \leq j$.
+%where for each $i = 1, \ldots, j$,
+%$1 \leq n_i \leq j$.
 
 \paragraph{Semantics}
 
@@ -626,7 +625,8 @@ \subsubsection{Table Projection}
 \paragraph{Notes}
 \begin{itemize}
 \item
-It may be the case that $\syntax{n_i} = \syntax{n_j}$ for some $i \neq j$,
+Like tuple projection,
+it may be the case that $\syntax{n_i} = \syntax{n_j}$ for some $i \neq j$,
 in which case two (or more) copies of the column at that position
 are in the result of the projection.
 \item
@@ -636,6 +636,10 @@ \subsubsection{Table Projection}
 For any table $t$,
 the application taking no integer arguments $\syntax{(table\_project\ t)}$ 
 returns a table with no columns whose cardinality is the same as that of $\syntax{t}$.
+\item
+When $n_1, \ldots, n_k$ are numerals in the range $[1, j]$,
+$\syntax{((\_\ table\_project\ n_1\ ...\ n_k)\ t)}$ is syntax sugar for the term
+$\syntax{(table\_project\ n_1\ ...\ n_k\ t)}$.
 \end{itemize}
 
 \subsubsection{Table Join}
@@ -676,8 +680,8 @@ \subsubsection{Table Join}
 is syntax sugar for $\syntax{(filter\ P\ (table\_join\ t_1\ t_2))}$ where $\syntax{P}$ is
 the predicate:
 \begin{verbatim}
-(lambda ((t_1 (Tuple X_1 ... X_j)) (t_2 (Tuple Y_1 ... Y_l)))
-  (= (tuple_project n_1 ... n_k t_1) (tuple_project m_1 ... m_k t_2))
+(lambda ((u1 (Tuple X_1 ... X_j)) (u2 (Tuple Y_1 ... Y_l)))
+  (= (tuple_project n_1 ... n_k u1) (tuple_project m_1 ... m_k u2))
 )
 \end{verbatim}
 In other words,
@@ -700,7 +704,8 @@ \subsubsection{Table Join}
 The cardinality of $\syntax{(join\ t_1\ t_2)}$
 is the cardinality of $\syntax{t_1}$ times the cardinality of $\syntax{t_2}$.
 \item 
-When $n_1, \ldots, n_k, m_1, \ldots, m_k$ are numerals,
+When $n_1, \ldots, n_k$ are numerals in the range $[1, j]$ 
+and $m_1, \ldots, m_k$ are numerals in the range $[1, l]$, then
 $\syntax{((\_\ join\ n_1\ m_1\ ...\ n_k\ m_k)\ t_1\ t_2)}$
 is syntax sugar for the term
 $\syntax{(join\ n_1\ m_1\ ...\ n_k\ m_k\ t_1\ t_2)}$.
@@ -764,12 +769,13 @@ \subsubsection{Table Aggregation}
 \begin{itemize}
 \item
 In common usage,
-the indices provided to this operator specify columns that are in bounds.
+the indices provided to table aggregation specify columns that are in bounds.
 When the indices are out of bounds,
-the semantics of the aggregation are the same as above, 
+the semantics are the same as above, 
 which however rely on the semantics of tuple projection for out of bound indices.
 \item
-When $n_1, \ldots, n_k$ are numerals,
+When $n_1, \ldots, n_k$ are numerals in the range $[1,j]$,
+we have that
 $\syntax{((\_\ table\_aggr\ n_1\ ...\ n_k)\ c\ i\ t)}$
 is syntax sugar for the term
 $\syntax{(table\_aggr\ n_1\ ...\ n_k\ c\ i\ t)}$.

From f8b832908e0d4ee34390a28372ab6db5bf6d8a34 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 1 Nov 2021 09:27:20 -0500
Subject: [PATCH 05/17] Product, fixes

---
 tableTheory/tableTheory.tex | 50 +++++++++++++++++++++++++++++--------
 1 file changed, 40 insertions(+), 10 deletions(-)

diff --git a/tableTheory/tableTheory.tex b/tableTheory/tableTheory.tex
index 9369df8..2fe9c7b 100644
--- a/tableTheory/tableTheory.tex
+++ b/tableTheory/tableTheory.tex
@@ -281,6 +281,9 @@ \subsubsection{Tuple Projection}
 \paragraph{Notes}
 \begin{itemize}
 \item
+When $k=0$,
+we have that $\syntax{(tuple\_project\ t)}$ is equivalent to the empty tuple.
+\item
 The indices $n_1, \ldots, n_k$ do not need to be ordered such that $n_1 < \ldots < n_k$.
 Moreover, it may be the case that $n_i = n_j$ for some $i \neq j$ in which
 case the component of the original is duplicated in the return value of the projection.
@@ -637,11 +640,37 @@ \subsubsection{Table Projection}
 the application taking no integer arguments $\syntax{(table\_project\ t)}$ 
 returns a table with no columns whose cardinality is the same as that of $\syntax{t}$.
 \item
-When $n_1, \ldots, n_k$ are numerals in the range $[1, j]$,
+When $k>0$ and
+$n_1, \ldots, n_k$ are numerals in the range $[1, j]$,
 $\syntax{((\_\ table\_project\ n_1\ ...\ n_k)\ t)}$ is syntax sugar for the term
 $\syntax{(table\_project\ n_1\ ...\ n_k\ t)}$.
 \end{itemize}
 
+\subsubsection{Table Product}
+The signature $\sigtable$ includes 
+the function symbol $\syntax{table\_product}$
+%where $n_1, m_1, \ldots, n_k, m_k$ are numerals.
+Its sort definition is:
+
+\begin{verbatim}
+(par (X_1 ... X_j Y_1 ... Y_l)
+  (table_product
+  
+    ; The tables to take the product of
+    (Table X_1 ... X_j)
+    (Table Y_1 ... Y_j)
+    
+    ; The return sort
+    (Table X_1 ... X_j Y_1 ... Y_j)
+  )
+)
+\end{verbatim}
+\paragraph{Semantics}
+We have that $\syntax{(table\_product\ t_1\ t_2)}$
+denotes the table containing a tuple corresponding to the concatentation
+of tuples $u_1$ and $u_2$
+for each $u_1 \in \syntax{t_1}$ and $u_2 \in \syntax{t_2}$.
+
 \subsubsection{Table Join}
 The signature $\sigtable$ includes 
 the function symbol $\syntax{table\_join}$
@@ -671,13 +700,8 @@ \subsubsection{Table Join}
 %$\syntax{join}$ (without numeral indices) denotes the above operator where $\syntax{k}$ is $0$.
 
 \paragraph{Semantics}
-When the join operator takes no integer arguments,
-we have that $\syntax{(table\_join\ t_1\ t_2)}$
-denotes the table containing a tuple corresponding to the concatentation
-of tuples $u_1$ and $u_2$
-for each $u_1 \in \syntax{t_1}$ and $u_2 \in \syntax{t_2}$.
-For any $\syntax{k}>0$, $\syntax{(table\_join\ n_1\ m_1\ ...\ n_k\ m_k\ t_1\ t_2)}$
-is syntax sugar for $\syntax{(filter\ P\ (table\_join\ t_1\ t_2))}$ where $\syntax{P}$ is
+We have that $\syntax{(table\_join\ n_1\ m_1\ ...\ n_k\ m_k\ t_1\ t_2)}$
+is syntax sugar for $\syntax{(filter\ P\ (table\_product\ t_1\ t_2))}$ where $\syntax{P}$ is
 the predicate:
 \begin{verbatim}
 (lambda ((u1 (Tuple X_1 ... X_j)) (u2 (Tuple Y_1 ... Y_l)))
@@ -691,10 +715,16 @@ \subsubsection{Table Join}
 the given indices,
 where $n_1\ ...\ n_k$ are indices corresponding to arguments of $u_1$
 and $m_1\ ...\ m_k$ are indices corresponding to arguments of $u_2$.
+Note that if $k=0$, all concenations are kept, and the join is
+equivalent to a product.
 
 \paragraph{Notes}
 \begin{itemize}
 \item
+When the join operator takes no integer arguments,
+we have that $\syntax{(table\_join\ t_1\ t_2)}$
+is equivalent to $\syntax{(table\_product\ t_1\ t_2)}$.
+\item
 In common usage,
 the indices provided to this operator specify columns that are in bounds.
 When the indices are out of bounds,
@@ -703,8 +733,8 @@ \subsubsection{Table Join}
 \item 
 The cardinality of $\syntax{(join\ t_1\ t_2)}$
 is the cardinality of $\syntax{t_1}$ times the cardinality of $\syntax{t_2}$.
-\item 
-When $n_1, \ldots, n_k$ are numerals in the range $[1, j]$ 
+\item
+If $k>0$ and $n_1, \ldots, n_k$ are numerals in the range $[1, j]$ 
 and $m_1, \ldots, m_k$ are numerals in the range $[1, l]$, then
 $\syntax{((\_\ join\ n_1\ m_1\ ...\ n_k\ m_k)\ t_1\ t_2)}$
 is syntax sugar for the term

From ee31754b608b30c582a421a2cf7371787295d882 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 5 Apr 2022 09:11:46 -0500
Subject: [PATCH 06/17] Update tokens

---
 tableTheory/tableTheory.tex | 156 ++++++++++++++++++------------------
 1 file changed, 78 insertions(+), 78 deletions(-)

diff --git a/tableTheory/tableTheory.tex b/tableTheory/tableTheory.tex
index 2fe9c7b..592a538 100644
--- a/tableTheory/tableTheory.tex
+++ b/tableTheory/tableTheory.tex
@@ -207,11 +207,11 @@ \subsubsection{Tuple Construction}
 
 \subsubsection{Tuple Selection}
 The signature $\sigtable$ includes 
-the polymorphic function symbol $\syntax{tuple\_select}$.
+the polymorphic function symbol $\syntax{tuple.select}$.
 Its sort definition is parametrized on $j$ sorts:
 \begin{verbatim}
 (par (X_1 ... X_j) 
-  (tuple_select
+  (tuple.select
     
     ; The index we are selecting 
     Int
@@ -225,21 +225,21 @@ \subsubsection{Tuple Selection}
 )
 \end{verbatim}
 When $1 \leq n \leq j$,
-the term $\syntax{(tuple\_select\ n\ t)}$ is
+the term $\syntax{(tuple.select\ n\ t)}$ is
 interpreted as the $\syntax{n}^{th}$ argument of the tuple $\syntax{t}$.
 When $n$ is out of bounds, e.g. $1 \leq n \leq j$ does not hold,
-then the value of $\syntax{(tuple\_select\ n\ t)}$ is unspecified.
+then the value of $\syntax{(tuple.select\ n\ t)}$ is unspecified.
 
 \paragraph{Notes}
 \begin{itemize}
 \item Like other operators with partially specified semantics,
-the symbol $\syntax{tuple\_select}$ behaves like a function, meaning
-that $\syntax{(tuple\_select\ n_1\ t_1)}$ and  $\syntax{(tuple\_select\ n_2\ t_2)}$
+the symbol $\syntax{tuple.select}$ behaves like a function, meaning
+that $\syntax{(tuple.select\ n_1\ t_1)}$ and  $\syntax{(tuple.select\ n_2\ t_2)}$
 must have the same value when $n_1, t_1$ pairwise have the same value as $n_2, t_2$,
 even when $n_1$ and $n_2$ are out of bounds.
 \item When $n$ is a numeral such that $1 \leq n \leq j$,
-$\syntax{((\_\ tuple\_select\ n)\ t)}$ is syntax sugar for the term
-$\syntax{(tuple\_select\ n\ t)}$.
+$\syntax{((\_\ tuple.select\ n)\ t)}$ is syntax sugar for the term
+$\syntax{(tuple.select\ n\ t)}$.
 The former may be used to make it is explicit the index to a tuple selector
 is within bounds, and is not allowed to be symbolic.
 \end{itemize}
@@ -247,12 +247,12 @@ \subsubsection{Tuple Selection}
 \subsubsection{Tuple Projection}
 \label{sec:tup-project}
 The signature $\sigtable$ includes 
-the function symbol $\syntax{tuple\_project}$.
+the function symbol $\syntax{tuple.project}$.
 Its sort definition includes an unbounded number of integer arguments, followed
 by a tuple:
 \begin{verbatim}
 (par (X_1 ... X_j) 
-  (tuple_project
+  (tuple.project
     
     ; the components to project
     Int ... Int
@@ -266,12 +266,12 @@ \subsubsection{Tuple Projection}
 )
 \end{verbatim}
 The term
-$\syntax{(tuple\_project\ n_1\ ...\ n_k\ t)}$
+$\syntax{(tuple.project\ n_1\ ...\ n_k\ t)}$
 returns the tuple obtained by collecting the
 values from $t$ at positions $n_1 \ldots n_k$.
 In other words, this term is equivalent to:
 \begin{align*}
-\syntax{(tuple\ (tuple\_select\ n_1\ t)\ ...\ (tuple\_select\ n_k\ t))}
+\syntax{(tuple\ (tuple.select\ n_1\ t)\ ...\ (tuple.select\ n_k\ t))}
 \end{align*}
 Notice that if any $n_i$ in the above term is out of bounds, the value of
 that component of the returned tuple is unspecified.
@@ -282,7 +282,7 @@ \subsubsection{Tuple Projection}
 \begin{itemize}
 \item
 When $k=0$,
-we have that $\syntax{(tuple\_project\ t)}$ is equivalent to the empty tuple.
+we have that $\syntax{(tuple.project\ t)}$ is equivalent to the empty tuple.
 \item
 The indices $n_1, \ldots, n_k$ do not need to be ordered such that $n_1 < \ldots < n_k$.
 Moreover, it may be the case that $n_i = n_j$ for some $i \neq j$ in which
@@ -290,11 +290,11 @@ \subsubsection{Tuple Projection}
 \item
 The list of integer arguments to tuple projection can be empty.
 The function application
-$\syntax{(tuple\_project\ t)}$ always returns the empty tuple for any input $t$.
+$\syntax{(tuple.project\ t)}$ always returns the empty tuple for any input $t$.
 \item Similar to the indexed syntax for tuple selection,
 when $n_1, \ldots, n_k$ are numerals in the range $[1, j]$,
-$\syntax{((\_\ tuple\_project\ n_1\ ...\ n_k)\ t)}$ is syntax sugar for the term
-$\syntax{(tuple\_project\ n_1\ ...\ n_k\ t)}$.
+$\syntax{((\_\ tuple.project\ n_1\ ...\ n_k)\ t)}$ is syntax sugar for the term
+$\syntax{(tuple.project\ n_1\ ...\ n_k\ t)}$.
 \end{itemize}
 
 \subsection{Bags}
@@ -326,10 +326,10 @@ \subsubsection{Bag Construction}
 
 \subsubsection{Bag Count}
 The signature $\sigtable$ includes 
-the function symbol $\syntax{count}$ whose sort definition is
+the function symbol $\syntax{bag.count}$ whose sort definition is
 \begin{verbatim}
 (par (X)
-  (count 
+  (bag.count 
   
     ; The element we are counting
     X 
@@ -349,7 +349,7 @@ \subsubsection{Bag Count}
 \begin{itemize}
 \item
 We do not include an explicit membership predicate for bags, although note that
-the formula $\syntax{(>\ (count\ u\ t)\ 0)}$ holds exactly when $\syntax{u}$
+the formula $\syntax{(>\ (bag.count\ u\ t)\ 0)}$ holds exactly when $\syntax{u}$
 is a member of $\syntax{t}$ (with any multiplicity).
 \end{itemize}
 
@@ -357,9 +357,9 @@ \subsubsection{Bag Compositions}
 \label{sec:bag-compositions}
 The signature $\sigtable$ includes 
 the binary function symbols 
-$\syntax{union\_max}$, $\syntax{union\_disjoint}$, 
-$\syntax{intersect\_min}$, $\syntax{difference\_subtract}$ and
-$\syntax{difference\_remove}$.
+$\syntax{bag.union\_max}$, $\syntax{bag.union\_disjoint}$, 
+$\syntax{bag.intersect\_min}$, $\syntax{bag.difference\_subtract}$ and
+$\syntax{bag.difference\_remove}$.
 Each $\syntax{f}$ of the aforementioned operators
 has sort definition:
 \begin{verbatim}
@@ -368,11 +368,11 @@ \subsubsection{Bag Compositions}
 These functions are such that for all elements $\syntax{x}$
 and bags $\syntax{A,B}$:
 \begin{verbatim}
-(count x (union_max A B))            = (max (count x A) (count x B))
-(count x (union_disjoint A B))       = (+ (count x A) (count x B))
-(count x (intersect_min A B))        = (min (count x A) (count x B))
-(count x (difference_subtract A B))  = (max (- (count x A) (count x B)) 0)
-(count x (difference_remove A B))    = (ite (> (count x B) 0) 0 (count x A))
+(bag.count x (bag.union_max A B))            = (max (bag.count x A) (bag.count x B))
+(bag.count x (bag.union_disjoint A B))       = (+ (bag.count x A) (bag.count x B))
+(bag.count x (bag.intersect_min A B))        = (min (bag.count x A) (bag.count x B))
+(bag.count x (bag.difference_subtract A B))  = (max (- (bag.count x A) (bag.count x B)) 0)
+(bag.count x (bag.difference_remove A B))    = (ite (> (bag.count x B) 0) 0 (bag.count x A))
 \end{verbatim}
 where $\syntax{max}$ and $\syntax{min}$ are binary functions
 returning the maximum (resp. minimum) of two integers, and $\syntax{ite}$
@@ -383,7 +383,7 @@ \subsubsection{Bag Cardinality}
 the function symbol $\syntax{card}$ whose sort definition is
 \begin{verbatim}
 (par (X) 
-  (card 
+  (bag.card 
   
     ; The bag to process
     (Bag X) 
@@ -393,19 +393,19 @@ \subsubsection{Bag Cardinality}
   )
 )
 \end{verbatim}
-The term $\syntax{(card\ t)}$ is equal to
+The term $\syntax{(bag.card\ t)}$ is equal to
 the total number of elements (taking into account multiplicity)
 that occur in the bag $\syntax{t}$.
-For example, the term $\syntax{(card\ (bag\ t\ n))}$ is
+For example, the term $\syntax{(bag.card\ (bag\ t\ n))}$ is
 equivalent to $\syntax{n}$.
 
 \subsubsection{Bag Filtering}
 The signature $\sigtable$ includes 
-the function symbol $\syntax{filter}$. Its sort definition is:
+the function symbol $\syntax{bag.filter}$. Its sort definition is:
 
 \begin{verbatim}
 (par (X)
-  (filter
+  (bag.filter
   
     ; The predicate we are filtering based on
     (-> X Bool)
@@ -424,12 +424,12 @@ \subsubsection{Bag Filtering}
 from its first argument
 for which the predicate of its second argument is true.
 In other words,
-$\syntax{(filter\ P\ t)}$
+$\syntax{(bag.filter\ P\ t)}$
 is the bag containing exactly
 the elements $u$ from $\syntax{t}$
 such that $\syntax{(P\ u)}$ is true.
 Notice that if $\syntax{(P\ u)}$ is true,
-then $u$ has the same multiplicity in $\syntax{(filter\ P\ t)}$
+then $u$ has the same multiplicity in $\syntax{(bag.filter\ P\ t)}$
 as it did in $\syntax{t}$.
 
 \subsubsection{Bag Map}
@@ -438,7 +438,7 @@ \subsubsection{Bag Map}
 
 \begin{verbatim}
 (par (X_1 X_2)
-  (map
+  (bag.map
     
     ; The function we are applying
     (-> X_1 X_2)
@@ -456,22 +456,22 @@ \subsubsection{Bag Map}
 The map operator runs the function provided
 in the second argument to all elements in the bag.
 In other words,
-$\syntax{(map\ f\ t)}$
+$\syntax{(bag.map\ f\ t)}$
 is the bag containing exactly
 the elements $\syntax{(f\ u)}$
 for each $\syntax{u}$ that occurs in $\syntax{t}$.
 The multiplicity of $\syntax{(f\ u)}$
-in $\syntax{(map\ f\ t)}$
+in $\syntax{(bag.map\ f\ t)}$
 is the same as the multiplicity of $\syntax{u}$ in $\syntax{t}$.
 
 \subsubsection{Bag Fold}
 \label{sec:fold}
 The signature $\sigtable$ includes 
-the function symbol $\syntax{fold}$. Its sort definition is:
+the function symbol $\syntax{bag.fold}$. Its sort definition is:
 
 \begin{verbatim}
 (par (X_1 X_2)
-  (fold
+  (bag.fold
     
     ; The "combining" function we are applying
     (-> X_1 X_2 X_2)
@@ -492,7 +492,7 @@ \subsubsection{Bag Fold}
 \paragraph{Semantics}
 Given a bag $t$ whose elements are $\syntax{u_1}, \ldots, \syntax{u_n}$,
 assume an arbitrary total ordering over these elements $\preceq$.
-Then, $\syntax{(fold\ c\ i\ t)}$ is equivalent to
+Then, $\syntax{(bag.fold\ c\ i\ t)}$ is equivalent to
 $
 \syntax{
 (c\ u_n\ ...\ (c\ u_2\ (c\ u_1\ i))\ ...\ )
@@ -532,11 +532,11 @@ \subsubsection{Bag Fold}
 
 \subsubsection{Bag Partition}
 The signature $\sigtable$ includes 
-the function symbol $\syntax{partition}$. Its sort definition is:
+the function symbol $\syntax{bag.partition}$. Its sort definition is:
 
 \begin{verbatim}
 (par (X)
-  (partition
+  (bag.partition
     
     ; The equivalence relation
     (-> X X Bool)
@@ -552,7 +552,7 @@ \subsubsection{Bag Partition}
 
 \paragraph{Semantics}
 Given a bag $t$, 
-the term $\syntax{(partition\ r\ t)}$ is interpreted
+the term $\syntax{(bag.partition\ r\ t)}$ is interpreted
 as a bag of bags that partition the elements of $\syntax{t}$,
 whose elements (of bag sort) are $\syntax{t_1}, \ldots, \syntax{t_n}$.
 For each pair of elements $\syntax{u_i}, \syntax{u_j}$
@@ -563,11 +563,11 @@ \subsubsection{Bag Partition}
 \begin{itemize}
 \item
 The argument $r$ passed as the
-first argument to $\syntax{partition}$ is expected to be an equivalence relation.
+first argument to $\syntax{bag.partition}$ is expected to be an equivalence relation.
 In particular, this means it is reflexive, symmetric and transitive.
 This ensures that a partition with the above properties
 can be computed.
-The semantics of applications of $\syntax{partition}$ for relations $\syntax{r}$
+The semantics of applications of $\syntax{bag.partition}$ for relations $\syntax{r}$
 that are not equivalence relations is undefined.
 \item
 If $\syntax{u}$ occurs with some multiplicity $n$ in $\syntax{t}$,
@@ -579,7 +579,7 @@ \subsection{Tables}
 \subsubsection{Table Projection}
 The signature $\sigtable$ includes 
 the functions symbol of the form
-$\syntax{tuple\_project}$.
+$\syntax{tuple.project}$.
 %Note this operator is overloaded,
 %as a separate projection function (of the same name)
 %is also defined for tuples in Section~\ref{sec:tup-project}.
@@ -587,7 +587,7 @@ \subsubsection{Table Projection}
 by a tuple:
 \begin{verbatim}
 (par (X_1 ... X_j) 
-  (table_project
+  (table.project
   
     ; The columns to project
     Int ... Int
@@ -608,18 +608,18 @@ \subsubsection{Table Projection}
 A projection operator for tables keeps (copies) of the given columns
 in each (tuple) element of its argument.
 In other words,
-consider the term $\syntax{(table\_project\ n_1\ ...\ n_k\ t)}$
+consider the term $\syntax{(table.project\ n_1\ ...\ n_k\ t)}$
 where $t$ is a table and $n_1, \ldots, n_k$ are integers.
 %The value of this term is the table containing a tuple of the form
 %$(u_{n_1}, \ldots, u_{n_k})$
 %for each tuple $(u_1, \ldots, u_j)$ from $t$.
 %More precisely,
-%the term $\syntax{((table\_project\ n_1\ ...\ n_k\ t)}$
+%the term $\syntax{((table.project\ n_1\ ...\ n_k\ t)}$
 This term
 can be seen as syntax sugar for $\syntax{(map\ p\ t)}$ where $\syntax{p}$
 is the function:
 \begin{verbatim}
-(lambda ((u (Tuple X_1 ... X_j))) (tuple_project n_1 ... n_k u))
+(lambda ((u (Tuple X_1 ... X_j))) (tuple.project n_1 ... n_k u))
 \end{verbatim}
 In other words, table projection
 applies the tuple projection on all tuples in its table argument $\syntax{t}$
@@ -633,53 +633,53 @@ \subsubsection{Table Projection}
 in which case two (or more) copies of the column at that position
 are in the result of the projection.
 \item
-The cardinality of $\syntax{(table\_project\ n_1\ ...\ n_k\ t)}$ is
+The cardinality of $\syntax{(table.project\ n_1\ ...\ n_k\ t)}$ is
 the same as the cardinality of $\syntax{t}$.
 \item
 For any table $t$,
-the application taking no integer arguments $\syntax{(table\_project\ t)}$ 
+the application taking no integer arguments $\syntax{(table.project\ t)}$ 
 returns a table with no columns whose cardinality is the same as that of $\syntax{t}$.
 \item
 When $k>0$ and
 $n_1, \ldots, n_k$ are numerals in the range $[1, j]$,
-$\syntax{((\_\ table\_project\ n_1\ ...\ n_k)\ t)}$ is syntax sugar for the term
-$\syntax{(table\_project\ n_1\ ...\ n_k\ t)}$.
+$\syntax{((\_\ table.project\ n_1\ ...\ n_k)\ t)}$ is syntax sugar for the term
+$\syntax{(table.project\ n_1\ ...\ n_k\ t)}$.
 \end{itemize}
 
 \subsubsection{Table Product}
 The signature $\sigtable$ includes 
-the function symbol $\syntax{table\_product}$
+the function symbol $\syntax{table.product}$
 %where $n_1, m_1, \ldots, n_k, m_k$ are numerals.
 Its sort definition is:
 
 \begin{verbatim}
 (par (X_1 ... X_j Y_1 ... Y_l)
-  (table_product
+  (table.product
   
     ; The tables to take the product of
     (Table X_1 ... X_j)
     (Table Y_1 ... Y_j)
-    
+
     ; The return sort
     (Table X_1 ... X_j Y_1 ... Y_j)
   )
 )
 \end{verbatim}
 \paragraph{Semantics}
-We have that $\syntax{(table\_product\ t_1\ t_2)}$
+We have that $\syntax{(table.product\ t_1\ t_2)}$
 denotes the table containing a tuple corresponding to the concatentation
 of tuples $u_1$ and $u_2$
 for each $u_1 \in \syntax{t_1}$ and $u_2 \in \syntax{t_2}$.
 
 \subsubsection{Table Join}
 The signature $\sigtable$ includes 
-the function symbol $\syntax{table\_join}$
+the function symbol $\syntax{table.join}$
 %where $n_1, m_1, \ldots, n_k, m_k$ are numerals.
 Its sort definition is:
 
 \begin{verbatim}
 (par (X_1 ... X_j Y_1 ... Y_l)
-  (table_join
+  (table.join
     
     ; the pairs of columns to join
     Int Int ... Int Int
@@ -700,12 +700,12 @@ \subsubsection{Table Join}
 %$\syntax{join}$ (without numeral indices) denotes the above operator where $\syntax{k}$ is $0$.
 
 \paragraph{Semantics}
-We have that $\syntax{(table\_join\ n_1\ m_1\ ...\ n_k\ m_k\ t_1\ t_2)}$
-is syntax sugar for $\syntax{(filter\ P\ (table\_product\ t_1\ t_2))}$ where $\syntax{P}$ is
+We have that $\syntax{(table.join\ n_1\ m_1\ ...\ n_k\ m_k\ t_1\ t_2)}$
+is syntax sugar for $\syntax{(filter\ P\ (table.product\ t_1\ t_2))}$ where $\syntax{P}$ is
 the predicate:
 \begin{verbatim}
 (lambda ((u1 (Tuple X_1 ... X_j)) (u2 (Tuple Y_1 ... Y_l)))
-  (= (tuple_project n_1 ... n_k u1) (tuple_project m_1 ... m_k u2))
+  (= (tuple.project n_1 ... n_k u1) (tuple.project m_1 ... m_k u2))
 )
 \end{verbatim}
 In other words,
@@ -722,8 +722,8 @@ \subsubsection{Table Join}
 \begin{itemize}
 \item
 When the join operator takes no integer arguments,
-we have that $\syntax{(table\_join\ t_1\ t_2)}$
-is equivalent to $\syntax{(table\_product\ t_1\ t_2)}$.
+we have that $\syntax{(table.join\ t_1\ t_2)}$
+is equivalent to $\syntax{(table.product\ t_1\ t_2)}$.
 \item
 In common usage,
 the indices provided to this operator specify columns that are in bounds.
@@ -731,25 +731,25 @@ \subsubsection{Table Join}
 the semantics of the join are the same as above, 
 which however rely on the semantics of tuple projection for out of bound indices.
 \item 
-The cardinality of $\syntax{(join\ t_1\ t_2)}$
+The cardinality of $\syntax{(table.join\ t_1\ t_2)}$
 is the cardinality of $\syntax{t_1}$ times the cardinality of $\syntax{t_2}$.
 \item
 If $k>0$ and $n_1, \ldots, n_k$ are numerals in the range $[1, j]$ 
 and $m_1, \ldots, m_k$ are numerals in the range $[1, l]$, then
-$\syntax{((\_\ join\ n_1\ m_1\ ...\ n_k\ m_k)\ t_1\ t_2)}$
+$\syntax{((\_\ table.join\ n_1\ m_1\ ...\ n_k\ m_k)\ t_1\ t_2)}$
 is syntax sugar for the term
-$\syntax{(join\ n_1\ m_1\ ...\ n_k\ m_k\ t_1\ t_2)}$.
+$\syntax{(table.join\ n_1\ m_1\ ...\ n_k\ m_k\ t_1\ t_2)}$.
 \end{itemize}
 
 
 \subsubsection{Table Aggregation}
 The signature $\sigtable$ includes 
-the function symbol $\syntax{table\_aggr}$
+the function symbol $\syntax{table.aggr}$
 called \emph{table aggregation operator}. Its sort definition is:
 
 \begin{verbatim}
 (par (X_1 ... X_j X) 
-  (table_aggr
+  (table.aggr
   
     ; The columns to aggregate
     Int ... Int
@@ -770,28 +770,28 @@ \subsubsection{Table Aggregation}
 \end{verbatim}
 
 \paragraph{Semantics}
-Let $\syntax{(table\_aggr\ n_1\ ...\ n_k\ c\ i\ t)}$
+Let $\syntax{(table.aggr\ n_1\ ...\ n_k\ c\ i\ t)}$
 be a well-sorted term for
 combining function $\syntax{c}$, 
 initial value $\syntax{i}$,
 and table-to-aggregate $\syntax{t}$.
 Assume that $\syntax{c}$ is \emph{order-agnostic} (see Section~\ref{sec:fold}).
-The application $\syntax{(table\_aggr\ n_1\ ...\ n_k\ c\ i\ t)}$ is
+The application $\syntax{(table.aggr\ n_1\ ...\ n_k\ c\ i\ t)}$ is
 the union of elements computed via a fold operation involving $\syntax{c}$ and $\syntax{i}$
 that run over elements in a partition of the table $\syntax{t}$.
 In particular, this application of an aggregation function is syntax sugar for:
 \begin{verbatim}
-(map (fold c i) (partition eq t))
+(bag.map (bag.fold c i) (bag.partition eq t))
 \end{verbatim}
 where $\syntax{eq}$ is the relation over tuples that holds
 when tuples are equivalent for indices $\syntax{n_1}, \ldots, \syntax{n_k}$:
 \begin{verbatim}
 (lambda ((t_1 (Tuple X_1 ... X_j)) (t_2 (Tuple X_1 ... X_j)))
-  (= (tuple_project n_1 ... n_k t_1) (tuple_project n_1 ... n_k t_2))
+  (= (tuple.project n_1 ... n_k t_1) (tuple.project n_1 ... n_k t_2))
 )
 \end{verbatim}
 Above, notice that 
-$\syntax{(fold\ c\ i)}$ is a partial application of the fold
+$\syntax{(bag.fold\ c\ i)}$ is a partial application of the fold
 function which takes a $\syntax{(Bag\ (Tuple\ X_1\ ...\ X_j))}$
 and returns a term of type $\syntax{X}$.
 
@@ -806,9 +806,9 @@ \subsubsection{Table Aggregation}
 \item
 When $n_1, \ldots, n_k$ are numerals in the range $[1,j]$,
 we have that
-$\syntax{((\_\ table\_aggr\ n_1\ ...\ n_k)\ c\ i\ t)}$
+$\syntax{((\_\ table.aggr\ n_1\ ...\ n_k)\ c\ i\ t)}$
 is syntax sugar for the term
-$\syntax{(table\_aggr\ n_1\ ...\ n_k\ c\ i\ t)}$.
+$\syntax{(table.aggr\ n_1\ ...\ n_k\ c\ i\ t)}$.
 \end{itemize}
 
 \begin{comment}
@@ -883,7 +883,7 @@ \subsection{Abstract Sorts}
 the abstract type.
 An annotation of the abstract type on a term $t$ gives no information about the type of $t$.
 
-\section{Examples}
+%\section{Examples}
 
 
 

From b2535d268610fe52f8b829197c5927dd4c7e3329 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Apr 2022 10:17:28 -0500
Subject: [PATCH 07/17] Examples

---
 tableTheory/tableTheory.tex | 142 +++++++++++++++++++++++++++++++++++-
 1 file changed, 139 insertions(+), 3 deletions(-)

diff --git a/tableTheory/tableTheory.tex b/tableTheory/tableTheory.tex
index 592a538..520a680 100644
--- a/tableTheory/tableTheory.tex
+++ b/tableTheory/tableTheory.tex
@@ -321,7 +321,7 @@ \subsubsection{Bag Construction}
 %If $n=0$,
 %then $\syntax{bag}$ denotes the empty bag.
 Notice that bags containing multiple distinct elements
-can be constructed using $\syntax{union\_disjoint}$,
+can be constructed using $\syntax{bag.union\_disjoint}$,
 introduced in Section~\ref{sec:bag-compositions}
 
 \subsubsection{Bag Count}
@@ -378,6 +378,14 @@ \subsubsection{Bag Compositions}
 returning the maximum (resp. minimum) of two integers, and $\syntax{ite}$
 is the if-then-else construct.
 
+\paragraph{Notes}
+\begin{itemize}
+\item
+The above operators are \emph{chainable}, that is,
+$\syntax{(bag.union_max\ A\ B\ C)}$ is syntax sugar for
+$\syntax{(bag.union_max\ (bag.union_max\ A\ B)\ C)}$.
+\end{itemize}
+
 \subsubsection{Bag Cardinality}
 The signature $\sigtable$ includes 
 the function symbol $\syntax{card}$ whose sort definition is
@@ -867,7 +875,7 @@ \section{Extensions}
 
 In this section, we provide an extended syntax for representing
 \emph{abstract} sorts and function symbols.
-We provide an extended type system for type checking terms over these symbols.
+%We provide an extended type system for type checking terms over these symbols.
 
 \subsection{Abstract Sorts}
 We write
@@ -883,8 +891,136 @@ \subsection{Abstract Sorts}
 the abstract type.
 An annotation of the abstract type on a term $t$ gives no information about the type of $t$.
 
-%\section{Examples}
+\section{Examples}
+
+\subsection{Table Transformation}
+The following is an example using the table theory in a syntax-guided synthesis problem
+in the SyGuS 2.1 format.
+
+\begin{verbatim}
+; Predicates for tuples
+(define-fun p_true ((r (Tuple Int String))) Bool true)
+(define-fun p_false ((r (Tuple Int String))) Bool false)
+(define-fun p_gt_zero ((r (Tuple Int String))) Bool (> ((_ tuple.select 0) r) 0))
+(define-fun p_lt_zero ((r (Tuple Int String))) Bool (< ((_ tuple.select 0) r) 0))
+(define-fun p_str_emp ((r (Tuple Int String))) Bool (= (str.len ((_ tuple.select 1) r)) 0))
+
+; Synthesize a transformation for tables with an integer and string column
+(synth-fun f ((x (Table Int String))) (Table Int String)(
+(Start (Table Int String))
+(StartTuple (Tuple Int String))
+(StartInt Int)
+(StartString String)
+(StartPred (-> (Tuple Int String) Bool))
+)(
+(Start (Table Int String) (
+  x
+  (bag StartTuple StartInt)
+  (bag.filter StartPred Start)
+  (bag.union_disjoint Start Start)
+))
+(StartTuple (Tuple Int String) (
+  (tuple StartInt StartString)
+))
+(StartInt Int (
+  0 1
+  ((_ tuple.select 0) StartTuple)
+))
+(StartString String (
+  "" "A" "B" "C" "D" "E" 
+  ((_ tuple.select 1) StartTuple)
+))
+(StartPred (-> (Tuple Int String) Bool)(
+  p_true p_false p_gt_zero p_lt_zero p_str_emp
+))
+))
+(constraint (= (f 
+(bag.union_disjoint
+(bag (tuple 1 "A") 1)
+(bag (tuple (- 2) "B") 1)
+(bag (tuple (- 1) "C") 1)
+(bag (tuple 1 "C") 1)
+(bag (tuple 0 "D") 1)
+(bag (tuple 2 "E") 1))
+)
+(bag.union_disjoint
+(bag (tuple 1 "A") 1)
+(bag (tuple 1 "C") 1)
+(bag (tuple 2 "E") 1))
+))
+(check-synth)
+\end{verbatim}
+In this example, we are looking to synthesize a transformation on
+tables with one integer column and one string column whose body
+fits the provided grammar.
+A possible correct response for this example from a synthesis solver is:
+\begin{verbatim}
+(
+(define-fun f ((x (Table Int String))) (Table Int String)
+  (bag.filter p_gt_zero x))
+)
+\end{verbatim}
+In particular, the transformation filters the rows of the table such that
+only those whose integer column is greater than zero, as specified by the
+predicate $\syntax{p\_gt\_zero}$ are kept.
+
+\subsection{Table Transformation with Abstract Sorts}
+The following additionally makes use of abstract sorts.
 
+\begin{verbatim}
+(synth-fun f ((x (Table String))) (Table Int String) (
+(Start ?Table)
+(StartTuple (Tuple Int))
+)(
+(Start ?Table (
+  x
+  (bag StartTuple StartInt)
+  (bag.union_disjoint Start Start)
+  (table.product Start Start)
+))
+(StartTuple (Tuple Int) (
+  (tuple StartInt)
+))
+(StartInt Int (
+  0 1 7
+  (tuple.select StartInt Start)
+))
+))
+(constraint (= (f 
+(bag.union_disjoint
+(bag (tuple "A") 1)
+(bag (tuple "C") 1)
+(bag (tuple "E") 1))
+)
+(bag.union_disjoint
+(bag (tuple 7 "A") 1)
+(bag (tuple 7 "C") 1)
+(bag (tuple 7 "E") 1))
+))
+(check-synth)
+\end{verbatim}
+In this example, we are looking to synthesize a function that transforms
+a table having a string column to one that has an integer and a string column.
+Notice that the grammar for $\syntax{f}$ begins with a non-terminal
+symbol $\syntax{Start}$ whose type annotation is $\syntax{?Table}$.
+In particular, this means that $\syntax{Start}$ may generate terms having
+\emph{any} table type. However, a term generated by this non-terminal is
+only valid as a solution for $\syntax{f}$ if it has type $\syntax{(Table\ Int\ String)}$,
+the return type of $\syntax{f}$.
+Note that several non-terminals of the above grammar are well-typed only for a subset of the terms they apply to.
+For example, $\syntax{(tuple.select\ StartInt\ Start)}$ is the right hand side of
+a production rule for $\syntax{StartInt}$.
+Thus, it is assumed that this rule is limited to generating terms
+$\syntax{(tuple.select\ n\ s)}$ where $\syntax{s}$ is a table whose $\syntax{n}^{th}$ column is an integer.
+
+A possible correct response for this example from a synthesis solver is:
+\begin{verbatim}
+(
+(define-fun f ((x (Table String))) (Table Int String) 
+  (table.product (bag (tuple 7) 1) x)
+)
+\end{verbatim}
 
+In particular, this prepends the integer $\syntax{7}$ to all rows of the original table.
 
 \end{document}

From 312d257234728df2b5bcc83890f0d42302f02937 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Apr 2022 10:30:25 -0500
Subject: [PATCH 08/17] More mods

---
 tableTheory/tableTheory.tex | 28 ++++++++++++++++++++++++----
 1 file changed, 24 insertions(+), 4 deletions(-)

diff --git a/tableTheory/tableTheory.tex b/tableTheory/tableTheory.tex
index 520a680..ee1e707 100644
--- a/tableTheory/tableTheory.tex
+++ b/tableTheory/tableTheory.tex
@@ -871,13 +871,12 @@ \subsubsection{Table Aggregation}
 fold computation described above unchanged.
 \end{comment}
 
-\section{Extensions}
+\section{Abstract Sorts}
 
 In this section, we provide an extended syntax for representing
 \emph{abstract} sorts and function symbols.
 %We provide an extended type system for type checking terms over these symbols.
 
-\subsection{Abstract Sorts}
 We write
 $\syntax{\abstype{Tuple}}$ and $\syntax{\abstype{Bag}}$
 to denote the abstract tuple type and the abstract bag type respectively.
@@ -887,8 +886,12 @@ \subsection{Abstract Sorts}
 but the parameters of that type is not given.
 We write $\syntax{\abstype{Table}}$ as shorthand for $\syntax{( Bag\ \abstype{Tuple})}$,
 that is, bags of tuples whose parameters are not given.
-Furthermore, we write $\syntax{\abstypebase}$ to denote
-the abstract type.
+Furthermore, 
+the syntax $\syntax{\abstype{->}}$ specifies the abstract function sort,
+i.e. functions having an unspecified (at least one) argument sort and a return sort.
+
+We write $\syntax{\abstypebase}$ to denote
+the (fully) abstract type.
 An annotation of the abstract type on a term $t$ gives no information about the type of $t$.
 
 \section{Examples}
@@ -977,6 +980,7 @@ \subsection{Table Transformation with Abstract Sorts}
   (bag StartTuple StartInt)
   (bag.union_disjoint Start Start)
   (table.product Start Start)
+  (table.project StartInt StartInt Start)
 ))
 (StartTuple (Tuple Int) (
   (tuple StartInt)
@@ -1023,4 +1027,20 @@ \subsection{Table Transformation with Abstract Sorts}
 
 In particular, this prepends the integer $\syntax{7}$ to all rows of the original table.
 
+Note the use of abstract sorts in this example gives
+greater flexibility for specifications. 
+Although not necessary in this example, the solution
+may involve types that are not explicitly specified in the grammar.
+For example,
+the following solution involves tables with two integer columns and a string column:
+\begin{verbatim}
+(
+(define-fun f ((x (Table String))) (Table Int String) 
+  (table.project 1 2 
+    (table.product (bag (tuple 0) 1) 
+    (table.product (bag (tuple 7) 1) x))))
+)
+\end{verbatim}
+It is also a solution to the above problem.
+
 \end{document}

From 5e698aaf76a6bf36bb1a93e39e8c954f7df474df Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Apr 2022 10:32:53 -0500
Subject: [PATCH 09/17] Minor

---
 tableTheory/tableTheory.tex | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/tableTheory/tableTheory.tex b/tableTheory/tableTheory.tex
index ee1e707..704d113 100644
--- a/tableTheory/tableTheory.tex
+++ b/tableTheory/tableTheory.tex
@@ -1017,7 +1017,8 @@ \subsection{Table Transformation with Abstract Sorts}
 Thus, it is assumed that this rule is limited to generating terms
 $\syntax{(tuple.select\ n\ s)}$ where $\syntax{s}$ is a table whose $\syntax{n}^{th}$ column is an integer.
 
-A possible correct response for this example from a synthesis solver is:
+A possible correct response for this example from a synthesis solver 
+prepends the integer $\syntax{7}$ to all rows of the original table:
 \begin{verbatim}
 (
 (define-fun f ((x (Table String))) (Table Int String) 
@@ -1025,14 +1026,11 @@ \subsection{Table Transformation with Abstract Sorts}
 )
 \end{verbatim}
 
-In particular, this prepends the integer $\syntax{7}$ to all rows of the original table.
-
 Note the use of abstract sorts in this example gives
 greater flexibility for specifications. 
 Although not necessary in this example, the solution
 may involve types that are not explicitly specified in the grammar.
-For example,
-the following solution involves tables with two integer columns and a string column:
+For example:
 \begin{verbatim}
 (
 (define-fun f ((x (Table String))) (Table Int String) 
@@ -1041,6 +1039,7 @@ \subsection{Table Transformation with Abstract Sorts}
     (table.product (bag (tuple 7) 1) x))))
 )
 \end{verbatim}
-It is also a solution to the above problem.
+The above solution involves constructing a table with two integer columns and a string column,
+and is also a valid solution to the above problem.
 
 \end{document}

From 617edea648ccb3cbd11a1a9f3e930a40f4a4e84b Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Apr 2022 10:40:10 -0500
Subject: [PATCH 10/17] Minor

---
 tableTheory/tableTheory.tex | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/tableTheory/tableTheory.tex b/tableTheory/tableTheory.tex
index 704d113..86d43a6 100644
--- a/tableTheory/tableTheory.tex
+++ b/tableTheory/tableTheory.tex
@@ -57,7 +57,7 @@
 
 \title{Proposal for a Theory of Tables}
 
-\author{Andrew Reynolds \and Chenglong Wang}
+\author{Andrew Reynolds \and Chenglong Wang \and Mudathir Mohammed \and Cesare Tinelli}
 
 \maketitle
 
@@ -1011,7 +1011,8 @@ \subsection{Table Transformation with Abstract Sorts}
 \emph{any} table type. However, a term generated by this non-terminal is
 only valid as a solution for $\syntax{f}$ if it has type $\syntax{(Table\ Int\ String)}$,
 the return type of $\syntax{f}$.
-Note that several non-terminals of the above grammar are well-typed only for a subset of the terms they apply to.
+
+Several non-terminals of the above grammar are well-typed only for a subset of the terms they apply to.
 For example, $\syntax{(tuple.select\ StartInt\ Start)}$ is the right hand side of
 a production rule for $\syntax{StartInt}$.
 Thus, it is assumed that this rule is limited to generating terms

From c23743f03d39b4466ddbbcd846f46743485be187 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Apr 2022 10:41:24 -0500
Subject: [PATCH 11/17] Minor

---
 tableTheory/tableTheory.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tableTheory/tableTheory.tex b/tableTheory/tableTheory.tex
index 86d43a6..9c5b1dd 100644
--- a/tableTheory/tableTheory.tex
+++ b/tableTheory/tableTheory.tex
@@ -1015,8 +1015,8 @@ \subsection{Table Transformation with Abstract Sorts}
 Several non-terminals of the above grammar are well-typed only for a subset of the terms they apply to.
 For example, $\syntax{(tuple.select\ StartInt\ Start)}$ is the right hand side of
 a production rule for $\syntax{StartInt}$.
-Thus, it is assumed that this rule is limited to generating terms
-$\syntax{(tuple.select\ n\ s)}$ where $\syntax{s}$ is a table whose $\syntax{n}^{th}$ column is an integer.
+This rule is limited to generating terms
+$\syntax{(tuple.select\ n\ t)}$ where $\syntax{t}$ is a table whose $\syntax{n}^{th}$ column is an integer.
 
 A possible correct response for this example from a synthesis solver 
 prepends the integer $\syntax{7}$ to all rows of the original table:

From bf3c38f15ea93c0232f3e44b4b09fc55d53472b7 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Apr 2022 10:58:39 -0500
Subject: [PATCH 12/17] Fix

---
 tableTheory/tableTheory.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tableTheory/tableTheory.tex b/tableTheory/tableTheory.tex
index 9c5b1dd..8d9baf2 100644
--- a/tableTheory/tableTheory.tex
+++ b/tableTheory/tableTheory.tex
@@ -381,9 +381,9 @@ \subsubsection{Bag Compositions}
 \paragraph{Notes}
 \begin{itemize}
 \item
-The above operators are \emph{chainable}, that is,
-$\syntax{(bag.union_max\ A\ B\ C)}$ is syntax sugar for
-$\syntax{(bag.union_max\ (bag.union_max\ A\ B)\ C)}$.
+The above operators are \emph{left-associative}, that is,
+$\syntax{(bag.union\_max\ A\ B\ C)}$ is syntax sugar for
+$\syntax{(bag.union\_max\ (bag.union\_max\ A\ B)\ C)}$.
 \end{itemize}
 
 \subsubsection{Bag Cardinality}

From 99e55034d39005c75a09ca35b9f35603912ff8b8 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 12 Apr 2022 16:20:05 -0500
Subject: [PATCH 13/17] Fixes

---
 tableTheory/tableTheory.tex | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/tableTheory/tableTheory.tex b/tableTheory/tableTheory.tex
index 8d9baf2..7ca7231 100644
--- a/tableTheory/tableTheory.tex
+++ b/tableTheory/tableTheory.tex
@@ -57,7 +57,7 @@
 
 \title{Proposal for a Theory of Tables}
 
-\author{Andrew Reynolds \and Chenglong Wang \and Mudathir Mohammed \and Cesare Tinelli}
+\author{Andrew Reynolds \and Chenglong Wang \and Mudathir Mohamed \and Cesare Tinelli}
 
 \maketitle
 
@@ -382,8 +382,10 @@ \subsubsection{Bag Compositions}
 \begin{itemize}
 \item
 The above operators are \emph{left-associative}, that is,
-$\syntax{(bag.union\_max\ A\ B\ C)}$ is syntax sugar for
-$\syntax{(bag.union\_max\ (bag.union\_max\ A\ B)\ C)}$.
+$\syntax{(bag.union\_max\ A\ B\ C)}$ is syntax sugar for:
+\begin{align*}
+\syntax{(bag.union\_max\ (bag.union\_max\ A\ B)\ C)}
+\end{align*}
 \end{itemize}
 
 \subsubsection{Bag Cardinality}
@@ -470,7 +472,7 @@ \subsubsection{Bag Map}
 for each $\syntax{u}$ that occurs in $\syntax{t}$.
 The multiplicity of $\syntax{(f\ u)}$
 in $\syntax{(bag.map\ f\ t)}$
-is the same as the multiplicity of $\syntax{u}$ in $\syntax{t}$.
+is at least the multiplicity of $\syntax{u}$ in $\syntax{t}$.
 
 \subsubsection{Bag Fold}
 \label{sec:fold}

From 7b276aac9a1929c8b04a75573d38c1e03579ca5b Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 13 Apr 2022 16:01:18 -0500
Subject: [PATCH 14/17] Update tableTheory/tableTheory.tex

Co-authored-by: mudathirmahgoub <mudathirmahgoub@gmail.com>
---
 tableTheory/tableTheory.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tableTheory/tableTheory.tex b/tableTheory/tableTheory.tex
index 7ca7231..3e9a044 100644
--- a/tableTheory/tableTheory.tex
+++ b/tableTheory/tableTheory.tex
@@ -224,7 +224,7 @@ \subsubsection{Tuple Selection}
   )
 )
 \end{verbatim}
-When $1 \leq n \leq j$,
+When $0 \leq n \leq j-1$,
 the term $\syntax{(tuple.select\ n\ t)}$ is
 interpreted as the $\syntax{n}^{th}$ argument of the tuple $\syntax{t}$.
 When $n$ is out of bounds, e.g. $1 \leq n \leq j$ does not hold,

From b56653997a2ebb6ff8bb2ec9a30f6b72a4facfa4 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 13 Apr 2022 16:16:19 -0500
Subject: [PATCH 15/17] Apply suggestions from code review

Co-authored-by: mudathirmahgoub <mudathirmahgoub@gmail.com>
---
 tableTheory/tableTheory.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tableTheory/tableTheory.tex b/tableTheory/tableTheory.tex
index 3e9a044..b243a5c 100644
--- a/tableTheory/tableTheory.tex
+++ b/tableTheory/tableTheory.tex
@@ -227,7 +227,7 @@ \subsubsection{Tuple Selection}
 When $0 \leq n \leq j-1$,
 the term $\syntax{(tuple.select\ n\ t)}$ is
 interpreted as the $\syntax{n}^{th}$ argument of the tuple $\syntax{t}$.
-When $n$ is out of bounds, e.g. $1 \leq n \leq j$ does not hold,
+When $n$ is out of bounds, e.g. $0 \leq n \leq j-1$ does not hold,
 then the value of $\syntax{(tuple.select\ n\ t)}$ is unspecified.
 
 \paragraph{Notes}
@@ -237,7 +237,7 @@ \subsubsection{Tuple Selection}
 that $\syntax{(tuple.select\ n_1\ t_1)}$ and  $\syntax{(tuple.select\ n_2\ t_2)}$
 must have the same value when $n_1, t_1$ pairwise have the same value as $n_2, t_2$,
 even when $n_1$ and $n_2$ are out of bounds.
-\item When $n$ is a numeral such that $1 \leq n \leq j$,
+\item When $n$ is a numeral such that $0 \leq n \leq j-1$,
 $\syntax{((\_\ tuple.select\ n)\ t)}$ is syntax sugar for the term
 $\syntax{(tuple.select\ n\ t)}$.
 The former may be used to make it is explicit the index to a tuple selector
@@ -292,7 +292,7 @@ \subsubsection{Tuple Projection}
 The function application
 $\syntax{(tuple.project\ t)}$ always returns the empty tuple for any input $t$.
 \item Similar to the indexed syntax for tuple selection,
-when $n_1, \ldots, n_k$ are numerals in the range $[1, j]$,
+when $n_1, \ldots, n_k$ are numerals in the range $[0, j-1]$,
 $\syntax{((\_\ tuple.project\ n_1\ ...\ n_k)\ t)}$ is syntax sugar for the term
 $\syntax{(tuple.project\ n_1\ ...\ n_k\ t)}$.
 \end{itemize}

From e5decd8603c589f09cb89efdd1b60a771eb9b480 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 14 Apr 2022 08:57:14 -0500
Subject: [PATCH 16/17] Apply suggestions from code review

Co-authored-by: mudathirmahgoub <mudathirmahgoub@gmail.com>
---
 tableTheory/tableTheory.tex | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/tableTheory/tableTheory.tex b/tableTheory/tableTheory.tex
index b243a5c..414fbd0 100644
--- a/tableTheory/tableTheory.tex
+++ b/tableTheory/tableTheory.tex
@@ -390,7 +390,7 @@ \subsubsection{Bag Compositions}
 
 \subsubsection{Bag Cardinality}
 The signature $\sigtable$ includes 
-the function symbol $\syntax{card}$ whose sort definition is
+the function symbol $\syntax{bag.card}$ whose sort definition is
 \begin{verbatim}
 (par (X) 
   (bag.card 
@@ -431,8 +431,8 @@ \subsubsection{Bag Filtering}
 
 \paragraph{Semantics}
 The filter operator keeps only the elements
-from its first argument
-for which the predicate of its second argument is true.
+from its second argument
+for which the predicate of its first argument is true.
 In other words,
 $\syntax{(bag.filter\ P\ t)}$
 is the bag containing exactly
@@ -440,7 +440,7 @@ \subsubsection{Bag Filtering}
 such that $\syntax{(P\ u)}$ is true.
 Notice that if $\syntax{(P\ u)}$ is true,
 then $u$ has the same multiplicity in $\syntax{(bag.filter\ P\ t)}$
-as it did in $\syntax{t}$.
+as it did in $\syntax{t}$. Otherwise its multiplicity is zero. 
 
 \subsubsection{Bag Map}
 The signature $\sigtable$ includes 
@@ -464,7 +464,7 @@ \subsubsection{Bag Map}
 
 \paragraph{Semantics}
 The map operator runs the function provided
-in the second argument to all elements in the bag.
+in the first argument to all elements in the bag.
 In other words,
 $\syntax{(bag.map\ f\ t)}$
 is the bag containing exactly
@@ -589,12 +589,12 @@ \subsection{Tables}
 \subsubsection{Table Projection}
 The signature $\sigtable$ includes 
 the functions symbol of the form
-$\syntax{tuple.project}$.
+$\syntax{table.project}$.
 %Note this operator is overloaded,
 %as a separate projection function (of the same name)
 %is also defined for tuples in Section~\ref{sec:tup-project}.
 Its sort definition includes an unbounded number of integer arguments, followed
-by a tuple:
+by a bag of tuples (or a table):
 \begin{verbatim}
 (par (X_1 ... X_j) 
   (table.project
@@ -651,7 +651,7 @@ \subsubsection{Table Projection}
 returns a table with no columns whose cardinality is the same as that of $\syntax{t}$.
 \item
 When $k>0$ and
-$n_1, \ldots, n_k$ are numerals in the range $[1, j]$,
+$n_1, \ldots, n_k$ are numerals in the range $[0, j-1]$,
 $\syntax{((\_\ table.project\ n_1\ ...\ n_k)\ t)}$ is syntax sugar for the term
 $\syntax{(table.project\ n_1\ ...\ n_k\ t)}$.
 \end{itemize}
@@ -744,7 +744,7 @@ \subsubsection{Table Join}
 The cardinality of $\syntax{(table.join\ t_1\ t_2)}$
 is the cardinality of $\syntax{t_1}$ times the cardinality of $\syntax{t_2}$.
 \item
-If $k>0$ and $n_1, \ldots, n_k$ are numerals in the range $[1, j]$ 
+If $k>0$ and $n_1, \ldots, n_k$ are numerals in the range $[0, j-1]$ 
 and $m_1, \ldots, m_k$ are numerals in the range $[1, l]$, then
 $\syntax{((\_\ table.join\ n_1\ m_1\ ...\ n_k\ m_k)\ t_1\ t_2)}$
 is syntax sugar for the term

From 5f2cec4e9511b1d1ef930b92af763b57ccd8140d Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 14 Apr 2022 08:59:34 -0500
Subject: [PATCH 17/17] Fix, generalize

---
 tableTheory/tableTheory.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tableTheory/tableTheory.tex b/tableTheory/tableTheory.tex
index 414fbd0..5de3f6e 100644
--- a/tableTheory/tableTheory.tex
+++ b/tableTheory/tableTheory.tex
@@ -141,7 +141,7 @@ \section{Function Symbols}
 The signature $\sigtable$ includes function symbols for
 lambda abstractions,
 tuples, bags, and
-three function symbols denoting table operations.
+several function symbols denoting table operations.
 We list these in the following.
 Function symbols in its signature may be polymorphic.
 To provide the sort of (classes of) polymorphic functions,
@@ -358,7 +358,7 @@ \subsubsection{Bag Compositions}
 The signature $\sigtable$ includes 
 the binary function symbols 
 $\syntax{bag.union\_max}$, $\syntax{bag.union\_disjoint}$, 
-$\syntax{bag.intersect\_min}$, $\syntax{bag.difference\_subtract}$ and
+$\syntax{bag.inter\_min}$, $\syntax{bag.difference\_subtract}$ and
 $\syntax{bag.difference\_remove}$.
 Each $\syntax{f}$ of the aforementioned operators
 has sort definition:
@@ -370,7 +370,7 @@ \subsubsection{Bag Compositions}
 \begin{verbatim}
 (bag.count x (bag.union_max A B))            = (max (bag.count x A) (bag.count x B))
 (bag.count x (bag.union_disjoint A B))       = (+ (bag.count x A) (bag.count x B))
-(bag.count x (bag.intersect_min A B))        = (min (bag.count x A) (bag.count x B))
+(bag.count x (bag.inter_min A B))            = (min (bag.count x A) (bag.count x B))
 (bag.count x (bag.difference_subtract A B))  = (max (- (bag.count x A) (bag.count x B)) 0)
 (bag.count x (bag.difference_remove A B))    = (ite (> (bag.count x B) 0) 0 (bag.count x A))
 \end{verbatim}