]> matita.cs.unibo.it Git - helm.git/blobdiff - mathql/doc/mathql_introduction_basic.tex
moved mathql/ under software/
[helm.git] / mathql / doc / mathql_introduction_basic.tex
diff --git a/mathql/doc/mathql_introduction_basic.tex b/mathql/doc/mathql_introduction_basic.tex
new file mode 100644 (file)
index 0000000..ccf13f2
--- /dev/null
@@ -0,0 +1,136 @@
+\subsection{The basic library} \label{Basic}
+
+The present paper leaves us too little space to present a complete
+description of {\MathQL}.4 basic library, so we only give a glance to the
+features it provides.
+
+For the user convenience {\MathQL}.4 includes a syntax extension for all the
+basic library functions, in order to hide the actual function invocation.
+
+Here are some of the provided constructions:
+
+\begin{itemize}
+
+\item 
+\textbf{Aliases for commonly used constant {\av} sets.}
+\EM{empty}, \EM{false}, \EM{true}. 
+
+\item 
+\textbf{Conditional operator.} 
+\TT{if} \EM{av-set} \TT{then} \EM{av-set} \TT{else} \EM{av-set}.
+Tests the first {\av} set for inhabitance and evaluates one of the other {\av}
+sets accordingly.
+
+\item 
+\textbf{Standard \emph{select} clause.} 
+\TT{select @}\EM{variable} \TT{from} \EM{av-set-1} \TT{where} \EM{av-set-2}.
+It is:
+\TT{for @}\EM{variable} \TT{in} \EM{av-set-1} \TT{sup}
+\TT{if} \EM{av-set-2} \TT{then @}\EM{variable} \TT{else empty}.
+
+\item
+\textbf{Set refinement}. The operator
+\TT{keep} \EM{optional-flag} \EM{name-list} \TT{in} \EM{av-set}
+removes from its argument every attribute whose name is included (or is not,
+according to the \EM{flag}) in the given \EM{name-list}.
+If the \EM{flag} is not present, the \EM{name-list} specifies the attributes
+to keep, whereas if the \EM{flag} is \TT{allbut}, the \EM{name-list} specifies
+the attributes to remove.
+Removing unwanted information from an {\av} set is useful in two cases: it
+lowers the complexity of intermediate query results increasing the performance
+of subsequent operations and it cleans the final query results making them
+easier to manage for the application that submits the query.%
+\footnote
+{Interpreting {\av} sets as relational database tables, this functionality
+allows to select the columns a table is made of, as with the {\SQL} 
+\emph{select} operator.}
+
+\item
+\textbf{projections.} 
+The operator 
+\TT{proj} \EM{name} \TT{of} \EM{av-set} makes the set-theoretic union of the
+contents that the specified attribute has in each group of the given {\av} set.
+Each element of this union then becomes the head string of an {\av} without
+attributes and the set of these is returned.%
+\footnote
+{This is the content of a labelled column of the given \EM{av-set} viewed as a
+table.} 
+See \figref{Proj}.
+
+\begin{figure}
+\begin{footnotesize} \begin{verbatim}
+proj /"name" of ["1" attr {\"name" = {"a", "b"}}, {\"name" = {"b", "c"}} 
+gives "a"; "b"; "b"
+\end{verbatim} \end{footnotesize}
+\vspace{-1pc}
+\caption{A simple projection} \label{Proj}
+\end{figure}
+
+The construction \TT{keep} \EM{av-set} is also provided to remove all the
+attributes in the given \EM{av-set} ({\ie} the list of the attributes to keep
+is empty).%
+\footnote
+{This is the content of the first column of the \EM{av-set} viewed as a table.}
+
+\item
+\textbf{Core operations on {\av} sets.}
+\EM{av-set} \EM{core-operator} \EM{av-set}
+returns an {\av} set composing the two operands according to the specified
+\EM{core-operator} (see \subsecref{AVSets}) which can be \TT{union}
+(set-theoretic union), \TT{intersect} (set-theoretic intersection) or
+\TT{diff} (difference). 
+\TT{union} and \TT{intersect} are also provided in their $n$-ary form
+($ n \ge 1 $ for \TT{intersect}) and the $n$-ary union has the syntax
+extension: 
+\verb+{+ \EM{av-set} \TT{,} $\cdots$ \TT{,} \EM{av-set} \verb+}+.
+
+\item 
+\textbf{Logical operations on {\av} sets.}
+\EM{and}, \EM{or}, \EM{xor}, \EM{not}.
+They are inspired by the C-style Boolean operators defined for the
+integer numbers. In particular:
+
+\TT{not} \EM{av-set}:
+returns \emph{false} if the \EM{av-set} is inhabited, or \emph{true} otherwise.
+
+\EM{av-set-1} \TT{and} \EM{av-set-2}:
+gives \EM{av-set-2} if \EM{av-set-1} is inhabited, or \emph{false} otherwise.
+
+\EM{av-set-1} \TT{or} \EM{av-set-2}:
+returns \EM{av-set-1} if it is inhabited, or \EM{av-set-2} otherwise.
+
+\EM{av-set-1} \TT{xor} \EM{av-set-2}:
+gives \emph{false} if both av-sets are inhabited or empty, or the inhabited
+\EM{av-set} otherwise.
+
+\TT{and} and \TT{or} are also available in their $n$-ary form.
+
+\item 
+\textbf{Comparisons between {\av} sets.}
+\EM{av-set} \EM{test-operator} \EM{av-set}.
+Following the repetition rules of {\av} sets presented in \subsecref{AVSets},
+these operators work just on the head strings of their arguments and
+discard the attributes. All of them return \emph{false} or \emph{true}
+according to the outcome of the respective test. 
+The \emph{test-operator} includes: \TT{sub} (set-theoretic subset relation),
+\TT{eq} (set-theoretic quality), \TT{meet} (inhabitance of the set-theoretic
+intersection), \TT{le} (numeric less-or-equal-than), \TT{lt} (numeric
+less-than).%
+\footnote{\TT{le} and \TT{lt} return \emph{false} if their operands are invalid
+numbers.}
+
+Note that the set-theoretic ``meet'' operator 
+({\ie} $ V \meet W \equiv (\lex v \in V)\ v \in W $)
+is the natural companion of the corresponding ``sub'' operator 
+({\ie} $ V \sub W \equiv (\lall v \in V)\ v \in W $) being its logical dual
+and is already being used successfully in the context of a constructive
+({\ie} intuitionistic and predicative) approach to point-free topology
+(see \cite{Sam00} for details).
+
+\item 
+\textbf{Cardinality of an {\av} set.}
+This information is retrieved by the operator \TT{count} \EM{av-set} that
+returns an {\av} set representing a natural number.
+
+\end{itemize}
+