[helm.git] / mathql_operational_core.tex

\subsection {The core language}

\subsubsection*{Preliminaries}

Wih the above background we are able to type the main objects needed in the
formalization:

\begin{itemize}

\item
A path $ s $ is a list of strings therefore its type is
$ T_{0a} = \Listof\ \Str $.

\item
A multiple string value $ V $ is an object of type $ T_{0b} = \Setof\ \Str $.

\item
A attribute group $ G $ is an association set connecting the attribute names
to their values, therefore its type is
$ T_1 = \Setof\ (T_{0a} \times T_{0b}) $. 

\item
A subject string $ r $ is an object of type $ \Str $.

\item
A set $ A $ of attribute groups is an object of type $ T_2 = \Setof\ T_1 $.  

\item
An {\av} is a subject string with its attribute groups, so its type is
$ T_3 = \Str \times T_2 $. 

\item
A set $ S $ of {\av}'s is an association set of type $ T_4 = \Setof\ T_3 $.

\item
A triple of an attributed relation is of type
$ T_5 = \Str \times \Str \times (T_{0a} \to \Str) $.

\end{itemize}

When a constant string appearing in a {\MathQL} expression is unquoted, the
surrounding double quotes are deleted and each escaped sequence is translated
according \figref{EscTS}.

This operation is formally performed by the function
$ \Unquote $ of type $ \Str \to \Str $.
Moreover $ \Name \oft \GP{path} \to T_{0a} $ is a helper function that
converts a linearized path in its structured representation.
Formally $ \Name\ (\TT{/}q_1\TT{/} \cdots \TT{/}q_m) $ 
rewrites to $ [\Unquote\ q_1, \cdots, \Unquote\ q_m] $.

The semantics of {\MathQL} expressions denoting queries is given by the infix
relation $ \daq $ that evaluates a query to an {\av} set.
These expressions are evaluated in a context $ \G = \g $
which is a triple of association sets that connect
svar's to {\av} sets, avar's to {\av}'s and avar's to attribute groups.
Therefore the type $ K $ of the context $ \G $ is:

\begin{footnotesize} \begin{center}
$ 
\Setof\ (\GP{svar} \times T_4)  \times
\Setof\ (\GP{avar} \times T_3)\ \times % $ \\ $ \times\
\Setof\ (\GP{avar} \times T_1)
$
\end{center} \end{footnotesize}

\noindent
and the evaluating relation is of the following type:

\begin{footnotesize}
\begin{center} \begin{tabular}{l}
$ \mathord{\daq} \oft (K \times \GP{query}) \times (K \times T_4) \to \Boole $.
\end{tabular} \end{center}
\end{footnotesize}

The context components $ \G_s $ and $ \G_a $ are used to store the contents of
variables, while $ \G_g $ is used by the \TT{ex} operator to be presented
below.

In the following we will write $ (\G, x) \daq S $ to abbreviate
$ (\G, x) \daq (\G, S) $. 

The semantics of {\MathQL} expressions denoting results is given by the infix
relation $ \dar \oft \GP{avs} \times T_4 \to \Boole $ that evaluates a result
to an {\av} set.

\subsubsection*{Queries}

The first \GP{query} expressions include explicit {\av} sets and syntactic
grouping:

\begin{itemize}

\item 
The syntactic grouping is obtained enclosing a \GP{query} between \TT{(}
and \TT{)}.    
An explicit {\av} set can be represented by a single string, which is
converted into a single {\av} with no attributes, or by a \GP{xavs}
(extended {\av} set) expression enclosed between \TT{[} and \TT{]}.
Such an expression describes all the components of an {\av} set and is
evaluated using the rules given below.    

\begin{footnotesize} 
\begin{center} 
%
\irule{(\G, x) \daq S}{}{(\G, (x)) \daq S} \spc
\irule{q \oft \GP{string}}{}{(\G, q) \daq \{(\Unquote\ q, \ES)\}}
%
\end{center} 
\begin{center} 
%
\irule{x_1, \cdots, x_m \in \GP{xav} \spc 
       (\G, TT{[} x_1 \TT{]}) \daq S_1 \spc \cdots \spc (\G, \TT{[} x_m \TT{]}) \daq S_m}{}
      {(\G, \TT{[} x_1 \TT{;} \cdots \TT{;} x_m \TT{]}) \daq S_1 \sum \cdots \sum S_m}
