X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql%2Fdoc%2Fmathql_operational.tex;h=a7b3a9a49dcfcef733349d20dac34d854253ea74;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=a1cbe954ab70c4705b33976449a35b6ba8cf6a50;hpb=2542d2235787a5792069343b81d3fd60ffa56c2a;p=helm.git diff --git a/helm/mathql/doc/mathql_operational.tex b/helm/mathql/doc/mathql_operational.tex index a1cbe954a..a7b3a9a49 100644 --- a/helm/mathql/doc/mathql_operational.tex +++ b/helm/mathql/doc/mathql_operational.tex @@ -1,713 +1,14 @@ -\section {Operational semantics} +\section {Operational Semantics} \label {Operational} This section describes {\MathQL} semantics, that we present in a natural operational style \cite{Lan98,Win93}. Here we use a simple type system that includes basic types such as strings and Booleans, and some type constructors such as product and exponentiation. $ y \oft Y $ will denote a typing judgement. -Note that this semantics is not meant as a formal system \emph{per se}, but -should serve as a reference for implementors. +This semantics is not meant as a formal system \emph{per se}, but should be a +reference for implementors. -\subsection {Mathematical background} - -As a mathematical background for the semantics, we take the one presented in -\cite{Gui03}. - -{\Str} denotes the type of strings and its elements are the finite sequences -of Unicode \cite{Unicode} characters. -Grammatical productions, represented as strings in angle brackets, denote the -subtype of {\Str} containing the produced sequences of characters. - -{\Num} denotes the type of numbers and is the subtype of {\Str} defined by the -regular expression: \TT{'0 - 9' [ '0 - 9' ]*}. -In this type, numbers are represented by their decimal expansion. - -$ \Setof\ Y $ denotes the type of finite sets ({\ie} unordered finite -sequences without repetitions) over $ Y $. -$ \Listof\ Y $ denotes the type of lists ({\ie} ordered finite sequences) -over $ Y $. -We will use the notation $ [y_1, \cdots, y_m] $ for the list whose elements -are $ y_1, \cdots, y_m $. - -{\Boole}, the type of Boolean values, is defined as -$ \{\ES, \{("", \ES)\}\} \oft \Setof\ \Setof\ (\Str \times \Setof\ Y) $ -where the first element stands for \emph{false} (denoted by {\F}) and the -second element stands for \emph{true} (denoted by {\T}). - -$ Y \times Z $ denotes the product of the types $ Y $ and $ Z $ whose elements -are the ordered pairs $ (y, z) $ such that $ y \oft Y $ and $ z \oft Z $. -The notation is also extended to a ternary product. - -$ Y \to Z $ denotes the type of functions from $ Y $ to $ Z $ and $ f\ y $ -denotes the application of $ f \oft Y \to Z $ to $ y \oft Y $. -Relations over types, such as equality, are seen as functions to {\Boole}. - -With the above constructors we can give a formal meaning to most of the -standard notation. For instance we will use the following: - -\begin{itemize} - -\item -$ {\ES} \oft (\Setof\ Y) $ - -\item -$ {\lex} \oft ((\Setof\ Y) \to \Boole) \to \Boole $ - -\item -$ {\lall} \oft ((\Setof\ Y) \to \Boole) \to \Boole $ - -\item -$ {\in} \oft Y \to (\Setof\ Y) \to \Boole $ (infix) - -\item -$ {\sub} \oft (\Setof\ Y) \to (\Setof\ Y) \to \Boole $ (infix) - -\item -$ {\meet} \oft (\Setof\ Y) \to (\Setof\ Y) \to \Boole $ (infix) - -%\item -$ {\sand} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $ (infix) - -\item -$ {\sor} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $ (infix) - -\item -$ {\sdor} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $ -(the disjoint union, infix) - -\item -$ \le \oft \Num \to \Num \to \Boole $ (infix) - -\item -$ < \oft \Num \to \Num \to \Boole $ (infix) - -\item -$ \# \oft (\Setof\ Y) \to \Num $ (the size operator) - -\item -$ \app \oft (\Listof\ Y) \to (\Listof\ Y) \to (\Listof\ Y) $ -(the concatenation, infix) - -\item -$ \lnot \oft \Boole \to \Boole $ - -\end{itemize} - -\noindent -Note that $ \lall $ and $ \lex $ are always decidable because the sets are -finite by definition. - -\noindent -$ U \meet W $ means $ (\lex u \in U)\ u \in W $ and expresses the fact that -$ U \sand W $ is inhabited as a primitive notion, {\ie} without mentioning -intersection and equality as for $ U \sand W \neq \ES $, which is equivalent -but may be implemented less efficiently in real cases% -\footnote{As for the Boolean condition $ \a \lor \b $ which may have a more -efficient implementation than $ \lnot(\lnot \a \land \lnot \b) $.}. - -$ U \meet W $ is a natural companion of $ U \sub W $ being its logical dual -(recall that $ U \sub W $ means $ (\lall u \in U)\ u \in W $) -and is already being used successfully in the context of a constructive -({\ie} intuitionistic and predicative) approach to point-free topology -\cite{Sam00}. - -Sets of couples play a central role in our formalization and in particular we -will use: - -\begin{itemize} - -\item -$ \Fst \oft (Y \times Z) \to Y $ such that $ \Fst\ (y, z) = y $. - -\item -$ \Snd \oft (Y \times Z) \to Z $ such that $ \Snd\ (y, z) = z $. - -\item -$ \Fsts \oft \Setof\ (Y \times Z) \to \Setof\ Z $ such that -$ \Fsts\ U = \{\Fst\ u \st u \in U\} $. - -\item -With the same notation, if $ W $ contains just one couple whose first -component is $ y $, then $ \get{W}{y} $ is the second component of that couple. -In the other cases $ \get{W}{y} $ is not defined. -This operator has type $ (\Setof\ (Y \times Z)) \to Y \to Z $. - -\item -Moreover $ \set{W}{y}{z} $ is the set obtained from $ W $ removing every -couple whose first component is $ y $ and adding the couple $ (y, z) $. -The type of this operator is \\ -$ (\Setof\ (Y \times Z)) \to Y \to Z \to (\Setof\ (Y \times Z)) $. - -\item -Also $ U + W $ is the union of two sets of couples in the following sense: - -\begin{footnotesize} -\begin{center} \begin{tabular}{rll} -% -$ U + \ES $ & rewrites to & $ U $ \\ -$ U + (W \sdor \{(y, z)\}) $ & rewrites to & $ \set{U}{y}{z} + W $ -% -\end{tabular} \end{center} -\end{footnotesize} - -\end{itemize} - -The last three operators are used to read, write and join association sets, -which are sets of couples such that the first components of two different -elements are always different. -These sets will be exploited to formalize the memories appearing in evaluation -contexts. - -\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{}). - -$ \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: -\URI{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} - - -\subsection {The basic library} +\input{mathql_operational_background} +\input{mathql_operational_core} +\input{mathql_operational_basic}