]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/mathql/doc/mathql_operational_core.tex
ocaml 3.09 transition
[helm.git] / helm / mathql / doc / mathql_operational_core.tex
index f9471292bda99135d6cc49aa638063bea94c68c8..e096879bba42f55f705be95811949e3a056a271e 100644 (file)
@@ -1,32 +1,32 @@
-\subsection {The core language}
+\subsection {The core language} \label{OCore}
 
 \subsubsection*{Preliminaries}
 
-Wih the above background we are able to type the main objects needed in the
+With 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
+A path $ p $ 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 $.
+The attribute contents $ V $ are 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
+An attribute group $ G $ is an association set connecting the attribute names
+to their contents, therefore its type is
 $ T_1 = \Setof\ (T_{0a} \times T_{0b}) $. 
 
 \item
-A subject string $ r $ is an object of type $ \Str $.
+A head 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
+An {\av}, {\ie} a head string with its attribute groups, has type
 $ T_3 = \Str \times T_2 $. 
 
 \item
@@ -40,8 +40,7 @@ $ T_5 = \Str \times \Str \times (T_{0a} \to \Str) $.
 
 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}.
-
+according to \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
@@ -53,14 +52,15 @@ 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.
+set variables to {\av} sets, element variables to {\av}'s and element
+variables 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)
+\Setof\ (\GP{svar} \times T_4) \times
+\Setof\ (\GP{evar} \times T_3) \times % $ \\ $ \times\
+\Setof\ (\GP{evar} \times T_1)
 $
 \end{center} \end{footnotesize}
 
@@ -73,7 +73,7 @@ $ \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
+The context components $ \G_s $ and $ \G_e $ are used to store the contents of
 variables, while $ \G_g $ is used by the \TT{ex} operator to be presented
 below.
 
@@ -86,15 +86,15 @@ to an {\av} set.
 
 \subsubsection*{Queries}
 
-The first \GP{query} expressions include explicit {\av} sets and syntactic
-grouping:
+The first group of \GP{query} expressions include the representation of
+explicit {\av} sets and the syntactic grouping facility:
 
 \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
+An explicit {\av} set can be represented either 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
@@ -110,21 +110,21 @@ evaluated using the rules given below.
 \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}
+       (\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 \ssum \cdots \ssum S_m}
 %
 \end{center} 
 \begin{center} 
 %