%
\end{center} 
\begin{center} 
%
\irule{q \in \GP{string} \spc g_1, \cdots, g_m \in \GP{xgroup} \spc
       (\G, \TT{[} q\ \TT{attr}\ g_1 \TT{]}) \daq S_1 \spc \cdots \spc
       (\G, \TT{[} q\ \TT{attr}\ g_m \TT{]}) \daq S_m}{}
      {(\G, \TT{[} q\ \TT{attr}\ g_1 \TT{,} \cdots \TT{,} g_m \TT{]}) \daq S_1 \sum \cdots \sum S_m}
%
\end{center} 
\begin{center} 
%
\irule{q \in \GP{string} \spc a_1, \cdots, a_m \in \GP{xatr} \spc
       (\G, \TT{[} q\ \TT{attr}\ \{ a_1 \} \TT{]}) \daq S_1 \spc \cdots \spc
       (\G, \TT{[} q\ \TT{attr}\ \{ a_m \} \TT{]}) \daq S_m}{}
      {(\G, \TT{[} q\ \TT{attr}\ \{ a_1 \TT{;} \cdots \TT{;} a_m \} \TT{]}) \daq S_1 \dsum \cdots \dsum S_m}
%
\end{center} 
\begin{center} 
%
\irule{q \in \GP{string} \spc p \in \GP{path} \spc x \daq S}{}
      {(\G, \TT{[} q\ \TT{attr}\ \{ p = x \} \TT{]}) \daq 
       \{(\Unquote\ q, \{ \{ (\Name\ p, \Fsts\ S) \} \})\}}
%
\end{center} 
\end{footnotesize}

$ \dsum $ and $ \sum $ are helper functions describing the two union operations
on {\av} sets: with and without attribute distribution respectively.
$ \dsum $ and $ \sum $ have two rewrite rules each.

