1 \section {Operational semantics} \label {Operational}
3 This section describes {\MathQL} semantics, that we present in a natural
4 operational style \cite{Lan98,Win93}.
5 Here we use a simple type system that includes basic types such as strings and
6 Booleans, and some type constructors such as product and exponentiation.
7 $ y \oft Y $ will denote a typing judgement.
8 Note that this semantics is not meant as a formal system \emph{per se}, but
9 should serve as a reference for implementors.
11 \subsection {Mathematical background}
13 As a mathematical background for the semantics, we take the one presented in
16 {\Str} denotes the type of strings and its elements are the finite sequences
17 of Unicode \cite{Unicode} characters.
18 Grammatical productions, represented as strings in angle brackets, denote the
19 subtype of {\Str} containing the produced sequences of characters.
21 {\Num} denotes the type of numbers and is the subtype of {\Str} defined by the
22 regular expression: \TT{'0 - 9' [ '0 - 9' ]*}.
23 In this type, numbers are represented by their decimal expansion.
25 $ \Setof\ Y $ denotes the type of finite sets ({\ie} unordered finite
26 sequences without repetitions) over $ Y $.
27 $ \Listof\ Y $ denotes the type of lists ({\ie} ordered finite sequences)
29 We will use the notation $ [y_1, \cdots, y_m] $ for the list whose elements
30 are $ y_1, \cdots, y_m $.
32 {\Boole}, the type of Boolean values, is defined as
33 $ \{\ES, \{("", \ES)\}\} \oft \Setof\ \Setof\ (\Str \times \Setof\ Y) $
34 where the first element stands for \emph{false} (denoted by {\F}) and the
35 second element stands for \emph{true} (denoted by {\T}).
37 $ Y \times Z $ denotes the product of the types $ Y $ and $ Z $ whose elements
38 are the ordered pairs $ (y, z) $ such that $ y \oft Y $ and $ z \oft Z $.
39 The notation is also extended to a ternary product.
41 $ Y \to Z $ denotes the type of functions from $ Y $ to $ Z $ and $ f\ y $
42 denotes the application of $ f \oft Y \to Z $ to $ y \oft Y $.
43 Relations over types, such as equality, are seen as functions to {\Boole}.
45 With the above constructors we can give a formal meaning to most of the
46 standard notation. For instance we will use the following:
51 $ {\ES} \oft (\Setof\ Y) $
54 $ {\lex} \oft ((\Setof\ Y) \to \Boole) \to \Boole $
57 $ {\lall} \oft ((\Setof\ Y) \to \Boole) \to \Boole $
60 $ {\in} \oft Y \to (\Setof\ Y) \to \Boole $ (infix)
63 $ {\sub} \oft (\Setof\ Y) \to (\Setof\ Y) \to \Boole $ (infix)
66 $ {\meet} \oft (\Setof\ Y) \to (\Setof\ Y) \to \Boole $ (infix)
69 $ {\sand} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $ (infix)
72 $ {\sor} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $ (infix)
75 $ {\sdor} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $
76 (the disjoint union, infix)
79 $ \le \oft \Num \to \Num \to \Boole $ (infix)
82 $ < \oft \Num \to \Num \to \Boole $ (infix)
85 $ \# \oft (\Setof\ Y) \to \Num $ (the size operator)
88 $ \app \oft (\Listof\ Y) \to (\Listof\ Y) \to (\Listof\ Y) $
89 (the concatenation, infix)
92 $ \lnot \oft \Boole \to \Boole $
97 Note that $ \lall $ and $ \lex $ are always decidable because the sets are
101 $ U \meet W $ means $ (\lex u \in U)\ u \in W $ and expresses the fact that
102 $ U \sand W $ is inhabited as a primitive notion, {\ie} without mentioning
103 intersection and equality as for $ U \sand W \neq \ES $, which is equivalent
104 but may be implemented less efficiently in real cases%
105 \footnote{As for the Boolean condition $ \a \lor \b $ which may have a more
106 efficient implementation than $ \lnot(\lnot \a \land \lnot \b) $.}.
108 $ U \meet W $ is a natural companion of $ U \sub W $ being its logical dual
109 (recall that $ U \sub W $ means $ (\lall u \in U)\ u \in W $)
110 and is already being used successfully in the context of a constructive
111 ({\ie} intuitionistic and predicative) approach to point-free topology
114 Sets of couples play a central role in our formalization and in particular we
120 $ \Fst \oft (Y \times Z) \to Y $ such that $ \Fst\ (y, z) = y $.
123 $ \Snd \oft (Y \times Z) \to Z $ such that $ \Snd\ (y, z) = z $.
126 $ \Fsts \oft \Setof\ (Y \times Z) \to \Setof\ Z $ such that
127 $ \Fsts\ U = \{\Fst\ u \st u \in U\} $.
130 With the same notation, if $ W $ contains just one couple whose first
131 component is $ y $, then $ \get{W}{y} $ is the second component of that couple.
132 In the other cases $ \get{W}{y} $ is not defined.
133 This operator has type $ (\Setof\ (Y \times Z)) \to Y \to Z $.
136 Moreover $ \set{W}{y}{z} $ is the set obtained from $ W $ removing every
137 couple whose first component is $ y $ and adding the couple $ (y, z) $.
138 The type of this operator is \\
139 $ (\Setof\ (Y \times Z)) \to Y \to Z \to (\Setof\ (Y \times Z)) $.
142 Also $ U + W $ is the union of two sets of couples in the following sense:
145 \begin{center} \begin{tabular}{rll}
147 $ U + \ES $ & rewrites to & $ U $ \\
148 $ U + (W \sdor \{(y, z)\}) $ & rewrites to & $ \set{U}{y}{z} + W $
150 \end{tabular} \end{center}
155 The last three operators are used to read, write and join association sets,
156 which are sets of couples such that the first components of two different
157 elements are always different.
158 These sets will be exploited to formalize the memories appearing in evaluation
161 \subsection {The core language}
163 \subsubsection {Preliminaries}
165 Wih the above background we are able to type the main objects needed in the
171 A path $ s $ is a list of strings therefore its type is
172 $ T_{0a} = \Listof\ \Str $.
175 A multiple string value $ V $ is an object of type $ T_{0b} = \Setof\ \Str $.
178 A attribute group $ G $ is an association set connecting the attribute names
179 to their values, therefore its type is
180 $ T_1 = \Setof\ (T_{0a} \times T_{0b}) $.
183 A subject string $ r $ is an object of type $ \Str $.
186 A set $ A $ of attribute groups is an object of type $ T_2 = \Setof\ T_1 $.
189 An {\av} is a subject string with its attribute groups, so its type is
190 $ T_3 = \Str \times T_2 $.
193 A set $ S $ of {\av}'s is an association set of type $ T_4 = \Setof\ T_3 $.
196 A triple of an attributed relation is of type
197 $ T_5 = \Str \times \Str \times (T_{0a} \to \Str) $.
201 When a constant string appearing in a {\MathQL} expression is unquoted, the
202 surrounding double quotes are deleted and each escaped sequence is translated
203 according \figref{EscTS}.
205 This operation is formally performed by the function
206 $ \Unquote $ of type $ \Str \to \Str $.
207 Moreover $ \Name \oft \GP{path} \to T_{0a} $ is a helper function that
208 converts a linearized path in its structured representation.
209 Formally $ \Name\ (\TT{/}q_1\TT{/} \cdots \TT{/}q_m) $
210 rewrites to $ [\Unquote\ q_1, \cdots, \Unquote\ q_m] $.
212 The semantics of {\MathQL} expressions denoting queries is given by the infix
213 relation $ \daq $ that evaluates a query to an {\av} set.
214 These expressions are evaluated in a context $ \G = \g $
215 which is a triple of association sets that connect
216 svar's to {\av} sets, avar's to {\av}'s and avar's to attribute groups.
217 Therefore the type $ K $ of the context $ \G $ is:
219 \begin{footnotesize} \begin{center}
221 \Setof\ (\GP{svar} \times T_4) \times
222 \Setof\ (\GP{avar} \times T_3)\ \times % $ \\ $ \times\
223 \Setof\ (\GP{avar} \times T_1)
225 \end{center} \end{footnotesize}
228 and the evaluating relation is of the following type:
231 \begin{center} \begin{tabular}{l}
232 $ \mathord{\daq} \oft (K \times \GP{query}) \times (K \times T_4) \to \Boole $.
233 \end{tabular} \end{center}
236 The context components $ \G_s $ and $ \G_a $ are used to store the contents of
237 variables, while $ \G_g $ is used by the \TT{ex} operator to be presented
240 In the following we will write $ (\G, x) \daq S $ to abbreviate
241 $ (\G, x) \daq (\G, S) $.
243 The semantics of {\MathQL} expressions denoting results is given by the infix
244 relation $ \dar \oft \GP{avs} \times T_4 \to \Boole $ that evaluates a result
247 \subsubsection{Queries}
249 The first \GP{query} expressions include explicit {\av} sets and syntactic
255 The syntactic grouping is obtained enclosing a \GP{query} between \TT{(}
257 An explicit {\av} set can be represented by a single string, which is
258 converted into a single {\av} with no attributes, or by a \GP{xavs}
259 (extended {\av} set) expression enclosed between \TT{[} and \TT{]}.
260 Such an expression describes all the components of an {\av} set and is
261 evaluated using the rules given below.
266 \irule{(\G, x) \daq S}{}{(\G, (x)) \daq S} \spc
267 \irule{q \oft \GP{string}}{}{(\G, q) \daq \{(\Unquote\ q, \ES)\}}
272 \irule{x_1, \cdots, x_m \in \GP{xav} \spc
273 (\G, TT{[} x_1 \TT{]}) \daq S_1 \spc \cdots \spc (\G, \TT{[} x_m \TT{]}) \daq S_m}{}
274 {(\G, \TT{[} x_1 \TT{;} \cdots \TT{;} x_m \TT{]}) \daq S_1 \sum \cdots \sum S_m}
279 \irule{q \in \GP{string} \spc g_1, \cdots, g_m \in \GP{xgroup} \spc
280 (\G, \TT{[} q\ \TT{attr}\ g_1 \TT{]}) \daq S_1 \spc \cdots \spc
281 (\G, \TT{[} q\ \TT{attr}\ g_m \TT{]}) \daq S_m}{}
282 {(\G, \TT{[} q\ \TT{attr}\ g_1 \TT{,} \cdots \TT{,} g_m \TT{]}) \daq S_1 \sum \cdots \sum S_m}
287 \irule{q \in \GP{string} \spc a_1, \cdots, a_m \in \GP{xatr} \spc
288 (\G, \TT{[} q\ \TT{attr}\ \{ a_1 \} \TT{]}) \daq S_1 \spc \cdots \spc
289 (\G, \TT{[} q\ \TT{attr}\ \{ a_m \} \TT{]}) \daq S_m}{}
290 {(\G, \TT{[} q\ \TT{attr}\ \{ a_1 \TT{;} \cdots \TT{;} a_m \} \TT{]}) \daq S_1 \dsum \cdots \dsum S_m}
295 \irule{q \in \GP{string} \spc p \in \GP{path} \spc x \daq S}{}
296 {(\G, \TT{[} q\ \TT{attr}\ \{ p = x \} \TT{]}) \daq
297 \{(\Unquote\ q, \{ \{ (\Name\ p, \Fsts\ S) \} \})\}}
302 $ \dsum $ and $ \sum $ are helper functions describing the two union operations
303 on {\av} sets: with and without attribute distribution respectively.
304 $ \dsum $ and $ \sum $ have two rewrite rules each.
307 \begin{center} \begin{tabular}{lrll}
310 $ (S_1 \sdor \{(r, A_1)\}) \sum (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
311 $ (S_1 \sum S_2) \sor \{(r, A_1 \sor A_2)\} $ \\
312 1b & $ S_1 \sum S_2 $ & rewrites to & $ S_1 \sor S_2 $ \\
314 $ (S_1 \sdor \{(r, A_1)\}) \dsum (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
315 $ (S_1 \dsum S_2) \sor \{(r, A_1 \distr A_2)\} $ \\
316 2b & $ S_1 \dsum S_2 $ & rewrites to & $ S_1 \sor S_2 $
318 \end{tabular} \end{center}
321 Rules 1a, 2a override 1b, 2b respectively and
322 $ A_1 \distr A_2 = \{G_1 \sum G_2 \st G_1 \in A_1, G_2 \in A_2\} $.
325 The semantics of \TT{property} operator is described below.
327 In the following rule,
328 $s$ is ``$ \TT{property}\ h\ p_1\ \TT{main}\ p_2\ \RM{attr}\ e_1, \cdots,
329 e_m\ \TT{in}\ k\ x $'', $P$ is $ \Property\ h $ and
330 $A_2$ is $ \{ \Exp\ P\ p_1\ r_1\ \{e_1, \cdots, e_m\}\} $:
336 {h \oft \GP{refine} \spc p_1, p_2 \oft \GP{path} \spc
337 e_1, \cdots, e_m \oft \GP{exp} \spc k \in \TT{["pattern"]?} \spc
340 {(\G, s) \daq \bigsum \{ \{(r_2, A_2)\} \st
341 (\lex r_1 \in \Src\ k\ P\ (\Fsts\ S))\
342 (r_1, p_1 \app p_2, r_2) \in P
348 When the \TT{main} clause is not present, we assume $ p_2 = \TT{/} $.
350 Here $ \Property\ h $ gives the appropriate access relation according to
351 the $ h $ flag (this is the primitive function that inspects the {\RDF} graph,
354 $ \Src\ k\ P\ V $ is a helper function giving the source set
355 according to the $ k $ flag. $ \Src $ is based on $ \Match $, the helper
356 function handling POSIX regular expressions. Formally:
359 \begin{center} \begin{tabular}{rll}
361 $ \Src\ \TT{""}\ P\ V $ & rewrites to & $ V $ \\
362 $ \Src\ \TT{"pattern"}\ P\ V $ & rewrites to &
363 $ \Match\ \{r_1 \st (\lex p, r2)\ (r_1, p, r_2) \in P\} $\ V \\
364 $ \Match\ W\ V $ & rewrites to & $ \bigsor \{\Pattern\ W\ s \st s \in V\} $
366 \end{tabular} \end{center}
369 Here $ \Pattern\ W\ s $ is the primitive function returning the subset of
370 $ W \oft \Setof\ \Str $ whose element match the POSIX 1003.2-1992%
371 \footnote{Included in POSIX 1003.1-2001:
372 \URI{http://www.unix-systems.org/version3/ieee\_\,std.html}.}
373 regular expression $ \verb+"^"+ \app s \app \TT{"\$"} $.
375 $ \Exp\ P\ \p_1\ r_1\ E $ is the helper function that builds the group of
376 attributes specified in the \TT{attr} clause.
377 $ \Exp $ is based on $ \Exp\p $ which handles a single attribute. Formally:
380 \begin{center} \begin{tabular}{rlll}
382 $ f\ P\ r_1\ p_1\ p $ & rewrites to &
383 $ \{ r_2 \st (r_1, p_1 \app (\Name\ p), r_2) \in P \} $ &
384 with $ p \oft \GP{path} $ \\
385 $ \Exp\p\ P\ r_1\ p_1\ p $ & rewrites to &
386 $ \{ (\Name\ p, f\ P\ r_1\ p_1\ p) \} $ &
387 with $ p \oft \GP{path} $ \\
388 $ \Exp\p\ P\ r_1\ p_1\ (p\ \TT{as}\ p\p) $ & rewrites to &
389 $ \{ (\Name\ p\p, f\ P\ r_1\ p_1\ p) \} $ &
390 with $ p, p\p \oft \GP{path} $ \\
391 $ \Exp\ P\ r_1\ p_1\ E $ & rewrites to &
392 $ \bigsum \{ \Exp\p\ P\ r_1\ p_1\ e \st e \in E \} $ &
393 with $ E \oft \Setof\ \GP{exp} $
394 \end{tabular} \end{center}
397 When $ c_1, \cdots, c_n \oft \GP{cons} $ and the clause
398 ``\TT{istrue} $ c_1, \cdots, c_n $'' is present, the set $ P $ must be replaced
399 with $ \{ (r_1, p, r_2) \in P \st \Istrue\ P\ r_1\ p_1\ C \} $
400 where $ C $ is $ \{c_1, \cdots, c_n\} $ and $ \Istrue $ is a helper function
401 that checks the constraints in $ C $.
402 $ \Istrue $ is based on $ \Istrue\p $ that handles a single constraint.
403 Formally, if $ p \oft \GP{path} $ and $ (\G, x) \daq S $:
406 \begin{center} \begin{tabular}{rll}
408 $ g\ P\ p_1\ p $ & rewrites to &
409 $ \{ r_2 \st (\lex r_1)\ (r_1, p_1 \app (\Name\ p), r_2) \in P \} $ \\
410 $ \Istrue\p\ P\ r_1\ p_1\ (p\ \TT{in}\ x) $ & rewrites to &
411 $ (f\ P\ r_1\ p_1\ p) \meet \Fsts\ S $ \\
412 $ \Istrue\p\ P\ r_1\ p_1\ (p\ \TT{match}\ x) $ & rewrites to &
413 $ (f\ P\ r_1\ p_1\ p) \meet \Match\ (g\ P\ p_1\ p)\ (\Fsts\ S) $ \\
414 $ \Istrue\ P\ r_1\ p_1\ C $ & rewrites to &
415 $ (\lall c \in W)\ \Istrue\p\ P\ r_1\ p_1\ c $
417 \end{tabular} \end{center}
420 For each clause ``\TT{isfalse} $ c_1, \cdots, c_n $'' the set $ P $
421 must be replaced with
422 $ \{ (r_1, p, r_2) \in P \st \lnot (\Istrue\ P\ r_1\ p_1\ C) \} $
423 (using the above notation).
424 Note that these substitutions and the former must be composed if necessary.
426 If the \TT{inverse} flag is present, also replace the instances of $ P $ in
427 the rule $A$ and in the definition of $ \Src $ with
428 $ \{ (r_2, p, r_1) \st (r_1, p, r_2) \in P \} $.
432 The second group of \GP{query} expressions includes the context manipulation
438 The operators for reading variables:
440 \begin{footnotesize} \begin{center}
442 \irule{i \oft \GP{svar}}{}{(\g, i) \daq \get{\G_s}{i}} \spc
443 \irule{i \oft \GP{avar}}{}{(\g, i) \daq \{\get{\G_a}{i}\}}
445 \end{center} \end{footnotesize}
447 $ \get{\G_s}{i} $ and $ \{\get{\G_a}{i}\} $ mean $ \ES $ if $ i $ is not defined.
450 The \TT{let} operator assigns an {\av} set variable (svar):
455 \irule{i \oft \GP{svar} \spc (\G_1, x_1) \daq (\g, S_1) \spc
456 ((\set{\G_s}{i}{S_1}, \G_a, \G_g), x_2) \daq (\G_2, S_2)}
457 {}{(\G_1, \TT{let}\ i\ \TT{=}\ x_1\ \TT{in}\ x_2) \daq (\G_2, S_2)}
462 The sequential composition operator \TT{;;} has the semantics of a \TT{let}
463 introducing a fresh variable, so ``$ x_1\ \TT{;;}\ x_2 $'' revrites
464 to ``$ \TT{let}\ i\ \TT{=}\ x_1\ \TT{in}\ x_2 $'' where $i$ does not occur in
468 The \TT{ex} and ``dot'' operators provide a way to read the attributes stored
471 The \TT{ex} (exists) operator gives access to the groups of attributes
472 associated to the {\av}'s in the $ \G_a $ part of the context and does
473 this by loading its $ \G_g $ part, which is used by the ``dot'' operator
476 \TT{ex} is true if the query following it is successful for at least one
477 pool of attribute groups, one for each {\av} in the $ \G_a $ part of the
478 context. Formally we have the rules:
483 \irule{(\lall \D_g \in \All\ \G_a)\ ((\G_s, \G_a, \G_g + \D_g), y) \daq \F}
484 {1}{(\G, \TT{ex}\ y) \daq \F} \spc
485 \irule{\Nop}{2}{(\G, \TT{ex}\ y) \daq \T} \spc
490 \irule {i \oft \GP{avar} \spc p \oft \GP{path} \spc \get{\get{\G_g}{i}}{\Name\ p} = \{s_1, \cdots, s_m\}}{}
491 {(\G, i\TT{.}p) \daq \{(s_1, \ES), \cdots, (s_m, \ES)\}}
497 \footnote{$\D_g$ has the type of $ \G_g $.}
498 $ \All\ \G_a = \{\D_g \st \get{\D_g}{i} = G\ \RM{iff}\ G \in \Snd\ \get{\G_a}{i} \} $,
501 Moreover $ \get{\get{\G_g}{i}}{\Name\ p} $ means $ \ES $
502 if $ i $ or $ \Name\ p $ are not defined where appropriate.
504 Here the first rule has higher precedence than the second one does.
508 The third group of \GP{query} expressions includes the {\av} set manipulation
514 The \TT{add} operator adds a given set of attribute groups to the {\av}'s
515 of an {\av} set using a union with or without attribute distribution
516 according to the \TT{distr} flag.
522 {h \in \TT{["distr"]?} \spc a \in \GP{xgroups} \spc
523 (\G, \TT{[} ""\ \TT{attr}\ a \TT{]}) \daq \{("", A)\} \spc
524 (\G, x) \daq \{(r_1, A_1), \cdots, (r_m, A_m)\}}{}
525 {(\G, \TT{add}\ a\ \TT{in}\ x) \daq \{(r_1, A_1 \jolly A), \cdots, (r_m, A_m \jolly A)\}}
531 {h \in \TT{["distr"]?} \spc i \in \GP{avar} \spc
532 (\g, x) \daq \{(r_1, A_1), \cdots, (r_m, A_m)\}}{}
533 {(\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})\}}
538 Where $ \jolly_{\tt""} = \sor $ and $ \jolly_{\tt"distr"} = \distr $.
539 Moreover $ \Snd\ \get{\G_a}{i} = \ES $ if $i$ is not defined.
542 The semantics of the \TT{for} operator is given in terms of the {\For} helper
548 \irule{i \oft \GP{avar} \spc (\G, x_1) \daq (\G_1, S_1) \spc h \in \TT{["sup"|"inf"]}}
549 {}{(\G, \TT{for}\ i\ \TT{in}\ x_1\ h\ x_2) \daq \For\ h\ \G_1\ i\ x_2\ S_1} \spc
550 \irule{i \oft \GP{avar} \spc x_2 \oft \GP{query}}{}
551 {\For\ h\ \G\ i\ x_2\ \ES\ \RM{rewrites to}\ (\G, \ES)}
556 \irule{i \oft \GP{avar} \spc ((\G_s, \set{\G_a}{i}{R}, \G_g), x_2) \daq (\G_2, S_2)}
557 {}{\For\ h\ \G\ i\ x_2\ (S_1 \sdor \{R\})\ \RM{rewrites to}\
558 (\G_2 ,(\Snd\ (\For\ h\ \G_2\ i\ x_2\ S_1)) \jolly_h S_2)}
563 Here we have $ R \oft T_3 $, $ \G = \g $, $ \jolly_{\tt"sup"} = \sum $ and
564 $ \jolly_{\tt"inf"} = \prod $.
566 $ \dprod $ and $ \prod $ are helper functions describing the two intersection
567 operations on {\av} sets: with and without attribute distribution respectively.
568 They are dual to $ \dsum $ and $ \sum $. $ \dprod $ does not appear in this
569 version of {\MathQL} but was used in the erlier versions
570 \cite{Lor02, GS03, Gui03}.
573 \begin{center} \begin{tabular}{lrll}
576 $ (S_1 \sdor \{(r, A_1)\}) \prod (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
577 $ (S_1 \prod S_2) \sor \{(r, A_1 \sor A_2)\} $ \\
578 1b & $ S_1 \prod S_2 $ & rewrites to & $ \ES $ \\
580 $ (S_1 \sdor \{(r, A_1)\}) \dprod (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
581 $ (S_1 \dprod S_2) \sor \{(r, A_1 \distr A_2)\} $ \\
582 2b & $ S_1 \dprod S_2 $ & rewrites to & $ \ES $
584 \end{tabular} \end{center}
587 As for $ \sum $ and $ \dsum $, rules 1a, 2a override rules 1b, 2b respectively.
590 The semantics of the \TT{while} operator is given by the rules below:
595 \irule{h \in \TT{["sup"|"inf"]} \spc (\G, x_1) \daq (\G_1, \ES)}{1}
596 {(\G, \TT{while}\ x_1\ h\ x_2) \daq (\G_1, \ES)}
602 {h \in \TT{["sup"|"inf"]} \spc (\G, x_1) \daq (\G_1, S_1) \spc
603 (\G_1, x_2) \daq (\G_2, S_2) \spc
604 (\G_2, \TT{while}\ x_1\ h\ x_2) \daq (\G_3, S)}{2}
605 {(\G, \TT{while}\ x_1\ h\ x_2) \daq (\G_3, S_2 \jolly_h S)}
610 Again $ \jolly_{\tt"sup"} = \sum $ and $ \jolly_{\tt"inf"} = \prod $.
611 Moreover rule 1 takes precedence over rule 2.
615 The forth group of \GP{query} constructions make {\MathQL} an extensible
621 The ``function'' construction invokes an external function returning an {\av}
622 set. The function is identified by a \GP{path} and its arguments are a set of
623 \GP{path}'s and a set of \GP{query}'s. It is a mistake to invoke a function
624 with the wrong number of \GP{path}'s and \GP{query}'s as input (each
625 particular function defines these numbers independently).
631 {p, p_1, \cdots, p_m \in \GP{path} \spc x_1, \cdots, x_n \in \GP{query}}{}
632 {(\G, p\ \{p_1 \TT{,} \cdots \TT{,} p_m\}\ \{x_1 \TT{,} \cdots \TT{,} x_m\})
633 \daq \Fun\ p\ [p_1, \cdots, p_m]\ [x_1, \cdots, x_n]\ \G}
638 where $ \Fun \oft \GP{path} \times (\Listof\ \GP{path}) \times (\Listof\
639 \GP{query}) \times K \to T_4 $ is the primitive function performing the
640 low level invocation.
641 The core language does not include any external function and it is a mistake
642 to invoke an undefined function.
645 The \TT{gen} construction invokes an external function returning a \GP{query}
646 The function is identified by a \GP{path} and its arguments are a set of
647 \GP{query}'s. It is a mistake to invoke a function with the wrong number of
648 \GP{query}'s as input (each particular function defines this number
655 {p \in \GP{path} \spc x_1, \cdots, x_n \in \GP{query} \spc
656 (\G, \Gen\ p\ [x_1, \cdots, x_n]\ \G) \daq (\G\p, S)}{}
657 {(\G, \TT{gen}\ p\ \{x_1 \TT{,} \cdots \TT{,} x_m\}) \daq (\G\p, S)}
662 where $ \Gen \oft \GP{path} \times (\Listof\ \GP{query}) \times K \to
663 \GP{query} $ is the primitive function performing the low level invocation.
664 The core language does not include any external function of this kind and it
665 is a mistake to invoke an undefined function.
667 The construction ``\TT{gen} p \TT{in} x'' rewrites to ``\TT{gen} p \{x\}''
668 for the user's convenience.
672 \subsubsection {Results}
674 An \GP{avs} expression ({\ie} the explicit representation of an {\av} set that
675 can denote a query result) is evaluated to an {\av} set according to the
681 \irule{x_1, \cdots, x_m \in \GP{av} \spc
682 x_1 \dar S_1 \spc \cdots \spc x_m \dar S_m}{}
683 {x_1 \TT{;} \cdots \TT{;} x_m \dar S_1 \sum \cdots \sum S_m}
688 \irule{q \in \GP{string} \spc g_1, \cdots, g_m \in \GP{group} \spc
689 q\ \TT{attr}\ g_1 \dar S_1 \spc \cdots \spc
690 q\ \TT{attr}\ g_m \dar S_m}{}
691 {q\ \TT{attr}\ g_1 \TT{,} \cdots \TT{,} g_m \dar S_1 \sum \cdots \sum S_m}
696 \irule{q \in \GP{string} \spc a_1, \cdots, a_m \in \GP{atr} \spc
697 q\ \TT{attr}\ \{ a_1 \} \dar S_1 \spc \cdots \spc
698 q\ \TT{attr}\ \{ a_m \} \dar S_m}{}
699 {(\G, q\ \TT{attr}\ \{ a_1 \TT{;} \cdots \TT{;} a_m \} \dar S_1 \dsum \cdots \dsum S_m}
704 \irule{q, q_1, \cdots, q_m \in \GP{string} \spc p \in \GP{path}}{}
705 {q\ \TT{attr}\ \{ p = \{ q_1 \TT{,} \cdots \TT{,} q_m \} \} \dar
706 \{(\Unquote\ q, \{ \{ (\Name\ p, \{ \Unquote\ q_1, \cdots, \Unquote\ q_m \}) \} \})\}}
712 \subsection {The basic library}