helm/mathql/doc/mathql_operational_basic.tex

   1 \subsection {The basic library}
   2
   3 In this section we present the functions provided by the {\MathQL}.4 basic
   4 library. Describing the whole library would require an amount of space that
   5 goes beyond the limits of this paper so we include here just a selection of
   6 the available functions (the ones for which we gave the syntax extension in
   7 \secref{Textual}).
   8
   9 The function below are grouped by their arity.
  10
  11 \begin{itemize}
  12
  13 \item
  14 \textbf{The predefined {\av} sets.}
  15 The functions \TT{/"empty"}, \TT{/"false"} and \newline \TT{/"true"} take no
  16 path arguments and no set arguments.
  17
  18 \begin{footnotesize}
  19 \begin{center}
  20 %
  21 \irule{\Nop}{}{\Fun\ \TT{/"empty"}\ [\,]\ [\,]\ \G \equiv \F} \spc
  22 \irule{\Nop}{}{\Fun\ \TT{/"false"}\ [\,]\ [\,]\ \G \equiv \F}
  23 \end{center}
  24 \begin{center}
  25 %
  26 \irule{\Nop}{}{\Fun\ \TT{/"true"}\ [\,]\ [\,]\ \G \equiv \T}
  27 %
  28 \end{center}
  29 \end{footnotesize}
  30
  31 Moreover ``\TT{empty}'' rewrites to ``\verb+fun /"empty" {} {}+'',
  32 ``\TT{false}'' rewrites to ``\verb+fun /"false" {} {}+'' and
  33 ``\TT{true}'' rewrites to ``\verb+fun /"true" {} {}+''.
  34
  35 \item
  36 \textbf{Boolean negation and size.}
  37 The functions \TT{/"not"} and \TT{/"count"} take no path arguments and one set
  38 argument.
  39 Here Rule 1 overrides rule 2.
  40
  41 \begin{footnotesize}
  42 \begin{center}
  43 %
  44 \irule{(\G, x) \daq \F}{1}{\Fun\ \TT{/"not"}\ [\,]\ [x]\ \G \equiv \T} \spc
  45 \irule{(\G, x) \daq S}{2}{\Fun\ \TT{/"not"}\ [\,]\ [x]\ \G \equiv \F}
  46 \end{center}
  47 \begin{center}
  48 %
  49 \irule{(\G, x) \daq S}{}{\Fun\ \TT{/"count"}\ [\,]\ [x]\ \G \equiv \#\ S}
  50 %
  51 \end{center}
  52 \end{footnotesize}
  53
  54 Moreover ``\TT{not} x'' rewrites to ``\verb+fun /"not" {} {+x\verb+}+''
  55 and ``\TT{count} x'' rewrites to ``\verb+fun /"count" {} {+x\verb+}+''.
  56
  57 \item
  58 \textbf{Boolean xor, set-theoretic and numerical tests, difference.}
  59 \TT{/"xor"}, \TT{/"sub"}, \TT{/"meet"}, \TT{/"eq"}, \TT{/"le"}, \TT{/"lt"} and
  60 \TT{/"diff"} take no path arguments and two set arguments.
  61 The rule with the lowest number is applied first.
  62
  63 \begin{footnotesize}
  64 \begin{center}
  65 %
  66 \irule{(\G, x_1) \daq \F \spc (\G, x_2) \daq \F}{1}
  67       {\Fun\ \TT{/"xor"}\ [\,]\ [x_1, x_2]\ \G \equiv \T} \spc
  68 \irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq \F}{2}
  69       {\Fun\ \TT{/"xor"}\ [\,]\ [x_1, x_2]\ \G \equiv S_1}
  70 %
  71 \end{center}
  72 \begin{center}
  73 %
  74 \irule{(\G, x_1) \daq \F \spc (\G, x_2) \daq S_2}{3}
  75       {\Fun\ \TT{/"xor"}\ [\,]\ [x_1, x_2]\ \G \equiv S_2} \spc
  76 \irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq S_2}{4}
  77       {\Fun\ \TT{/"xor"}\ [\,]\ [x_1, x_2]\ \G \equiv \F}
  78 %
  79 \end{center}
  80 \begin{center}
  81 %
  82 \irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq S_2}{}
  83       {\Fun\ \TT{/"sub"}\ [\,]\ [x_1, x_2]\ \G \equiv (\Fsts\ S_1 \sub \Fsts\ S_2)}
  84 %
  85 \end{center}
  86 \begin{center}
  87 %
  88 \irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq S_2}{}
  89       {\Fun\ \TT{/"meet"}\ [\,]\ [x_1, x_2]\ \G \equiv (\Fsts\ S_1 \meet \Fsts\ S_2)}
  90 %
  91 \end{center}
  92 \begin{center}
  93 %
  94 \irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq S_2}{}
  95       {\Fun\ \TT{/"eq"}\ [\,]\ [x_1, x_2]\ \G \equiv (\Fsts\ S_1 = \Fsts\ S_2)}
  96 %
  97 \end{center}
  98 \begin{center}
  99 %
 100 \irule{(\G, x_1) \daq \{(r_1, A_1)\} \spc (\G, x_2) \daq \{(r_2, A_2)\}}{}
 101       {\Fun\ \TT{/"le"}\ [\,]\ [x_1, x_2]\ \G \equiv (r_1 \le r_2)}
 102 %
 103 \end{center}
 104 \begin{center}
 105 %
 106 \irule{(\G, x_1) \daq \{(r_1, A_1)\} \spc (\G, x_2) \daq \{(r_2, A_2)\}}{}
 107       {\Fun\ \TT{/"lt"}\ [\,]\ [x_1, x_2]\ \G \equiv (r_1 < r_2)}
 108 %
 109 \end{center}
 110 \begin{center}
 111 %
 112 \irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq S_2}{}
 113       {\Fun\ \TT{/"eq"}\ [\,]\ [x_1, x_2]\ \G \equiv (S_1 \sdiff S_2)}
 114 %
 115 \end{center}
 116 \end{footnotesize}
 117
 118 where $\sdiff$ is a helper function two rewrite rules:
 119
 120 \begin{footnotesize}
 121 \begin{center} \begin{tabular}{lrll}
 122 5 &
 123 $ (S_1 \sdor \{(r, A_1)\}) \sdiff (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
 124 $ S_1 \sdiff S_2 $ \\
 125 6 & $ S_1 \sdiff S_2 $ & rewrites to & $ S_1 $
 126 %
 127 \end{tabular} \end{center}
 128 \end{footnotesize}
 129
 130 ``x \TT{xor} y'' rewrites to ``\verb+fun /"xor" {} {+x\TT{,}y\verb+}+'',
 131 ``x \TT{sub} y'' rewrites to \newline ``\verb+fun /"sub" {} {+x\TT{,}y\verb+}+'',
 132 ``x \TT{meet} y'' rewrites to ``\verb+fun /"meet" {} {+x\TT{,}y\verb+}+'',
 133 ``x \TT{eq} y'' rewrites to ``\verb+fun /"eq" {} {+x\TT{,}y\verb+}+'',
 134 ``x \TT{le} y'' rewrites to \newline ``\verb+fun /"le" {} {+x\TT{,}y\verb+}+'',
 135 ``x \TT{lt} y'' rewrites to ``\verb+fun /"lt" {} {+x\TT{,}y\verb+}+'' and
 136 ``x \TT{diff} y'' rewrites to ``\verb+fun /"diff" {} {+x\TT{,}y\verb+}+''
 137
 138 \item
 139 \textbf{Conditional operator and standard \emph{select} clause}.
 140 \TT{/"if"} takes no path arguments and three set arguments.
 141 The usual rule overriding policy applies.
 142
 143 \begin{footnotesize}
 144 \begin{center}
 145 %
 146 \irule{(\G, x_1) \daq \F \spc (\G, x_3) \daq S_3}{1}
 147       {\Fun\ \TT{/"if"}\ [\,]\ [x_1, x_2, x_2]\ \G \equiv S_3} \spc
 148 \irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq S_2}{2}
 149       {\Fun\ \TT{/"if"}\ [\,]\ [x_1, x_2, x_2]\ \G \equiv S_2}
 150 %
 151 \end{center}
 152 \end{footnotesize}
 153
 154 ``\TT{if} x \TT{then} y \TT{else} z'' rewrites to
 155 ``\verb+fun /"if" {} {+x\TT{,}y\TT{,}z\verb+}+'' and
 156 ``\TT{select} i \TT{from} x \TT{where} y'' rewrites to
 157 ``\TT{for} i \TT{in} x \TT{sup} \TT{if} y \TT{then} i \TT{else} \TT{empty}''.
 158
 159 \item
 160 \textbf{Intersection without attribute distribution.}
 161 \TT{/"intersect"} takes no path arguments and any positive number of set
 162 arguments.
 163
 164 \begin{footnotesize}
 165 \begin{center}
 166 %
 167 \irule{(\G, x_1) \daq S_1 \spc \cdots \spc (\G, x_m) \daq S_m}{}
 168       {\Fun\ \TT{/"intersect"}\ [\,]\ [x_1, \cdots, x_m]\ \G \equiv
 169        (S_1 \sprod \cdots \sprod S_m)}
 170 %
 171 \end{center}
 172 \end{footnotesize}
 173
 174 As usual
 175 ``x \TT{intersect} y'' rewrites to ``\verb+fun /"intersect" {} {+x\TT{,}y\verb+}+''.
 176
 177 \item
 178 \textbf{Union without attribute distribution, Boolean conjunction and
 179 disjunction.}
 180 \TT{/"union"}, \TT{/"and"} and \TT{/"or"} take no path arguments and any
 181 number of set arguments.
 182 The usual rule overriding policy applies.
 183
 184 \begin{footnotesize}
 185 \begin{center}
 186 %
 187 \irule{\Nop}{}{\Fun\ \TT{/"union"}\ [\,]\ [\,]\ \G \equiv \F} \spc
 188 \irule{(\G, x_1) \daq S_1 \spc \cdots \spc (\G, x_m) \daq S_m}{}
 189       {\Fun\ \TT{/"union"}\ [\,]\ [x_1, \cdots, x_m]\ \G \equiv
 190        (S_1 \ssum \cdots \ssum S_m)}
 191 %
 192 \end{center}
 193 \begin{center}
 194 %
 195 \irule{\Nop}{}{\Fun\ \TT{/"and"}\ [\,]\ [\,]\ \G \equiv \T} \spc
 196 \irule{\Nop}{}{\Fun\ \TT{/"or"}\ [\,]\ [\,]\ \G \equiv \F}
 197 %
 198 \end{center}
 199 \begin{center}
 200 %
 201 \irule{\Fun\ \TT{/"and"}\ [\,]\ l\ \G \equiv \F}{1}
 202       {\Fun\ \TT{/"and"}\ [\,]\ (l \app [x])\ \G \equiv \F} \spc
 203 \irule{\Fun\ \TT{/"or"}\ [\,]\ l\ \G \equiv \F \spc (\G, x) \daq S}{3}
 204       {\Fun\ \TT{/"or"}\ [\,]\ (l \app [x])\ \G \equiv S}
 205 %
 206 \end{center}
 207 \begin{center}
 208 %
 209 \irule{\Fun\ \TT{/"and"}\ [\,]\ l\ \G \equiv S_l \spc (\G, x) \daq S}{2}
 210       {\Fun\ \TT{/"and"}\ [\,]\ (l \app [x])\ \G \equiv S} \spc
 211 \irule{\Fun\ \TT{/"or"}\ [\,]\ l\ \G \equiv S_l}{4}
 212       {\Fun\ \TT{/"or"}\ [\,]\ (l \app [x])\ \G \equiv S_l}
 213 \end{center}
 214 \end{footnotesize}
 215
 216 ``x \TT{and} y'' rewrites to ``\verb+fun /"and" {} {+x\TT{,}y\verb+}+'',
 217 ``x \TT{or} y'' rewrites to \newline ``\verb+fun /"or" {} {+x\TT{,}y\verb+}+'',
 218 ``x \TT{union} y'' rewrites to \kern-1.1pt ``\verb+fun /"union" {} {+x\TT{,}y\verb+}+''
 219 and ``\verb+{+x$_1$\TT{,}$\cdots$\TT{,}x$_m$\verb+}+'' rewrites to
 220 ``\verb+fun /"union" {} {+x$_1$\TT{,}$\cdots$\TT{,}x$_m$\verb+}+''.
 221
 222 \item
 223 \textbf{Projection.}
 224 \TT{/"proj"} takes one path argument and one set argument.
 225
 226 \begin{footnotesize}
 227 \begin{center}
 228 %
 229 \irule {p \oft \TT{<path>} \spc
 230         (\G, x) \daq \{ (r_1, A_1), \cdots, (r_m, A_m) \}}{}
 231        {\Fun\ \TT{/"proj"}\ [p]\ [x]\ \G \equiv
 232         \Head\ (\Proj\ (\Name\ p)\ A_1 \sor \cdots \sor \Proj\ (\Name\ p)\ A_m)}
 233 %
 234 \end{center}
 235 \begin{center} \begin{tabular}{rll}
 236 %
 237 $ \Proj\ p\ \{G_1, \cdots, G_n\} $ & rewrites to &
 238 $ \get{G_1}{p} \sor \cdots \sor \get{G_n}{p} $ \\
 239 $ \Head\ \{s_1, \cdots, s_k\} $ & rewrites to & $ \{ (s_1, \ES), \cdots, (s_k, \ES) \} $
 240 \end{tabular} \end{center}
 241 \end{footnotesize}
 242
 243 where, for each $ 1 \le j \le n $, $ \get{G_j}{p} $ is $ \ES $ if $ p $ is not
 244 defined in $ G_j $.
 245
 246 Moreover
 247 ``\TT{proj} p \TT{of} x'' rewrites to ``\verb+fun /"proj" {+p\verb+} {+x\verb+}+''.
 248
 249 \item
 250 \textbf{Refinement.}
 251 The functions \TT{/"keep"/"these"} and \TT{/"keep"/"allbut"} take any number
 252 of path arguments and one set argument.
 253 In the following rules if $ l $ is $ [p_1, \cdots, p_m] $ then
 254 $ W $ is $ \{\Name\ p_1, \cdots, \Name\ p_m\} $ Moreover {\Keep} and $\Keep\p$
 255 are helper functions and the usual rule overriding policy applies.
 256
 257 \begin{footnotesize}
 258 \begin{center}
 259 %
 260 \irule{l \oft \Listof\ \TT{<path>} \spc (\G, x) \daq S}{}
 261       {\Fun\ \TT{/"keep"/"these"}\ l\ [x]\ \G \equiv
 262        \{ (r, \bigsor \{ \Keep\ \T\ W\ G \st G \in A \}) \st (r, A) \in S \}}
 263 %
 264 \end{center}
 265 \begin{center}
 266 %
 267 \irule{l \oft \Listof\ \TT{<path>} \spc (\G, x) \daq S}{}
 268       {\Fun\ \TT{/"keep"/"allbut"}\ l\ [x]\ \G \equiv
 269        \{ (r, \bigsor \{ \Keep\ \F\ W\ G \st G \in A \}) \st (r, A) \in S \}}
 270 %
 271 \end{center}
 272 \begin{center}
 273 %
 274 \irule{\Keep\p\ b\ W\ G\ \RM{rewrites to}\ \ES}{1}
 275 {\Keep\ b\ W\ G\ \RM{rewrites to}\ \ES} \spc
 276 \irule{\Keep\p\ b\ W\ G\ \RM{rewrites to}\ G\p}{2}
 277 {\Keep\ b\ W\ G\ \RM{rewrites to}\ \{G\p\}}
 278 %
 279 \end{center}
 280 \begin{center} \begin{tabular}{rll}
 281 %
 282 $ \Keep\p\ \T\ W\ G $ & rewrites to & $ \{ (p, V) \in G \st p \in W \} $ \\
 283 $ \Keep\p\ \F\ W\ G $ & rewrites to & $ \{ (p, V) \in G \st p \notin W \} $
 284 %
 285 \end{tabular} \end{center}
 286 \end{footnotesize}
 287
 288 ``\TT{keep} p$_1$\TT{,}$\cdots$\TT{,}p$_m$ \TT{in} x'' rewrites to
 289 ``\TT{fun /"keep"/"these"} \verb+{+p$_1$\TT{,}$\cdots$\TT{,}p$_m$\verb+}+ \verb+{+x\verb+}+'',
 290 ``\TT{keep} x'' rewrites to ``\TT{fun /"keep"/"these"} \verb+{}+ \verb+{+x\verb+}+'',
 291 ``\TT{keep allbut} p$_1$\TT{,}$\cdots$\TT{,}p$_m$ \TT{in} x'' rewrites to
 292 ``\TT{fun /"keep"/"allbut"} \verb+{+p$_1$\TT{,}$\cdots$\TT{,}p$_m$\verb+}+ \verb+{+x\verb+}+''
 293 and
 294 ``\TT{keep allbut} x'' rewrites to ``\TT{fun /"keep"/"allbut"} \verb+{}+ \verb+{+x\verb+}+''.
 295
 296 Note that ``\TT{keep allbut} x'' gives the same result as ``x'' does.
 297
 298 \end{itemize}