\begin{footnotesize}
\begin{center} \begin{tabular}{lrll}
%
1a &
$ (S_1 \sdor \{(r, A_1)\}) \sum (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
$ (S_1 \sum S_2) \sor \{(r, A_1 \sor A_2)\} $ \\
1b & $ S_1 \sum S_2 $ & rewrites to & $ S_1 \sor S_2 $ \\ 
2a &
$ (S_1 \sdor \{(r, A_1)\}) \dsum (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
$ (S_1 \dsum S_2) \sor \{(r, A_1 \distr A_2)\} $ \\
2b & $ S_1 \dsum S_2 $ & rewrites to & $ S_1 \sor S_2 $
%
\end{tabular} \end{center}
\end{footnotesize}

Rules 1a, 2a override 1b, 2b respectively and
$ A_1 \distr A_2 = \{G_1 \sum G_2 \st G_1 \in A_1, G_2 \in A_2\} $.

\item 
The semantics of \TT{property} operator is described below.

In the following rule,
$s$ is ``$ \TT{property}\ h\ p_1\ \TT{main}\ p_2\ \RM{attr}\ e_1, \cdots,
e_m\ \TT{in}\ k\ x $'', $P$ is $ \Property\ h $ and
$A_2$ is $ \{ \Exp\ P\ p_1\ r_1\ \{e_1, \cdots, e_m\}\} $:

\begin{footnotesize}
\begin{center}
%
\irule
{h \oft \GP{refine} \spc p_1, p_2 \oft \GP{path} \spc 
 e_1, \cdots, e_m \oft \GP{exp} \spc k \in \TT{["pattern"]?} \spc 
 (\G, x) \daq S
}{A}
{(\G, s) \daq \bigsum \{ \{(r_2, A_2)\} \st  
(\lex r_1 \in \Src\ k\ P\ (\Fsts\ S))\ 
(r_1, p_1 \app p_2, r_2) \in P
\}}
%
\end{center}
\end{footnotesize}

When the \TT{main} clause is not present, we assume $ p_2 = \TT{/} $.

Here $ \Property\ h $ gives the appropriate access relation according to
the $ h $ flag (this is the primitive function that inspects the {\RDF} graph,
see \subsecref{HighAccess}). 

$ \Src\ k\ P\ V $ is a helper function giving the source set
according to the $ k $ flag. $ \Src $ is based on $ \Match $, the helper
function handling POSIX regular expressions. Formally:

\begin{footnotesize}
\begin{center} \begin{tabular}{rll}
%
$ \Src\ \TT{""}\ P\ V $ & rewrites to & $ V $ \\
$ \Src\ \TT{"pattern"}\ P\ V $ & rewrites to &
$ \Match\ \{r_1 \st (\lex p, r2)\ (r_1, p, r_2) \in P\} $\ V \\
$ \Match\ W\ V $ & rewrites to & $ \bigsor \{\Pattern\ W\ s \st s \in V\} $
%
\end{tabular} \end{center}
\end{footnotesize}

Here $ \Pattern\ W\ s $ is the primitive function returning the subset of
$ W \oft \Setof\ \Str $ whose element match the POSIX 1003.2-1992%
\footnote{Included in POSIX 1003.1-2001:
\CURI{http://www.unix-systems.org/version3/ieee\_\,std.html}.}
regular expression $ \verb+"^"+ \app s \app \TT{"\$"} $.

$ \Exp\ P\ \p_1\ r_1\ E $ is the helper function that builds the group of
attributes specified in the \TT{attr} clause.
$ \Exp $ is based on $ \Exp\p $ which handles a single attribute. Formally:

\begin{footnotesize}
\begin{center} \begin{tabular}{rlll}
%
$ f\ P\ r_1\ p_1\ p $ & rewrites to &
$ \{ r_2 \st (r_1, p_1 \app (\Name\ p), r_2) \in P \} $ &
with $ p \oft \GP{path} $ \\
$ \Exp\p\ P\ r_1\ p_1\ p $ & rewrites to &
$ \{ (\Name\ p, f\ P\ r_1\ p_1\ p) \} $ & 
with $ p \oft \GP{path} $ \\
$ \Exp\p\ P\ r_1\ p_1\ (p\ \TT{as}\ p\p) $ & rewrites to &
$ \{ (\Name\ p\p, f\ P\ r_1\ p_1\ p) \} $ & 
with $ p, p\p \oft \GP{path} $ \\
$ \Exp\ P\ r_1\ p_1\ E $ & rewrites to &
$ \bigsum \{ \Exp\p\ P\ r_1\ p_1\ e \st e \in E \} $ &
with $ E \oft \Setof\ \GP{exp} $ 
\end{tabular} \end{center}
\end{footnotesize}

When $ c_1, \cdots, c_n \oft \GP{cons} $ and the clause
``\TT{istrue} $ c_1, \cdots, c_n $'' is present, the set $ P $ must be replaced
with $ \{ (r_1, p, r_2) \in P \st \Istrue\ P\ r_1\ p_1\ C \} $
where $ C $ is $ \{c_1, \cdots, c_n\} $ and $ \Istrue $ is a helper function
that checks the constraints in $ C $.
$ \Istrue $ is based on $ \Istrue\p $ that handles a single constraint.
Formally, if $ p \oft \GP{path} $ and $ (\G, x) \daq S $:

\begin{footnotesize}
\begin{center} \begin{tabular}{rll}
%
$ g\ P\ p_1\ p $ & rewrites to &
$ \{ r_2 \st (\lex r_1)\ (r_1, p_1 \app (\Name\ p), r_2) \in P \} $ \\
$ \Istrue\p\ P\ r_1\ p_1\ (p\ \TT{in}\ x) $ & rewrites to &
$ (f\ P\ r_1\ p_1\ p) \meet \Fsts\ S $ \\
$ \Istrue\p\ P\ r_1\ p_1\ (p\ \TT{match}\ x) $ & rewrites to &
$ (f\ P\ r_1\ p_1\ p) \meet \Match\ (g\ P\ p_1\ p)\ (\Fsts\ S) $ \\
$ \Istrue\ P\ r_1\ p_1\ C $ & rewrites to &
$ (\lall c \in W)\ \Istrue\p\ P\ r_1\ p_1\ c $
%
\end{tabular} \end{center}
\end{footnotesize}

For each clause ``\TT{isfalse} $ c_1, \cdots, c_n $'' the set $ P $
must be replaced with
$ \{ (r_1, p, r_2) \in P \st \lnot (\Istrue\ P\ r_1\ p_1\ C) \} $
(using the above notation).
Note that these substitutions and the former must be composed if necessary.

If the \TT{inverse} flag is present, also replace the instances of $ P $ in
the rule $A$ and in the definition of $ \Src $ with
$ \{ (r_2, p, r_1) \st (r_1, p, r_2) \in P \} $.

\end{itemize}

The second group of \GP{query} expressions includes the context manipulation
facilities:

\begin{itemize}

\item
The operators for reading variables:

\begin{footnotesize} \begin{center}
%
\irule{i \oft \GP{svar}}{}{(\g, i) \daq \get{\G_s}{i}} \spc
\irule{i \oft \GP{avar}}{}{(\g, i) \daq \{\get{\G_a}{i}\}}
%
\end{center} \end{footnotesize}

$ \get{\G_s}{i} $ and $ \{\get{\G_a}{i}\} $ mean $ \ES $ if $ i $ is not defined.

\item 
The \TT{let} operator assigns an {\av} set variable (svar):

\begin{footnotesize} 
\begin{center}
%
\irule{i \oft \GP{svar} \spc (\G_1, x_1) \daq (\g, S_1) \spc
       ((\set{\G_s}{i}{S_1}, \G_a, \G_g), x_2) \daq (\G_2, S_2)}
{}{(\G_1, \TT{let}\ i\ \TT{=}\ x_1\ \TT{in}\ x_2) \daq (\G_2, S_2)} 
%
\end{center} 
\end{footnotesize}

The sequential composition operator \TT{;;} has the semantics of a \TT{let}
introducing a fresh variable, so ``$ x_1\ \TT{;;}\ x_2 $'' revrites
to ``$ \TT{let}\ i\ \TT{=}\ x_1\ \TT{in}\ x_2 $'' where $i$ does not occur in
$x_2$.

\item 
The \TT{ex} and ``dot'' operators provide a way to read the attributes stored
in avar's.

The \TT{ex} (exists) operator gives access to the groups of attributes
associated to the {\av}'s in the $ \G_a $ part of the context and does
this by loading its $ \G_g $ part, which is used by the ``dot'' operator
described below. 

\TT{ex} is true if the query following it is successful for at least one
pool of attribute groups, one for each {\av} in the $ \G_a $ part of the
context. Formally we have the rules:

\begin{footnotesize}
\begin{center}
%
\irule{(\lall \D_g \in \All\ \G_a)\ ((\G_s, \G_a, \G_g + \D_g), y) \daq \F}
      {1}{(\G, \TT{ex}\ y) \daq \F} \spc
\irule{\Nop}{2}{(\G, \TT{ex}\ y) \daq \T} \spc
%
\end{center}
\begin{center}
%
\irule {i \oft \GP{avar} \spc p \oft \GP{path} \spc \get{\get{\G_g}{i}}{\Name\ p} = \{s_1, \cdots, s_m\}}{}
       {(\G, i\TT{.}p) \daq \{(s_1, \ES), \cdots, (s_m, \ES)\}}
%
\end{center}
\end{footnotesize}

where%
\footnote{$\D_g$ has the type of $ \G_g $.}
$ \All\ \G_a = \{\D_g \st \get{\D_g}{i} = G\ \RM{iff}\ G \in \Snd\ \get{\G_a}{i} \} $,
and $ \G = \g $.

Moreover $ \get{\get{\G_g}{i}}{\Name\ p} $ means $ \ES $
if $ i $ or $ \Name\ p $ are not defined where appropriate.

Here the first rule has higher precedence than the second one does.

\end{itemize}

The third group of \GP{query} expressions includes the {\av} set manipulation
facilities:

\begin{itemize}

\item
The \TT{add} operator adds a given set of attribute groups to the {\av}'s
of an {\av} set using a union with or without attribute distribution
according to the \TT{distr} flag.

\begin{footnotesize} 
\begin{center}
%
\irule
{h \in \TT{["distr"]?} \spc a \in \GP{xgroups} \spc 
 (\G, \TT{[} ""\ \TT{attr}\ a \TT{]}) \daq \{("", A)\} \spc 
 (\G, x) \daq \{(r_1, A_1), \cdots, (r_m, A_m)\}}{}
{(\G, \TT{add}\ a\ \TT{in}\ x) \daq \{(r_1, A_1 \jolly A), \cdots, (r_m, A_m \jolly A)\}}
%
\end{center}
\begin{center}
%
\irule
{h \in \TT{["distr"]?} \spc i \in \GP{avar} \spc  
 (\g, x) \daq \{(r_1, A_1), \cdots, (r_m, A_m)\}}{}
{(\g, \TT{add}\ i\ \TT{in}\ x) \daq \{(r_1, A_1 \jolly \Snd\ \get{\G_a}{i}), \cdots, (r_m, A_m \jolly \Snd\ \get{\G_a}{i})\}}
%
\end{center}
\end{footnotesize}

Where $ \jolly_{\tt""} = \sor $ and $ \jolly_{\tt"distr"} = \distr $.
Moreover $ \Snd\ \get{\G_a}{i} = \ES $ if $i$ is not defined.

\item
The semantics of the \TT{for} operator is given in terms of the {\For} helper
function:

\begin{footnotesize}
\begin{center}
%
\irule{i \oft \GP{avar} \spc (\G, x_1) \daq (\G_1, S_1) \spc h \in \TT{["sup"|"inf"]}}
{}{(\G, \TT{for}\ i\ \TT{in}\ x_1\ h\ x_2) \daq \For\ h\ \G_1\ i\ x_2\ S_1} \spc
\irule{i \oft \GP{avar} \spc x_2 \oft \GP{query}}{}
      {\For\ h\ \G\ i\ x_2\ \ES\ \RM{rewrites to}\ (\G, \ES)}
%
\end{center} 
\begin{center}
%
\irule{i \oft \GP{avar} \spc ((\G_s, \set{\G_a}{i}{R}, \G_g), x_2) \daq (\G_2, S_2)}
      {}{\For\ h\ \G\ i\ x_2\ (S_1 \sdor \{R\})\ \RM{rewrites to}\
      (\G_2 ,(\Snd\ (\For\ h\ \G_2\ i\ x_2\ S_1)) \jolly_h S_2)} 
%
\end{center}
\end{footnotesize}

Here we have $ R \oft T_3 $, $ \G = \g $, $ \jolly_{\tt"sup"} = \sum $ and
$ \jolly_{\tt"inf"} = \prod $.

$ \dprod $ and $ \prod $ are helper functions describing the two intersection
operations on {\av} sets: with and without attribute distribution respectively.
They are dual to $ \dsum $ and $ \sum $. $ \dprod $ does not appear in this
version of {\MathQL} but was used in the erlier versions 
\cite{Lor02, GS03, Gui03}.   

\begin{footnotesize}
\begin{center} \begin{tabular}{lrll}
%
1a &
$ (S_1 \sdor \{(r, A_1)\}) \prod (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
$ (S_1 \prod S_2) \sor \{(r, A_1 \sor A_2)\} $ \\
1b & $ S_1 \prod S_2 $ & rewrites to & $ \ES $ \\ 
2a &
$ (S_1 \sdor \{(r, A_1)\}) \dprod (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
$ (S_1 \dprod S_2) \sor \{(r, A_1 \distr A_2)\} $ \\
2b & $ S_1 \dprod S_2 $ & rewrites to & $ \ES $
%
\end{tabular} \end{center}
\end{footnotesize}

As for $ \sum $ and $ \dsum $, rules 1a, 2a override rules 1b, 2b respectively.

\item
The semantics of the \TT{while} operator is given by the rules below:

\begin{footnotesize}
\begin{center}
%
\irule{h \in \TT{["sup"|"inf"]} \spc (\G, x_1) \daq (\G_1, \ES)}{1}
{(\G, \TT{while}\ x_1\ h\ x_2) \daq (\G_1, \ES)}
%
\end{center} 
\begin{center}
%
\irule
{h \in \TT{["sup"|"inf"]} \spc (\G, x_1) \daq (\G_1, S_1) \spc
 (\G_1, x_2) \daq (\G_2, S_2) \spc 
 (\G_2, \TT{while}\ x_1\ h\ x_2) \daq (\G_3, S)}{2}
{(\G, \TT{while}\ x_1\ h\ x_2) \daq (\G_3, S_2 \jolly_h S)}
%
\end{center} 
\end{footnotesize}

Again $ \jolly_{\tt"sup"} = \sum $ and $ \jolly_{\tt"inf"} = \prod $.
Moreover rule 1 takes precedence over rule 2.

\end{itemize}

The forth group of \GP{query} constructions make {\MathQL} an extensible
language.

\begin{itemize}

\item
The ``function'' construction invokes an external function returning an {\av}
set. The function is identified by a \GP{path} and its arguments are a set of 
\GP{path}'s and a set of \GP{query}'s. It is a mistake to invoke a function
with the wrong number of \GP{path}'s and \GP{query}'s as input (each
particular function defines these numbers independently).

\begin{footnotesize}
\begin{center}
%
\irule
{p, p_1, \cdots, p_m \in \GP{path} \spc x_1, \cdots, x_n \in \GP{query}}{}
{(\G, p\ \{p_1 \TT{,} \cdots \TT{,} p_m\}\ \{x_1 \TT{,} \cdots \TT{,} x_m\})
 \daq \Fun\ p\ [p_1, \cdots, p_m]\ [x_1, \cdots, x_n]\ \G} 
%
\end{center} 
\end{footnotesize}

where $ \Fun \oft \GP{path} \times (\Listof\ \GP{path}) \times (\Listof\
\GP{query}) \times K \to T_4 $ is the primitive function performing the
low level invocation. 
The core language does not include any external function and it is a mistake
to invoke an undefined function.

\item
The \TT{gen} construction invokes an external function returning a \GP{query}
The function is identified by a \GP{path} and its arguments are a set of 
\GP{query}'s. It is a mistake to invoke a function with the wrong number of
\GP{query}'s as input (each particular function defines this number
independently).

\begin{footnotesize}
\begin{center}
%
\irule
{p \in \GP{path} \spc x_1, \cdots, x_n \in \GP{query} \spc 
 (\G, \Gen\ p\ [x_1, \cdots, x_n]\ \G) \daq (\G\p, S)}{}
{(\G, \TT{gen}\ p\ \{x_1 \TT{,} \cdots \TT{,} x_m\}) \daq (\G\p, S)} 
%
\end{center} 
\end{footnotesize}

where $ \Gen \oft \GP{path} \times (\Listof\ \GP{query}) \times K \to
\GP{query} $ is the primitive function performing the low level invocation. 
The core language does not include any external function of this kind and it
is a mistake to invoke an undefined function.

The construction ``\TT{gen} p \TT{in} x'' rewrites to ``\TT{gen} p \{x\}''
for the user's convenience.

\end{itemize}

\subsubsection*{Results}

An \GP{avs} expression ({\ie} the explicit representation of an {\av} set that
can denote a query result) is evaluated to an {\av} set according to the
following rules.

\begin{footnotesize}
\begin{center} 
%
\irule{x_1, \cdots, x_m \in \GP{av} \spc 
       x_1 \dar S_1 \spc \cdots \spc x_m \dar S_m}{}
      {x_1 \TT{;} \cdots \TT{;} x_m \dar S_1 \sum \cdots \sum S_m}
%
\end{center} 
\begin{center} 
%
\irule{q \in \GP{string} \spc g_1, \cdots, g_m \in \GP{group} \spc
       q\ \TT{attr}\ g_1 \dar S_1 \spc \cdots \spc
       q\ \TT{attr}\ g_m \dar S_m}{}
      {q\ \TT{attr}\ g_1 \TT{,} \cdots \TT{,} g_m \dar S_1 \sum \cdots \sum S_m}
%
\end{center} 
\begin{center} 
%
\irule{q \in \GP{string} \spc a_1, \cdots, a_m \in \GP{atr} \spc
       q\ \TT{attr}\ \{ a_1 \} \dar S_1 \spc \cdots \spc
       q\ \TT{attr}\ \{ a_m \} \dar S_m}{}
      {(\G, q\ \TT{attr}\ \{ a_1 \TT{;} \cdots \TT{;} a_m \} \dar S_1 \dsum \cdots \dsum S_m}
%
\end{center} 
\begin{center} 
%
\irule{q, q_1, \cdots, q_m \in \GP{string} \spc p \in \GP{path}}{}
      {q\ \TT{attr}\ \{ p = \{ q_1 \TT{,} \cdots \TT{,} q_m \} \} \dar 
       \{(\Unquote\ q, \{ \{ (\Name\ p, \{ \Unquote\ q_1, \cdots, \Unquote\ q_m \}) \} \})\}}
%
\end{center} 
\end{footnotesize}