]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/mathql/doc/mathql_introduction_basic.tex
This commit was manufactured by cvs2svn to create branch 'moogle'.
[helm.git] / helm / mathql / doc / mathql_introduction_basic.tex
diff --git a/helm/mathql/doc/mathql_introduction_basic.tex b/helm/mathql/doc/mathql_introduction_basic.tex
deleted file mode 100644 (file)
index ccf13f2..0000000
+++ /dev/null
@@ -1,136 +0,0 @@
-\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}
-