X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fmathql%2Fdoc%2Fmathql_operational_basic.tex;fp=helm%2Fmathql%2Fdoc%2Fmathql_operational_basic.tex;h=0000000000000000000000000000000000000000;hp=cc309f732b66a502852bcb6d1898309baf38f555;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1 diff --git a/helm/mathql/doc/mathql_operational_basic.tex b/helm/mathql/doc/mathql_operational_basic.tex deleted file mode 100644 index cc309f732..000000000 --- a/helm/mathql/doc/mathql_operational_basic.tex +++ /dev/null @@ -1,298 +0,0 @@ -\subsection {The basic library} - -In this section we present the functions provided by the {\MathQL}.4 basic -library. Describing the whole library would require an amount of space that -goes beyond the limits of this paper so we include here just a selection of -the available functions (the ones for which we gave the syntax extension in -\secref{Textual}). - -The function below are grouped by their arity. - -\begin{itemize} - -\item -\textbf{The predefined {\av} sets.} -The functions \TT{/"empty"}, \TT{/"false"} and \newline \TT{/"true"} take no -path arguments and no set arguments. - -\begin{footnotesize} -\begin{center} -% -\irule{\Nop}{}{\Fun\ \TT{/"empty"}\ [\,]\ [\,]\ \G \equiv \F} \spc -\irule{\Nop}{}{\Fun\ \TT{/"false"}\ [\,]\ [\,]\ \G \equiv \F} -\end{center} -\begin{center} -% -\irule{\Nop}{}{\Fun\ \TT{/"true"}\ [\,]\ [\,]\ \G \equiv \T} -% -\end{center} -\end{footnotesize} - -Moreover ``\TT{empty}'' rewrites to ``\verb+fun /"empty" {} {}+'', -``\TT{false}'' rewrites to ``\verb+fun /"false" {} {}+'' and -``\TT{true}'' rewrites to ``\verb+fun /"true" {} {}+''. - -\item -\textbf{Boolean negation and size.} -The functions \TT{/"not"} and \TT{/"count"} take no path arguments and one set -argument. -Here Rule 1 overrides rule 2. - -\begin{footnotesize} -\begin{center} -% -\irule{(\G, x) \daq \F}{1}{\Fun\ \TT{/"not"}\ [\,]\ [x]\ \G \equiv \T} \spc -\irule{(\G, x) \daq S}{2}{\Fun\ \TT{/"not"}\ [\,]\ [x]\ \G \equiv \F} -\end{center} -\begin{center} -% -\irule{(\G, x) \daq S}{}{\Fun\ \TT{/"count"}\ [\,]\ [x]\ \G \equiv \#\ S} -% -\end{center} -\end{footnotesize} - -Moreover ``\TT{not} x'' rewrites to ``\verb+fun /"not" {} {+x\verb+}+'' -and ``\TT{count} x'' rewrites to ``\verb+fun /"count" {} {+x\verb+}+''. - -\item -\textbf{Boolean xor, set-theoretic and numerical tests, difference.} -\TT{/"xor"}, \TT{/"sub"}, \TT{/"meet"}, \TT{/"eq"}, \TT{/"le"}, \TT{/"lt"} and -\TT{/"diff"} take no path arguments and two set arguments. -The rule with the lowest number is applied first. - -\begin{footnotesize} -\begin{center} -% -\irule{(\G, x_1) \daq \F \spc (\G, x_2) \daq \F}{1} - {\Fun\ \TT{/"xor"}\ [\,]\ [x_1, x_2]\ \G \equiv \T} \spc -\irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq \F}{2} - {\Fun\ \TT{/"xor"}\ [\,]\ [x_1, x_2]\ \G \equiv S_1} -% -\end{center} -\begin{center} -% -\irule{(\G, x_1) \daq \F \spc (\G, x_2) \daq S_2}{3} - {\Fun\ \TT{/"xor"}\ [\,]\ [x_1, x_2]\ \G \equiv S_2} \spc -\irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq S_2}{4} - {\Fun\ \TT{/"xor"}\ [\,]\ [x_1, x_2]\ \G \equiv \F} -% -\end{center} -\begin{center} -% -\irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq S_2}{} - {\Fun\ \TT{/"sub"}\ [\,]\ [x_1, x_2]\ \G \equiv (\Fsts\ S_1 \sub \Fsts\ S_2)} -% -\end{center} -\begin{center} -% -\irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq S_2}{} - {\Fun\ \TT{/"meet"}\ [\,]\ [x_1, x_2]\ \G \equiv (\Fsts\ S_1 \meet \Fsts\ S_2)} -% -\end{center} -\begin{center} -% -\irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq S_2}{} - {\Fun\ \TT{/"eq"}\ [\,]\ [x_1, x_2]\ \G \equiv (\Fsts\ S_1 = \Fsts\ S_2)} -% -\end{center} -\begin{center} -% -\irule{(\G, x_1) \daq \{(r_1, A_1)\} \spc (\G, x_2) \daq \{(r_2, A_2)\}}{} - {\Fun\ \TT{/"le"}\ [\,]\ [x_1, x_2]\ \G \equiv (r_1 \le r_2)} -% -\end{center} -\begin{center} -% -\irule{(\G, x_1) \daq \{(r_1, A_1)\} \spc (\G, x_2) \daq \{(r_2, A_2)\}}{} - {\Fun\ \TT{/"lt"}\ [\,]\ [x_1, x_2]\ \G \equiv (r_1 < r_2)} -% -\end{center} -\begin{center} -% -\irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq S_2}{} - {\Fun\ \TT{/"eq"}\ [\,]\ [x_1, x_2]\ \G \equiv (S_1 \sdiff S_2)} -% -\end{center} -\end{footnotesize} - -where $\sdiff$ is a helper function two rewrite rules: - -\begin{footnotesize} -\begin{center} \begin{tabular}{lrll} -5 & -$ (S_1 \sdor \{(r, A_1)\}) \sdiff (S_2 \sdor \{(r, A_2)\}) $ & rewrites to & -$ S_1 \sdiff S_2 $ \\ -6 & $ S_1 \sdiff S_2 $ & rewrites to & $ S_1 $ -% -\end{tabular} \end{center} -\end{footnotesize} - -``x \TT{xor} y'' rewrites to ``\verb+fun /"xor" {} {+x\TT{,}y\verb+}+'', -``x \TT{sub} y'' rewrites to \newline ``\verb+fun /"sub" {} {+x\TT{,}y\verb+}+'', -``x \TT{meet} y'' rewrites to ``\verb+fun /"meet" {} {+x\TT{,}y\verb+}+'', -``x \TT{eq} y'' rewrites to ``\verb+fun /"eq" {} {+x\TT{,}y\verb+}+'', -``x \TT{le} y'' rewrites to \newline ``\verb+fun /"le" {} {+x\TT{,}y\verb+}+'', -``x \TT{lt} y'' rewrites to ``\verb+fun /"lt" {} {+x\TT{,}y\verb+}+'' and -``x \TT{diff} y'' rewrites to ``\verb+fun /"diff" {} {+x\TT{,}y\verb+}+'' - -\item -\textbf{Conditional operator and standard \emph{select} clause}. -\TT{/"if"} takes no path arguments and three set arguments. -The usual rule overriding policy applies. - -\begin{footnotesize} -\begin{center} -% -\irule{(\G, x_1) \daq \F \spc (\G, x_3) \daq S_3}{1} - {\Fun\ \TT{/"if"}\ [\,]\ [x_1, x_2, x_2]\ \G \equiv S_3} \spc -\irule{(\G, x_1) \daq S_1 \spc (\G, x_2) \daq S_2}{2} - {\Fun\ \TT{/"if"}\ [\,]\ [x_1, x_2, x_2]\ \G \equiv S_2} -% -\end{center} -\end{footnotesize} - -``\TT{if} x \TT{then} y \TT{else} z'' rewrites to -``\verb+fun /"if" {} {+x\TT{,}y\TT{,}z\verb+}+'' and -``\TT{select} i \TT{from} x \TT{where} y'' rewrites to -``\TT{for} i \TT{in} x \TT{sup} \TT{if} y \TT{then} i \TT{else} \TT{empty}''. - -\item -\textbf{Intersection without attribute distribution.} -\TT{/"intersect"} takes no path arguments and any positive number of set -arguments. - -\begin{footnotesize} -\begin{center} -% -\irule{(\G, x_1) \daq S_1 \spc \cdots \spc (\G, x_m) \daq S_m}{} - {\Fun\ \TT{/"intersect"}\ [\,]\ [x_1, \cdots, x_m]\ \G \equiv - (S_1 \sprod \cdots \sprod S_m)} -% -\end{center} -\end{footnotesize} - -As usual -``x \TT{intersect} y'' rewrites to ``\verb+fun /"intersect" {} {+x\TT{,}y\verb+}+''. - -\item -\textbf{Union without attribute distribution, Boolean conjunction and -disjunction.} -\TT{/"union"}, \TT{/"and"} and \TT{/"or"} take no path arguments and any -number of set arguments. -The usual rule overriding policy applies. - -\begin{footnotesize} -\begin{center} -% -\irule{\Nop}{}{\Fun\ \TT{/"union"}\ [\,]\ [\,]\ \G \equiv \F} \spc -\irule{(\G, x_1) \daq S_1 \spc \cdots \spc (\G, x_m) \daq S_m}{} - {\Fun\ \TT{/"union"}\ [\,]\ [x_1, \cdots, x_m]\ \G \equiv - (S_1 \ssum \cdots \ssum S_m)} -% -\end{center} -\begin{center} -% -\irule{\Nop}{}{\Fun\ \TT{/"and"}\ [\,]\ [\,]\ \G \equiv \T} \spc -\irule{\Nop}{}{\Fun\ \TT{/"or"}\ [\,]\ [\,]\ \G \equiv \F} -% -\end{center} -\begin{center} -% -\irule{\Fun\ \TT{/"and"}\ [\,]\ l\ \G \equiv \F}{1} - {\Fun\ \TT{/"and"}\ [\,]\ (l \app [x])\ \G \equiv \F} \spc -\irule{\Fun\ \TT{/"or"}\ [\,]\ l\ \G \equiv \F \spc (\G, x) \daq S}{3} - {\Fun\ \TT{/"or"}\ [\,]\ (l \app [x])\ \G \equiv S} -% -\end{center} -\begin{center} -% -\irule{\Fun\ \TT{/"and"}\ [\,]\ l\ \G \equiv S_l \spc (\G, x) \daq S}{2} - {\Fun\ \TT{/"and"}\ [\,]\ (l \app [x])\ \G \equiv S} \spc -\irule{\Fun\ \TT{/"or"}\ [\,]\ l\ \G \equiv S_l}{4} - {\Fun\ \TT{/"or"}\ [\,]\ (l \app [x])\ \G \equiv S_l} -\end{center} -\end{footnotesize} - -``x \TT{and} y'' rewrites to ``\verb+fun /"and" {} {+x\TT{,}y\verb+}+'', -``x \TT{or} y'' rewrites to \newline ``\verb+fun /"or" {} {+x\TT{,}y\verb+}+'', -``x \TT{union} y'' rewrites to \kern-1.1pt ``\verb+fun /"union" {} {+x\TT{,}y\verb+}+'' -and ``\verb+{+x$_1$\TT{,}$\cdots$\TT{,}x$_m$\verb+}+'' rewrites to -``\verb+fun /"union" {} {+x$_1$\TT{,}$\cdots$\TT{,}x$_m$\verb+}+''. - -\item -\textbf{Projection.} -\TT{/"proj"} takes one path argument and one set argument. - -\begin{footnotesize} -\begin{center} -% -\irule {p \oft \TT{} \spc - (\G, x) \daq \{ (r_1, A_1), \cdots, (r_m, A_m) \}}{} - {\Fun\ \TT{/"proj"}\ [p]\ [x]\ \G \equiv - \Head\ (\Proj\ (\Name\ p)\ A_1 \sor \cdots \sor \Proj\ (\Name\ p)\ A_m)} -% -\end{center} -\begin{center} \begin{tabular}{rll} -% -$ \Proj\ p\ \{G_1, \cdots, G_n\} $ & rewrites to & -$ \get{G_1}{p} \sor \cdots \sor \get{G_n}{p} $ \\ -$ \Head\ \{s_1, \cdots, s_k\} $ & rewrites to & $ \{ (s_1, \ES), \cdots, (s_k, \ES) \} $ -\end{tabular} \end{center} -\end{footnotesize} - -where, for each $ 1 \le j \le n $, $ \get{G_j}{p} $ is $ \ES $ if $ p $ is not -defined in $ G_j $. - -Moreover -``\TT{proj} p \TT{of} x'' rewrites to ``\verb+fun /"proj" {+p\verb+} {+x\verb+}+''. - -\item -\textbf{Refinement.} -The functions \TT{/"keep"/"these"} and \TT{/"keep"/"allbut"} take any number -of path arguments and one set argument. -In the following rules if $ l $ is $ [p_1, \cdots, p_m] $ then -$ W $ is $ \{\Name\ p_1, \cdots, \Name\ p_m\} $ Moreover {\Keep} and $\Keep\p$ -are helper functions and the usual rule overriding policy applies. - -\begin{footnotesize} -\begin{center} -% -\irule{l \oft \Listof\ \TT{} \spc (\G, x) \daq S}{} - {\Fun\ \TT{/"keep"/"these"}\ l\ [x]\ \G \equiv - \{ (r, \bigsor \{ \Keep\ \T\ W\ G \st G \in A \}) \st (r, A) \in S \}} -% -\end{center} -\begin{center} -% -\irule{l \oft \Listof\ \TT{} \spc (\G, x) \daq S}{} - {\Fun\ \TT{/"keep"/"allbut"}\ l\ [x]\ \G \equiv - \{ (r, \bigsor \{ \Keep\ \F\ W\ G \st G \in A \}) \st (r, A) \in S \}} -% -\end{center} -\begin{center} -% -\irule{\Keep\p\ b\ W\ G\ \RM{rewrites to}\ \ES}{1} -{\Keep\ b\ W\ G\ \RM{rewrites to}\ \ES} \spc -\irule{\Keep\p\ b\ W\ G\ \RM{rewrites to}\ G\p}{2} -{\Keep\ b\ W\ G\ \RM{rewrites to}\ \{G\p\}} -% -\end{center} -\begin{center} \begin{tabular}{rll} -% -$ \Keep\p\ \T\ W\ G $ & rewrites to & $ \{ (p, V) \in G \st p \in W \} $ \\ -$ \Keep\p\ \F\ W\ G $ & rewrites to & $ \{ (p, V) \in G \st p \notin W \} $ -% -\end{tabular} \end{center} -\end{footnotesize} - -``\TT{keep} p$_1$\TT{,}$\cdots$\TT{,}p$_m$ \TT{in} x'' rewrites to -``\TT{fun /"keep"/"these"} \verb+{+p$_1$\TT{,}$\cdots$\TT{,}p$_m$\verb+}+ \verb+{+x\verb+}+'', -``\TT{keep} x'' rewrites to ``\TT{fun /"keep"/"these"} \verb+{}+ \verb+{+x\verb+}+'', -``\TT{keep allbut} p$_1$\TT{,}$\cdots$\TT{,}p$_m$ \TT{in} x'' rewrites to -``\TT{fun /"keep"/"allbut"} \verb+{+p$_1$\TT{,}$\cdots$\TT{,}p$_m$\verb+}+ \verb+{+x\verb+}+'' -and -``\TT{keep allbut} x'' rewrites to ``\TT{fun /"keep"/"allbut"} \verb+{}+ \verb+{+x\verb+}+''. - -Note that ``\TT{keep allbut} x'' gives the same result as ``x'' does. - -\end{itemize}