-\irule{q \in \GP{string} \spc g_1, \cdots, g_m \in \GP{xgroup} \spc
+\irule{q \in \GP{string} \spc g_1, \cdots, g_m \in \GP{xgroup} \icr
        (\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}
+      {(\G, \TT{[} q\ \TT{attr}\ g_1 \TT{,} \cdots \TT{,} g_m \TT{]}) \daq S_1 \ssum \cdots \ssum S_m}
 %
 \end{center} 
 \begin{center} 
 %
-\irule{q \in \GP{string} \spc a_1, \cdots, a_m \in \GP{xatr} \spc
+\irule{q \in \GP{string} \spc a_1, \cdots, a_m \in \GP{xatr} \icr
        (\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}
@@ -139,17 +139,16 @@ evaluated using the rules given below.
 \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.
+$ \dsum $ and $ \ssum $ are helper functions describing the two union
+operations on {\av} sets: with and without attribute distribution respectively.
 
 \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 $ \\ 
+$ (S_1 \sdor \{(r, A_1)\}) \ssum (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
+$ (S_1 \ssum S_2) \sor \{(r, A_1 \sor A_2)\} $ \\
+1b & $ S_1 \ssum 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)\} $ \\
@@ -158,14 +157,14 @@ $ (S_1 \dsum S_2) \sor \{(r, A_1 \distr A_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\} $.
+Rules 1a, 2a override 1b, 2b and
+$ A_1 \distr A_2 = \{G_1 \ssum G_2 \st G_1 \in A_1, G_2 \in A_2\} $.
 
 \item 
-The semantics of \TT{property} operator is described below.
+The semantics of the \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,
+$s$ is ``$ \TT{property}\ h\ p_1\ \TT{main}\ p_2\ \TT{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\}\} $:
 
@@ -173,7 +172,7 @@ $A_2$ is $ \{ \Exp\ P\ p_1\ r_1\ \{e_1, \cdots, e_m\}\} $:
 \begin{center}
 %
 \irule
-{h \oft \GP{refine} \spc p_1, p_2 \oft \GP{path} \spc 
+{h \oft \GP{ref} \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}
@@ -188,12 +187,17 @@ $A_2$ is $ \{ \Exp\ P\ p_1\ r_1\ \{e_1, \cdots, e_m\}\} $:
 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}). 
+the $ h $ flag (this is the primitive function that inspects the {\RDF}
+graph).
 
 $ \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:
+function handling {\POSIX} regular expressions.
+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{In {\POSIX} 1003.1-2001:
+\CURI{http://www.unix-systems.org/version3/ieee\_\,std.html}.}
+regular expression $ \verb+"^"+ \app s \app \TT{"\$"} $.
 
 \begin{footnotesize}
 \begin{center} \begin{tabular}{rll}
@@ -206,31 +210,22 @@ $ \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
+$ \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:
+$ \Exp $ is based on $ \Exp\p $ which handles a single attribute. Formally,
+if $ p, p\p \oft \GP{path} $ and $ E \oft \Setof\ \GP{exp} $:
 
 \begin{footnotesize}
-\begin{center} \begin{tabular}{rlll}
+\begin{center} \begin{tabular}{rll}
 %
 $ 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} $ \\
+$ \{ r_2 \st (r_1, p_1 \app (\Name\ p), r_2) \in P \} $ \\
 $ \Exp\p\ P\ r_1\ p_1\ p $ & rewrites to &
-$ \{ (\Name\ p, f\ P\ r_1\ p_1\ p) \} $ & 
-with $ p \oft \GP{path} $ \\
+$ \{ (\Name\ p, f\ P\ r_1\ p_1\ p) \} $ \\
 $ \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} $ \\
+$ \{ (\Name\ p\p, f\ P\ r_1\ p_1\ p) \} $ \\
 $ \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} $ 
+$ \bigsum \{ \Exp\p\ P\ r_1\ p_1\ e \st e \in E \} $ \\ 
 \end{tabular} \end{center}
 \end{footnotesize}
 
@@ -258,7 +253,7 @@ $ (\lall c \in W)\ \Istrue\p\ P\ r_1\ p_1\ c $
 \end{footnotesize}
 
 For each clause ``\TT{isfalse} $ c_1, \cdots, c_n $'' the set $ P $
-must be replaced with
+must be replaced with \newline
 $ \{ (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.
@@ -269,8 +264,7 @@ $ \{ (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:
+The second group of \GP{query} expressions allows the context manipulation:
 
 \begin{itemize}
 
@@ -280,54 +274,53 @@ 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}\}}
+\irule{i \oft \GP{evar}}{}{(\g, i) \daq \{\get{\G_e}{i}\}}
 %
 \end{center} \end{footnotesize}
 
-$ \get{\G_s}{i} $ and $ \{\get{\G_a}{i}\} $ mean $ \ES $ if $ i $ is not defined.
+$ \get{\G_s}{i} $ and $ \{\get{\G_e}{i}\} $ mean $ \ES $ if $ i $ is not defined.
 
 \item 
-The \TT{let} operator assigns an {\av} set variable (svar):
+The \TT{let} operator assigns a set variable (\GP{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)}
+       ((\set{\G_s}{i}{S_1}, \G_e, \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
+introducing a fresh variable, so ``$ x_1\ \TT{;;}\ x_2 $'' rewrites
 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.
-
+in element variables.
 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
+associated to the {\av}'s in the $ \G_e $ 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
+pool of attribute groups, one for each {\av} in the $ \G_e $ 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}
+\irule{(\lall \D_g \in \All\ \G_e)\ ((\G_s, \G_e, \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\}}{}
+\irule {i \oft \GP{evar} \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}
@@ -335,31 +328,29 @@ context. Formally we have the rules:
 
 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} \} $,
+$ \All\ \G_e = \{\D_g \st \get{\D_g}{i} = G\ \RM{iff}\ G \in \Snd\ \get{\G_e}{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:
+The third group of \GP{query} expressions allows the {\av} set manipulation:
 
 \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.
+according to the setting of the \TT{distr} flag.
 
 \begin{footnotesize} 
 \begin{center}
 %
 \irule
-{h \in \TT{["distr"]?} \spc a \in \GP{xgroups} \spc 
+{h \in \TT{["distr"]?} \spc a \in \GP{xgroups} \icr 
  (\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)\}}
@@ -368,54 +359,58 @@ according to the \TT{distr} flag.
 \begin{center}
 %
 \irule
-{h \in \TT{["distr"]?} \spc i \in \GP{avar} \spc  
+{h \in \TT{["distr"]?} \spc i \in \GP{evar} \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})\}}
+{(\g, \TT{add}\ i\ \TT{in}\ x) \daq \{(r_1, A_1 \jolly \Snd\ \get{\G_e}{i}), \cdots, (r_m, A_m \jolly \Snd\ \get{\G_e}{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.
+Moreover $ \Snd\ \get{\G_e}{i} = \ES $ if $i$ is not defined.
 
 \item
-The semantics of the \TT{for} operator is given in terms of the {\For} helper
+The semantics of the \TT{for} operator is given using 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}}{}
+\irule{i \oft \GP{evar} \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}
+%
+\end{center} 
+\begin{center}
+%
+\irule{i \oft \GP{evar} \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)}
+\irule{i \oft \GP{evar} \spc ((\G_s, \set{\G_e}{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 $.
+Here we have $ R \oft T_3 $, $ \G = \g $, $ \jolly_{\tt"sup"} = \ssum $ and
+$ \jolly_{\tt"inf"} = \sprod $.
 
-$ \dprod $ and $ \prod $ are helper functions describing the two intersection
+$ \dprod $ and $ \sprod $ 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}.   
+They are dual to $ \dsum $ and $ \ssum $. $ \dprod $ does not appear in this
+version of {\MathQL} but was used in the earlier 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 $ \\ 
+$ (S_1 \sdor \{(r, A_1)\}) \sprod (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
+$ (S_1 \sprod S_2) \sor \{(r, A_1 \sor A_2)\} $ \\
+1b & $ S_1 \sprod 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)\} $ \\
@@ -424,7 +419,7 @@ $ (S_1 \dprod S_2) \sor \{(r, A_1 \distr A_2)\} $ \\
 \end{tabular} \end{center}
 \end{footnotesize}
 
-As for $ \sum $ and $ \dsum $, rules 1a, 2a override rules 1b, 2b respectively.
+As for $ \ssum $ and $ \dsum $, rules 1a, 2a override rules 1b, 2b respectively.
 
 \item
 The semantics of the \TT{while} operator is given by the rules below:
@@ -440,20 +435,19 @@ The semantics of the \TT{while} operator is given by the rules below:
 %
 \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_1, x_2) \daq (\G_2, S_2) \icr 
  (\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.
+Again $ \jolly_{\tt"sup"} = \ssum $ and $ \jolly_{\tt"inf"} = \sprod $.
+Rule 1 takes precedence over rule 2.
 
 \end{itemize}
 
-The forth group of \GP{query} constructions make {\MathQL} an extensible
-language.
+The forth group of \GP{query} constructions makes {\MathQL} extensible.
 
 \begin{itemize}
 
@@ -482,7 +476,7 @@ 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 \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
@@ -503,24 +497,21 @@ 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.
+The construction ``\TT{gen} p \TT{in} x'' rewrites to ``\TT{gen} p \verb+{+x\verb+}+''.
 
 \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.
+An \GP{avs} expression (the explicit representation of an {\av} set denoting 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}
+      {x_1 \TT{;} \cdots \TT{;} x_m \dar S_1 \ssum \cdots \ssum S_m}
 %
 \end{center} 
 \begin{center} 
@@ -528,7 +519,7 @@ following rules.
 \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}
+      {q\ \TT{attr}\ g_1 \TT{,} \cdots \TT{,} g_m \dar S_1 \ssum \cdots \ssum S_m}
 %
 \end{center} 
 \begin{center} 
@@ -541,6 +532,13 @@ following rules.
 \end{center} 
 \begin{center} 
 %
+\irule{q, q_0 \in \GP{string} \spc p \in \GP{path}}{}
+      {q\ \TT{attr}\ \{ p = q_0 \} \dar 
+       \{(\Unquote\ q, \{ \{ (\Name\ p, \{ \Unquote\ q_0 \}) \} \})\}}
+%
+\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 \}) \} \})\}}