updating all sections

diff --git a/helm/mathql/doc/fguidi-defs.sty b/helm/mathql/doc/fguidi-defs.sty
deleted file mode 100644 (file)
index df71b44..0000000
--- a/helm/mathql/doc/fguidi-defs.sty
+++ /dev/null
@@ -1,121 +0,0 @@
-%\DeclareSymbolFont{stmary}{U}{stmary}{m}{n}
-%\DeclareFontFamily{U}{stmary}{}%
-%\DeclareFontShape{U}{stmary}{m}{n}{<-6>stmary5<6-8>stmary7<8->stmary10}{}%
-%\DeclareMathSymbol{\odb}{\mathopen}{stmary}{"4A}
-%\DeclareMathSymbol{\cdb}{\mathclose}{stmary}{"4B}
-
-\usepackage{amssymb}
-\usepackage{stmaryrd}
-
-% LOGIC  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
-
-% utilities
-
-\def\cv{\,]}
-\def\ov{[\,}
-\def\spc{\hspace{1em}} % 0.25em per la tesi
-\def\nop{{}}
-\def\Nop{\noindent\hbox to 0pt{\vbox to 1ex{\vfil}\hfil}}
-\def\gdlap#1#2{\vbox to 0pt {\vskip#2\hbox{#1}\vss}}
-\def\?#1{\mathord{#1}}
-
-% inference trees
-
-\def\imain#1{{\offinterlineskip\lineskip=2pt\noindent
-  \hbox{$\vcenter{\halign{\hss$##$\hss&##\hss\cr#1\crcr}}$}}}
-\def\itree#1{{\offinterlineskip\lineskip=2pt\noindent
-  \hbox{$\vbox{\halign{\hss$##$\hss&##\hss\cr#1\crcr}}$}}}
-
-\def\setnames@#1#2{&\gdlap{\kern2pt$#1$}{#2}} 
-\def\iname#1 {\cr\hrulefill\setnames@{#1}{-1.0ex}\cr}
-\def\inames#1 {\cr\hrulefill\cr\hrulefill\setnames@{#1}{-1.2ex}\cr}
-\def\ivrule{\cr\vrule height 3ex \cr}
-\def\discharge#1#2 {\iname{#1\,#2} }
-\def\assume#1#2{\ov #1\cv\rlap{$^{#2}$}}
-
-% single rules
-
-\def\irule#1#2#3{\imain{#1 \iname{#2} #3 }}   % "single step"
-\def\irules#1#2#3{\imain{#1 \inames{#2} #3 }} % "multistep"
-
-\def\drule#1#2#3{\itree{#1 \iname{#2} #3 }}   % "single step"
-\def\drules#1#2#3{\itree{#1 \inames{#2} #3 }} % "multistep"
-
-\def\cirule#1#2#3{$\vcenter{\irule{#1}{#2}{#3}}$}   % "single step"
-\def\cirules#1#2#3{$\vcenter{\irules{#1}{#2}{#3}}$} % "multistep"
-
-% MATHEMATICS  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\def\a{\phi}
-\def\b{\psi}
-\def\c{\xi}
-\def\d{\eta}
-\def\A{\Phi}
-\def\B{\Psi}
-\def\C{\Xi}
-\def\jolly{\mathbin\square}
-\def\lall{\forall}
-\def\lex{\exists}
-\def\lbot{{\bot}}
-\def\lexcl{\mathrel\leftarrow}
-\def\limp{\mathrel\rightarrow}
-\def\liff{\mathrel\leftrightarrow}
-\def\lone{1}
-\def\lplus{\mathrel\oplus}
-\def\ltimes{\mathrel\otimes}
-\def\ltop{{\top}}
-\def\lzero{0}
-\def\lpar{\mathrel\bindnasrepma}
-\def\lamp{\mathrel\binampersand}
-
-\def\meet{\between}
-\def\bigsor{\bigcup}
-\def\bigsand{\bigcap}
-\def\sand{\cap}
-\def\sdor{\sqcup}
-\def\sor{\cup}
-\def\simp{\Rightarrow}
-\def\snot{-}
-\def\sub{\subseteq}
-\def\sup{\supseteq}
-\def\sbot{\emptyset}
-\def\stop{\ltop}
-
-\def\after{\mathbin\circ}
-\def\app{\mathbin @}
-\def\e{\mathrel\epsilon}
-\def\oft{\mathrel :}
-\def\p{{^\prime}}
-\def\st{\mathrel |}
-\def\subset#1{\{#1\}}
-\def\yld{\mathrel\vdash}
-\def\Frm{\textsf{Frm}}
-\def\Trm{\textsf{Trm}}
-\def\LB{{\bf B}}
-\def\LBm{{\bf B}$^-$}
-\def\LBmi{{\bf B}$^-_{\limp}$}
-\def\LBmiq{{\bf B}$^-_{\limp\lexcl\lall\lex}$}
-\def\LBLS{{\bf BLS}}
-\def\P{{\cal P}}
-
-\def\mand{\mathrel{\textbf{and}}}
-\def\miff{\mathrel{\textbf{iff}}}
-\def\mimp{\mathrel{\textbf{implies}}}
-\def\mpiff{\mathrel{\textbf{\frenchspacing prim. iff}}}
-\def\mpimp{\mathrel{\textbf{\frenchspacing prim. implies}}}
-\def\mtrue{\mathord{\textbf{true}}}
-\def\mall{\mathrel{\textbf{all}}}
-
-% TEXT  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\def\EM#1{\noindent\hbox{\frenchspacing\em #1}}
-\def\TT#1{\noindent\hbox{\frenchspacing\tt #1}}
-\def\RM#1{\noindent\hbox{\frenchspacing\rm #1}}
-\def\URI#1{\texttt{<#1>}}
-
-\def\ie{{\frenchspacing i.e.}}
-\def\df#1{{\bf #1}}
-\long\def\xcomment#1{}
-\def\proc{{\frenchspacing proc.}}
-\def\etc{{\frenchspacing etc.}}
-\def\po{{\frenchspacing p.o.}}

diff --git a/helm/mathql/doc/llncs.cls b/helm/mathql/doc/llncs.cls
new file mode 100644 (file)
index 0000000..29e505e
--- /dev/null
+++ b/helm/mathql/doc/llncs.cls
@@ -0,0 +1,1189 @@
+% LLNCS DOCUMENT CLASS -- version 2.13 (28-Jan-2002)
+% Springer Verlag LaTeX2e support for Lecture Notes in Computer Science
+%
+%%
+%% \CharacterTable
+%%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+%%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+%%   Digits        \0\1\2\3\4\5\6\7\8\9
+%%   Exclamation   \!     Double quote  \"     Hash (number) \#
+%%   Dollar        \$     Percent       \%     Ampersand     \&
+%%   Acute accent  \'     Left paren    \(     Right paren   \)
+%%   Asterisk      \*     Plus          \+     Comma         \,
+%%   Minus         \-     Point         \.     Solidus       \/
+%%   Colon         \:     Semicolon     \;     Less than     \<
+%%   Equals        \=     Greater than  \>     Question mark \?
+%%   Commercial at \@     Left bracket  \[     Backslash     \\
+%%   Right bracket \]     Circumflex    \^     Underscore    \_
+%%   Grave accent  \`     Left brace    \{     Vertical bar  \|
+%%   Right brace   \}     Tilde         \~}
+%%
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesClass{llncs}[2002/01/28 v2.13
+^^J LaTeX document class for Lecture Notes in Computer Science]
+% Options
+\let\if@envcntreset\iffalse
+\DeclareOption{envcountreset}{\let\if@envcntreset\iftrue}
+\DeclareOption{citeauthoryear}{\let\citeauthoryear=Y}
+\DeclareOption{oribibl}{\let\oribibl=Y}
+\let\if@custvec\iftrue
+\DeclareOption{orivec}{\let\if@custvec\iffalse}
+\let\if@envcntsame\iffalse
+\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue}
+\let\if@envcntsect\iffalse
+\DeclareOption{envcountsect}{\let\if@envcntsect\iftrue}
+\let\if@runhead\iffalse
+\DeclareOption{runningheads}{\let\if@runhead\iftrue}
+
+\let\if@openbib\iffalse
+\DeclareOption{openbib}{\let\if@openbib\iftrue}
+
+% languages
+\let\switcht@@therlang\relax
+\def\ds@deutsch{\def\switcht@@therlang{\switcht@deutsch}}
+\def\ds@francais{\def\switcht@@therlang{\switcht@francais}}
+
+\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}}
+
+\ProcessOptions
+
+\LoadClass[twoside]{article}
+\RequirePackage{multicol} % needed for the list of participants, index
+
+\setlength{\textwidth}{12.2cm}
+\setlength{\textheight}{19.3cm}
+\renewcommand\@pnumwidth{2em}
+\renewcommand\@tocrmarg{3.5em}
+%
+\def\@dottedtocline#1#2#3#4#5{%
+  \ifnum #1>\c@tocdepth \else
+    \vskip \z@ \@plus.2\p@
+    {\leftskip #2\relax \rightskip \@tocrmarg \advance\rightskip by 0pt plus 2cm
+               \parfillskip -\rightskip \pretolerance=10000
+     \parindent #2\relax\@afterindenttrue
+     \interlinepenalty\@M
+     \leavevmode
+     \@tempdima #3\relax
+     \advance\leftskip \@tempdima \null\nobreak\hskip -\leftskip
+     {#4}\nobreak
+     \leaders\hbox{$\m@th
+        \mkern \@dotsep mu\hbox{.}\mkern \@dotsep
+        mu$}\hfill
+     \nobreak
+     \hb@xt@\@pnumwidth{\hfil\normalfont \normalcolor #5}%
+     \par}%
+  \fi}
+%
+\def\switcht@albion{%
+\def\abstractname{Abstract.}
+\def\ackname{Acknowledgement.}
+\def\andname{and}
+\def\lastandname{\unskip, and}
+\def\appendixname{Appendix}
+\def\chaptername{Chapter}
+\def\claimname{Claim}
+\def\conjecturename{Conjecture}
+\def\contentsname{Table of Contents}
+\def\corollaryname{Corollary}
+\def\definitionname{Definition}
+\def\examplename{Example}
+\def\exercisename{Exercise}
+\def\figurename{Fig.}
+\def\keywordname{{\bf Key words:}}
+\def\indexname{Index}
+\def\lemmaname{Lemma}
+\def\contriblistname{List of Contributors}
+\def\listfigurename{List of Figures}
+\def\listtablename{List of Tables}
+\def\mailname{{\it Correspondence to\/}:}
+\def\noteaddname{Note added in proof}
+\def\notename{Note}
+\def\partname{Part}
+\def\problemname{Problem}
+\def\proofname{Proof}
+\def\propertyname{Property}
+\def\propositionname{Proposition}
+\def\questionname{Question}
+\def\remarkname{Remark}
+\def\seename{see}
+\def\solutionname{Solution}
+\def\subclassname{{\it Subject Classifications\/}:}
+\def\tablename{Table}
+\def\theoremname{Theorem}}
+\switcht@albion
+% Names of theorem like environments are already defined
+% but must be translated if another language is chosen
+%
+% French section
+\def\switcht@francais{%\typeout{On parle francais.}%
+ \def\abstractname{R\'esum\'e.}%
+ \def\ackname{Remerciements.}%
+ \def\andname{et}%
+ \def\lastandname{ et}%
+ \def\appendixname{Appendice}
+ \def\chaptername{Chapitre}%
+ \def\claimname{Pr\'etention}%
+ \def\conjecturename{Hypoth\`ese}%
+ \def\contentsname{Table des mati\`eres}%
+ \def\corollaryname{Corollaire}%
+ \def\definitionname{D\'efinition}%
+ \def\examplename{Exemple}%
+ \def\exercisename{Exercice}%
+ \def\figurename{Fig.}%
+ \def\keywordname{{\bf Mots-cl\'e:}}
+ \def\indexname{Index}
+ \def\lemmaname{Lemme}%
+ \def\contriblistname{Liste des contributeurs}
+ \def\listfigurename{Liste des figures}%
+ \def\listtablename{Liste des tables}%
+ \def\mailname{{\it Correspondence to\/}:}
+ \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}%
+ \def\notename{Remarque}%
+ \def\partname{Partie}%
+ \def\problemname{Probl\`eme}%
+ \def\proofname{Preuve}%
+ \def\propertyname{Caract\'eristique}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Question}%
+ \def\remarkname{Remarque}%
+ \def\seename{voir}
+ \def\solutionname{Solution}%
+ \def\subclassname{{\it Subject Classifications\/}:}
+ \def\tablename{Tableau}%
+ \def\theoremname{Th\'eor\`eme}%
+}
+%
+% German section
+\def\switcht@deutsch{%\typeout{Man spricht deutsch.}%
+ \def\abstractname{Zusammenfassung.}%
+ \def\ackname{Danksagung.}%
+ \def\andname{und}%
+ \def\lastandname{ und}%
+ \def\appendixname{Anhang}%
+ \def\chaptername{Kapitel}%
+ \def\claimname{Behauptung}%
+ \def\conjecturename{Hypothese}%
+ \def\contentsname{Inhaltsverzeichnis}%
+ \def\corollaryname{Korollar}%
+%\def\definitionname{Definition}%
+ \def\examplename{Beispiel}%
+ \def\exercisename{\"Ubung}%
+ \def\figurename{Abb.}%
+ \def\keywordname{{\bf Schl\"usselw\"orter:}}
+ \def\indexname{Index}
+%\def\lemmaname{Lemma}%
+ \def\contriblistname{Mitarbeiter}
+ \def\listfigurename{Abbildungsverzeichnis}%
+ \def\listtablename{Tabellenverzeichnis}%
+ \def\mailname{{\it Correspondence to\/}:}
+ \def\noteaddname{Nachtrag}%
+ \def\notename{Anmerkung}%
+ \def\partname{Teil}%
+%\def\problemname{Problem}%
+ \def\proofname{Beweis}%
+ \def\propertyname{Eigenschaft}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Frage}%
+ \def\remarkname{Anmerkung}%
+ \def\seename{siehe}
+ \def\solutionname{L\"osung}%
+ \def\subclassname{{\it Subject Classifications\/}:}
+ \def\tablename{Tabelle}%
+%\def\theoremname{Theorem}%
+}
+
+% Ragged bottom for the actual page
+\def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil
+\global\let\@textbottom\relax}}
+
+\renewcommand\small{%
+   \@setfontsize\small\@ixpt{11}%
+   \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@
+   \abovedisplayshortskip \z@ \@plus2\p@
+   \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@
+   \def\@listi{\leftmargin\leftmargini
+               \parsep 0\p@ \@plus1\p@ \@minus\p@
+               \topsep 8\p@ \@plus2\p@ \@minus4\p@
+               \itemsep0\p@}%
+   \belowdisplayskip \abovedisplayskip
+}
+
+\frenchspacing
+\widowpenalty=10000
+\clubpenalty=10000
+
+\setlength\oddsidemargin   {63\p@}
+\setlength\evensidemargin  {63\p@}
+\setlength\marginparwidth  {90\p@}
+
+\setlength\headsep   {16\p@}
+
+\setlength\footnotesep{7.7\p@}
+\setlength\textfloatsep{8mm\@plus 2\p@ \@minus 4\p@}
+\setlength\intextsep   {8mm\@plus 2\p@ \@minus 2\p@}
+
+\setcounter{secnumdepth}{2}
+
+\newcounter {chapter}
+\renewcommand\thechapter      {\@arabic\c@chapter}
+
+\newif\if@mainmatter \@mainmattertrue
+\newcommand\frontmatter{\cleardoublepage
+            \@mainmatterfalse\pagenumbering{Roman}}
+\newcommand\mainmatter{\cleardoublepage
+       \@mainmattertrue\pagenumbering{arabic}}
+\newcommand\backmatter{\if@openright\cleardoublepage\else\clearpage\fi
+      \@mainmatterfalse}
+
+\renewcommand\part{\cleardoublepage
+                 \thispagestyle{empty}%
+                 \if@twocolumn
+                     \onecolumn
+                     \@tempswatrue
+                   \else
+                     \@tempswafalse
+                 \fi
+                 \null\vfil
+                 \secdef\@part\@spart}
+
+\def\@part[#1]#2{%
+    \ifnum \c@secnumdepth >-2\relax
+      \refstepcounter{part}%
+      \addcontentsline{toc}{part}{\thepart\hspace{1em}#1}%
+    \else
+      \addcontentsline{toc}{part}{#1}%
+    \fi
+    \markboth{}{}%
+    {\centering
+     \interlinepenalty \@M
+     \normalfont
+     \ifnum \c@secnumdepth >-2\relax
+       \huge\bfseries \partname~\thepart
+       \par
+       \vskip 20\p@
+     \fi
+     \Huge \bfseries #2\par}%
+    \@endpart}
+\def\@spart#1{%
+    {\centering
+     \interlinepenalty \@M
+     \normalfont
+     \Huge \bfseries #1\par}%
+    \@endpart}
+\def\@endpart{\vfil\newpage
+              \if@twoside
+                \null
+                \thispagestyle{empty}%
+                \newpage
+              \fi
+              \if@tempswa
+                \twocolumn
+              \fi}
+
+\newcommand\chapter{\clearpage
+                    \thispagestyle{empty}%
+                    \global\@topnum\z@
+                    \@afterindentfalse
+                    \secdef\@chapter\@schapter}
+\def\@chapter[#1]#2{\ifnum \c@secnumdepth >\m@ne
+                       \if@mainmatter
+                         \refstepcounter{chapter}%
+                         \typeout{\@chapapp\space\thechapter.}%
+                         \addcontentsline{toc}{chapter}%
+                                  {\protect\numberline{\thechapter}#1}%
+                       \else
+                         \addcontentsline{toc}{chapter}{#1}%
+                       \fi
+                    \else
+                      \addcontentsline{toc}{chapter}{#1}%
+                    \fi
+                    \chaptermark{#1}%
+                    \addtocontents{lof}{\protect\addvspace{10\p@}}%
+                    \addtocontents{lot}{\protect\addvspace{10\p@}}%
+                    \if@twocolumn
+                      \@topnewpage[\@makechapterhead{#2}]%
+                    \else
+                      \@makechapterhead{#2}%
+                      \@afterheading
+                    \fi}
+\def\@makechapterhead#1{%
+% \vspace*{50\p@}%
+  {\centering
+    \ifnum \c@secnumdepth >\m@ne
+      \if@mainmatter
+        \large\bfseries \@chapapp{} \thechapter
+        \par\nobreak
+        \vskip 20\p@
+      \fi
+    \fi
+    \interlinepenalty\@M
+    \Large \bfseries #1\par\nobreak
+    \vskip 40\p@
+  }}
+\def\@schapter#1{\if@twocolumn
+                   \@topnewpage[\@makeschapterhead{#1}]%
+                 \else
+                   \@makeschapterhead{#1}%
+                   \@afterheading
+                 \fi}
+\def\@makeschapterhead#1{%
+% \vspace*{50\p@}%
+  {\centering
+    \normalfont
+    \interlinepenalty\@M
+    \Large \bfseries  #1\par\nobreak
+    \vskip 40\p@
+  }}
+
+\renewcommand\section{\@startsection{section}{1}{\z@}%
+                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {12\p@ \@plus 4\p@ \@minus 4\p@}%
+                       {\normalfont\large\bfseries\boldmath
+                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
+\renewcommand\subsection{\@startsection{subsection}{2}{\z@}%
+                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {8\p@ \@plus 4\p@ \@minus 4\p@}%
+                       {\normalfont\normalsize\bfseries\boldmath
+                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
+\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}%
+                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {-0.5em \@plus -0.22em \@minus -0.1em}%
+                       {\normalfont\normalsize\bfseries\boldmath}}
+\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}%
+                       {-12\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {-0.5em \@plus -0.22em \@minus -0.1em}%
+                       {\normalfont\normalsize\itshape}}
+\renewcommand\subparagraph[1]{\typeout{LLNCS warning: You should not use
+                  \string\subparagraph\space with this class}\vskip0.5cm
+You should not use \verb|\subparagraph| with this class.\vskip0.5cm}
+
+\DeclareMathSymbol{\Gamma}{\mathalpha}{letters}{"00}
+\DeclareMathSymbol{\Delta}{\mathalpha}{letters}{"01}
+\DeclareMathSymbol{\Theta}{\mathalpha}{letters}{"02}
+\DeclareMathSymbol{\Lambda}{\mathalpha}{letters}{"03}
+\DeclareMathSymbol{\Xi}{\mathalpha}{letters}{"04}
+\DeclareMathSymbol{\Pi}{\mathalpha}{letters}{"05}
+\DeclareMathSymbol{\Sigma}{\mathalpha}{letters}{"06}
+\DeclareMathSymbol{\Upsilon}{\mathalpha}{letters}{"07}
+\DeclareMathSymbol{\Phi}{\mathalpha}{letters}{"08}
+\DeclareMathSymbol{\Psi}{\mathalpha}{letters}{"09}
+\DeclareMathSymbol{\Omega}{\mathalpha}{letters}{"0A}
+
+\let\footnotesize\small
+
+\if@custvec
+\def\vec#1{\mathchoice{\mbox{\boldmath$\displaystyle#1$}}
+{\mbox{\boldmath$\textstyle#1$}}
+{\mbox{\boldmath$\scriptstyle#1$}}
+{\mbox{\boldmath$\scriptscriptstyle#1$}}}
+\fi
+
+\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
+\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
+\penalty50\hskip1em\null\nobreak\hfil\squareforqed
+\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}
+
+\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip
+\halign{\hfil
+$\displaystyle##$\hfil\cr\gets\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets
+\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets
+\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+\gets\cr\to\cr}}}}}
+\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
+$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr
+\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr
+\noalign{\vskip1pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+<\cr
+\noalign{\vskip0.9pt}=\cr}}}}}
+\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
+$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr
+\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr
+\noalign{\vskip1pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+>\cr
+\noalign{\vskip0.9pt}=\cr}}}}}
+\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip
+\halign{\hfil
+$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-1pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr
+>\cr\noalign{\vskip-1pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr
+>\cr\noalign{\vskip-0.8pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+>\cr\noalign{\vskip-0.3pt}<\cr}}}}}
+\def\bbbr{{\rm I\!R}} %reelle Zahlen
+\def\bbbm{{\rm I\!M}}
+\def\bbbn{{\rm I\!N}} %natuerliche Zahlen
+\def\bbbf{{\rm I\!F}}
+\def\bbbh{{\rm I\!H}}
+\def\bbbk{{\rm I\!K}}
+\def\bbbp{{\rm I\!P}}
+\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l}
+{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}}
+\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}}}
+\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
+Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}}
+\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
+T$}\hbox{\hbox to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}}}
+\def\bbbs{{\mathchoice
+{\setbox0=\hbox{$\displaystyle     \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
+to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle        \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
+to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle      \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
+to0pt{\kern0.5\wd0\vrule height0.45\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.4\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
+to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}}
+\def\bbbz{{\mathchoice {\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
+{\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
+{\hbox{$\mathsf\scriptstyle Z\kern-0.3em Z$}}
+{\hbox{$\mathsf\scriptscriptstyle Z\kern-0.2em Z$}}}}
+
+\let\ts\,
+
+\setlength\leftmargini  {17\p@}
+\setlength\leftmargin    {\leftmargini}
+\setlength\leftmarginii  {\leftmargini}
+\setlength\leftmarginiii {\leftmargini}
+\setlength\leftmarginiv  {\leftmargini}
+\setlength  \labelsep  {.5em}
+\setlength  \labelwidth{\leftmargini}
+\addtolength\labelwidth{-\labelsep}
+
+\def\@listI{\leftmargin\leftmargini
+            \parsep 0\p@ \@plus1\p@ \@minus\p@
+            \topsep 8\p@ \@plus2\p@ \@minus4\p@
+            \itemsep0\p@}
+\let\@listi\@listI
+\@listi
+\def\@listii {\leftmargin\leftmarginii
+              \labelwidth\leftmarginii
+              \advance\labelwidth-\labelsep
+              \topsep    0\p@ \@plus2\p@ \@minus\p@}
+\def\@listiii{\leftmargin\leftmarginiii
+              \labelwidth\leftmarginiii
+              \advance\labelwidth-\labelsep
+              \topsep    0\p@ \@plus\p@\@minus\p@
+              \parsep    \z@
+              \partopsep \p@ \@plus\z@ \@minus\p@}
+
+\renewcommand\labelitemi{\normalfont\bfseries --}
+\renewcommand\labelitemii{$\m@th\bullet$}
+
+\setlength\arraycolsep{1.4\p@}
+\setlength\tabcolsep{1.4\p@}
+
+\def\tableofcontents{\chapter*{\contentsname\@mkboth{{\contentsname}}%
+                                                    {{\contentsname}}}
+ \def\authcount##1{\setcounter{auco}{##1}\setcounter{@auth}{1}}
+ \def\lastand{\ifnum\value{auco}=2\relax
+                 \unskip{} \andname\
+              \else
+                 \unskip \lastandname\
+              \fi}%
+ \def\and{\stepcounter{@auth}\relax
+          \ifnum\value{@auth}=\value{auco}%
+             \lastand
+          \else
+             \unskip,
+          \fi}%
+ \@starttoc{toc}\if@restonecol\twocolumn\fi}
+
+\def\l@part#1#2{\addpenalty{\@secpenalty}%
+   \addvspace{2em plus\p@}%  % space above part line
+   \begingroup
+     \parindent \z@
+     \rightskip \z@ plus 5em
+     \hrule\vskip5pt
+     \large               % same size as for a contribution heading
+     \bfseries\boldmath   % set line in boldface
+     \leavevmode          % TeX command to enter horizontal mode.
+     #1\par
+     \vskip5pt
+     \hrule
+     \vskip1pt
+     \nobreak             % Never break after part entry
+   \endgroup}
+
+\def\@dotsep{2}
+
+\def\hyperhrefextend{\ifx\hyper@anchor\@undefined\else
+{chapter.\thechapter}\fi}
+
+\def\addnumcontentsmark#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{\protect\numberline
+                     {\thechapter}#3}{\thepage}\hyperhrefextend}}
+\def\addcontentsmark#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}\hyperhrefextend}}
+\def\addcontentsmarkwop#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{#3}{0}\hyperhrefextend}}
+
+\def\@adcmk[#1]{\ifcase #1 \or
+\def\@gtempa{\addnumcontentsmark}%
+  \or    \def\@gtempa{\addcontentsmark}%
+  \or    \def\@gtempa{\addcontentsmarkwop}%
+  \fi\@gtempa{toc}{chapter}}
+\def\addtocmark{\@ifnextchar[{\@adcmk}{\@adcmk[3]}}
+
+\def\l@chapter#1#2{\addpenalty{-\@highpenalty}
+ \vskip 1.0em plus 1pt \@tempdima 1.5em \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
+ {\large\bfseries\boldmath#1}\ifx0#2\hfil\null
+ \else
+      \nobreak
+      \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
+      \@dotsep mu$}\hfill
+      \nobreak\hbox to\@pnumwidth{\hss #2}%
+ \fi\par
+ \penalty\@highpenalty \endgroup}
+
+\def\l@title#1#2{\addpenalty{-\@highpenalty}
+ \addvspace{8pt plus 1pt}
+ \@tempdima \z@
+ \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
+ #1\nobreak
+ \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
+ \@dotsep mu$}\hfill
+ \nobreak\hbox to\@pnumwidth{\hss #2}\par
+ \penalty\@highpenalty \endgroup}
+
+\def\l@author#1#2{\addpenalty{\@highpenalty}
+ \@tempdima=\z@ %15\p@
+ \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima %\hskip -\leftskip
+ \textit{#1}\par
+ \penalty\@highpenalty \endgroup}
+
+\setcounter{tocdepth}{0}
+\newdimen\tocchpnum
+\newdimen\tocsecnum
+\newdimen\tocsectotal
+\newdimen\tocsubsecnum
+\newdimen\tocsubsectotal
+\newdimen\tocsubsubsecnum
+\newdimen\tocsubsubsectotal
+\newdimen\tocparanum
+\newdimen\tocparatotal
+\newdimen\tocsubparanum
+\tocchpnum=\z@            % no chapter numbers
+\tocsecnum=15\p@          % section 88. plus 2.222pt
+\tocsubsecnum=23\p@       % subsection 88.8 plus 2.222pt
+\tocsubsubsecnum=27\p@    % subsubsection 88.8.8 plus 1.444pt
+\tocparanum=35\p@         % paragraph 88.8.8.8 plus 1.666pt
+\tocsubparanum=43\p@      % subparagraph 88.8.8.8.8 plus 1.888pt
+\def\calctocindent{%
+\tocsectotal=\tocchpnum
+\advance\tocsectotal by\tocsecnum
+\tocsubsectotal=\tocsectotal
+\advance\tocsubsectotal by\tocsubsecnum
+\tocsubsubsectotal=\tocsubsectotal
+\advance\tocsubsubsectotal by\tocsubsubsecnum
+\tocparatotal=\tocsubsubsectotal
+\advance\tocparatotal by\tocparanum}
+\calctocindent
+
+\def\l@section{\@dottedtocline{1}{\tocchpnum}{\tocsecnum}}
+\def\l@subsection{\@dottedtocline{2}{\tocsectotal}{\tocsubsecnum}}
+\def\l@subsubsection{\@dottedtocline{3}{\tocsubsectotal}{\tocsubsubsecnum}}
+\def\l@paragraph{\@dottedtocline{4}{\tocsubsubsectotal}{\tocparanum}}
+\def\l@subparagraph{\@dottedtocline{5}{\tocparatotal}{\tocsubparanum}}
+
+\def\listoffigures{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
+ \fi\section*{\listfigurename\@mkboth{{\listfigurename}}{{\listfigurename}}}
+ \@starttoc{lof}\if@restonecol\twocolumn\fi}
+\def\l@figure{\@dottedtocline{1}{0em}{1.5em}}
+
+\def\listoftables{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
+ \fi\section*{\listtablename\@mkboth{{\listtablename}}{{\listtablename}}}
+ \@starttoc{lot}\if@restonecol\twocolumn\fi}
+\let\l@table\l@figure
+
+\renewcommand\listoffigures{%
+    \section*{\listfigurename
+      \@mkboth{\listfigurename}{\listfigurename}}%
+    \@starttoc{lof}%
+    }
+
+\renewcommand\listoftables{%
+    \section*{\listtablename
+      \@mkboth{\listtablename}{\listtablename}}%
+    \@starttoc{lot}%
+    }
+
+\ifx\oribibl\undefined
+\ifx\citeauthoryear\undefined
+\renewenvironment{thebibliography}[1]
+     {\section*{\refname}
+      \def\@biblabel##1{##1.}
+      \small
+      \list{\@biblabel{\@arabic\c@enumiv}}%
+           {\settowidth\labelwidth{\@biblabel{#1}}%
+            \leftmargin\labelwidth
+            \advance\leftmargin\labelsep
+            \if@openbib
+              \advance\leftmargin\bibindent
+              \itemindent -\bibindent
+              \listparindent \itemindent
+              \parsep \z@
+            \fi
+            \usecounter{enumiv}%
+            \let\p@enumiv\@empty
+            \renewcommand\theenumiv{\@arabic\c@enumiv}}%
+      \if@openbib
+        \renewcommand\newblock{\par}%
+      \else
+        \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
+      \fi
+      \sloppy\clubpenalty4000\widowpenalty4000%
+      \sfcode`\.=\@m}
+     {\def\@noitemerr
+       {\@latex@warning{Empty `thebibliography' environment}}%
+      \endlist}
+\def\@lbibitem[#1]#2{\item[{[#1]}\hfill]\if@filesw
+     {\let\protect\noexpand\immediate
+     \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
+\newcount\@tempcntc
+\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi
+  \@tempcnta\z@\@tempcntb\m@ne\def\@citea{}\@cite{\@for\@citeb:=#2\do
+    {\@ifundefined
+       {b@\@citeb}{\@citeo\@tempcntb\m@ne\@citea\def\@citea{,}{\bfseries
+        ?}\@warning
+       {Citation `\@citeb' on page \thepage \space undefined}}%
+    {\setbox\z@\hbox{\global\@tempcntc0\csname b@\@citeb\endcsname\relax}%
+     \ifnum\@tempcntc=\z@ \@citeo\@tempcntb\m@ne
+       \@citea\def\@citea{,}\hbox{\csname b@\@citeb\endcsname}%
+     \else
+      \advance\@tempcntb\@ne
+      \ifnum\@tempcntb=\@tempcntc
+      \else\advance\@tempcntb\m@ne\@citeo
+      \@tempcnta\@tempcntc\@tempcntb\@tempcntc\fi\fi}}\@citeo}{#1}}
+\def\@citeo{\ifnum\@tempcnta>\@tempcntb\else
+               \@citea\def\@citea{,\,\hskip\z@skip}%
+               \ifnum\@tempcnta=\@tempcntb\the\@tempcnta\else
+               {\advance\@tempcnta\@ne\ifnum\@tempcnta=\@tempcntb \else
+                \def\@citea{--}\fi
+      \advance\@tempcnta\m@ne\the\@tempcnta\@citea\the\@tempcntb}\fi\fi}
+\else
+\renewenvironment{thebibliography}[1]
+     {\section*{\refname}
+      \small
+      \list{}%
+           {\settowidth\labelwidth{}%
+            \leftmargin\parindent
+            \itemindent=-\parindent
+            \labelsep=\z@
+            \if@openbib
+              \advance\leftmargin\bibindent
+              \itemindent -\bibindent
+              \listparindent \itemindent
+              \parsep \z@
+            \fi
+            \usecounter{enumiv}%
+            \let\p@enumiv\@empty
+            \renewcommand\theenumiv{}}%
+      \if@openbib
+        \renewcommand\newblock{\par}%
+      \else
+        \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
+      \fi
+      \sloppy\clubpenalty4000\widowpenalty4000%
+      \sfcode`\.=\@m}
+     {\def\@noitemerr
+       {\@latex@warning{Empty `thebibliography' environment}}%
+      \endlist}
+      \def\@cite#1{#1}%
+      \def\@lbibitem[#1]#2{\item[]\if@filesw
+        {\def\protect##1{\string ##1\space}\immediate
+      \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
+   \fi
+\else
+\@cons\@openbib@code{\noexpand\small}
+\fi
+
+\def\idxquad{\hskip 10\p@}% space that divides entry from number
+
+\def\@idxitem{\par\hangindent 10\p@}
+
+\def\subitem{\par\setbox0=\hbox{--\enspace}% second order
+                \noindent\hangindent\wd0\box0}% index entry
+
+\def\subsubitem{\par\setbox0=\hbox{--\,--\enspace}% third
+                \noindent\hangindent\wd0\box0}% order index entry
+
+\def\indexspace{\par \vskip 10\p@ plus5\p@ minus3\p@\relax}
+
+\renewenvironment{theindex}
+               {\@mkboth{\indexname}{\indexname}%
+                \thispagestyle{empty}\parindent\z@
+                \parskip\z@ \@plus .3\p@\relax
+                \let\item\par
+                \def\,{\relax\ifmmode\mskip\thinmuskip
+                             \else\hskip0.2em\ignorespaces\fi}%
+                \normalfont\small
+                \begin{multicols}{2}[\@makeschapterhead{\indexname}]%
+                }
+                {\end{multicols}}
+
+\renewcommand\footnoterule{%
+  \kern-3\p@
+  \hrule\@width 2truecm
+  \kern2.6\p@}
+  \newdimen\fnindent
+  \fnindent1em
+\long\def\@makefntext#1{%
+    \parindent \fnindent%
+    \leftskip \fnindent%
+    \noindent
+    \llap{\hb@xt@1em{\hss\@makefnmark\ }}\ignorespaces#1}
+
+\long\def\@makecaption#1#2{%
+  \vskip\abovecaptionskip
+  \sbox\@tempboxa{{\bfseries #1.} #2}%
+  \ifdim \wd\@tempboxa >\hsize
+    {\bfseries #1.} #2\par
+  \else
+    \global \@minipagefalse
+    \hb@xt@\hsize{\hfil\box\@tempboxa\hfil}%
+  \fi
+  \vskip\belowcaptionskip}
+
+\def\fps@figure{htbp}
+\def\fnum@figure{\figurename\thinspace\thefigure}
+\def \@floatboxreset {%
+        \reset@font
+        \small
+        \@setnobreak
+        \@setminipage
+}
+\def\fps@table{htbp}
+\def\fnum@table{\tablename~\thetable}
+\renewenvironment{table}
+               {\setlength\abovecaptionskip{0\p@}%
+                \setlength\belowcaptionskip{10\p@}%
+                \@float{table}}
+               {\end@float}
+\renewenvironment{table*}
+               {\setlength\abovecaptionskip{0\p@}%
+                \setlength\belowcaptionskip{10\p@}%
+                \@dblfloat{table}}
+               {\end@dblfloat}
+
+\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname
+  ext@#1\endcsname}{#1}{\protect\numberline{\csname
+  the#1\endcsname}{\ignorespaces #2}}\begingroup
+    \@parboxrestore
+    \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
+  \endgroup}
+
+% LaTeX does not provide a command to enter the authors institute
+% addresses. The \institute command is defined here.
+
+\newcounter{@inst}
+\newcounter{@auth}
+\newcounter{auco}
+\newdimen\instindent
+\newbox\authrun
+\newtoks\authorrunning
+\newtoks\tocauthor
+\newbox\titrun
+\newtoks\titlerunning
+\newtoks\toctitle
+
+\def\clearheadinfo{\gdef\@author{No Author Given}%
+                   \gdef\@title{No Title Given}%
+                   \gdef\@subtitle{}%
+                   \gdef\@institute{No Institute Given}%
+                   \gdef\@thanks{}%
+                   \global\titlerunning={}\global\authorrunning={}%
+                   \global\toctitle={}\global\tocauthor={}}
+
+\def\institute#1{\gdef\@institute{#1}}
+
+\def\institutename{\par
+ \begingroup
+ \parskip=\z@
+ \parindent=\z@
+ \setcounter{@inst}{1}%
+ \def\and{\par\stepcounter{@inst}%
+ \noindent$^{\the@inst}$\enspace\ignorespaces}%
+ \setbox0=\vbox{\def\thanks##1{}\@institute}%
+ \ifnum\c@@inst=1\relax
+   \gdef\fnnstart{0}%
+ \else
+   \xdef\fnnstart{\c@@inst}%
+   \setcounter{@inst}{1}%
+   \noindent$^{\the@inst}$\enspace
+ \fi
+ \ignorespaces
+ \@institute\par
+ \endgroup}
+
+\def\@fnsymbol#1{\ensuremath{\ifcase#1\or\star\or{\star\star}\or
+   {\star\star\star}\or \dagger\or \ddagger\or
+   \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger
+   \or \ddagger\ddagger \else\@ctrerr\fi}}
+
+\def\inst#1{\unskip$^{#1}$}
+\def\fnmsep{\unskip$^,$}
+\def\email#1{{\tt#1}}
+\AtBeginDocument{\@ifundefined{url}{\def\url#1{#1}}{}%
+\@ifpackageloaded{babel}{%
+\@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}%
+\@ifundefined{extrasfrenchb}{}{\addto\extrasfrenchb{\switcht@francais}}%
+\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}%
+}{\switcht@@therlang}%
+}
+\def\homedir{\~{ }}
+
+\def\subtitle#1{\gdef\@subtitle{#1}}
+\clearheadinfo
+
+\renewcommand\maketitle{\newpage
+  \refstepcounter{chapter}%
+  \stepcounter{section}%
+  \setcounter{section}{0}%
+  \setcounter{subsection}{0}%
+  \setcounter{figure}{0}
+  \setcounter{table}{0}
+  \setcounter{equation}{0}
+  \setcounter{footnote}{0}%
+  \begingroup
+    \parindent=\z@
+    \renewcommand\thefootnote{\@fnsymbol\c@footnote}%
+    \if@twocolumn
+      \ifnum \col@number=\@ne
+        \@maketitle
+      \else
+        \twocolumn[\@maketitle]%
+      \fi
+    \else
+      \newpage
+      \global\@topnum\z@   % Prevents figures from going at top of page.
+      \@maketitle
+    \fi
+    \thispagestyle{empty}\@thanks
+%
+    \def\\{\unskip\ \ignorespaces}\def\inst##1{\unskip{}}%
+    \def\thanks##1{\unskip{}}\def\fnmsep{\unskip}%
+    \instindent=\hsize
+    \advance\instindent by-\headlineindent
+    \if!\the\toctitle!\addcontentsline{toc}{title}{\@title}\else
+       \addcontentsline{toc}{title}{\the\toctitle}\fi
+    \if@runhead
+       \if!\the\titlerunning!\else
+         \edef\@title{\the\titlerunning}%
+       \fi
+       \global\setbox\titrun=\hbox{\small\rm\unboldmath\ignorespaces\@title}%
+       \ifdim\wd\titrun>\instindent
+          \typeout{Title too long for running head. Please supply}%
+          \typeout{a shorter form with \string\titlerunning\space prior to
+                   \string\maketitle}%
+          \global\setbox\titrun=\hbox{\small\rm
+          Title Suppressed Due to Excessive Length}%
+       \fi
+       \xdef\@title{\copy\titrun}%
+    \fi
+%
+    \if!\the\tocauthor!\relax
+      {\def\and{\noexpand\protect\noexpand\and}%
+      \protected@xdef\toc@uthor{\@author}}%
+    \else
+      \def\\{\noexpand\protect\noexpand\newline}%
+      \protected@xdef\scratch{\the\tocauthor}%
+      \protected@xdef\toc@uthor{\scratch}%
+    \fi
+    \addcontentsline{toc}{author}{\toc@uthor}%
+    \if@runhead
+       \if!\the\authorrunning!
+         \value{@inst}=\value{@auth}%
+         \setcounter{@auth}{1}%
+       \else
+         \edef\@author{\the\authorrunning}%
+       \fi
+       \global\setbox\authrun=\hbox{\small\unboldmath\@author\unskip}%
+       \ifdim\wd\authrun>\instindent
+          \typeout{Names of authors too long for running head. Please supply}%
+          \typeout{a shorter form with \string\authorrunning\space prior to
+                   \string\maketitle}%
+          \global\setbox\authrun=\hbox{\small\rm
+          Authors Suppressed Due to Excessive Length}%
+       \fi
+       \xdef\@author{\copy\authrun}%
+       \markboth{\@author}{\@title}%
+     \fi
+  \endgroup
+  \setcounter{footnote}{\fnnstart}%
+  \clearheadinfo}
+%
+\def\@maketitle{\newpage
+ \markboth{}{}%
+ \def\lastand{\ifnum\value{@inst}=2\relax
+                 \unskip{} \andname\
+              \else
+                 \unskip \lastandname\
+              \fi}%
+ \def\and{\stepcounter{@auth}\relax
+          \ifnum\value{@auth}=\value{@inst}%
+             \lastand
+          \else
+             \unskip,
+          \fi}%
+ \begin{center}%
+ \let\newline\\
+ {\Large \bfseries\boldmath
+  \pretolerance=10000
+  \@title \par}\vskip .8cm
+\if!\@subtitle!\else {\large \bfseries\boldmath
+  \vskip -.65cm
+  \pretolerance=10000
+  \@subtitle \par}\vskip .8cm\fi
+ \setbox0=\vbox{\setcounter{@auth}{1}\def\and{\stepcounter{@auth}}%
+ \def\thanks##1{}\@author}%
+ \global\value{@inst}=\value{@auth}%
+ \global\value{auco}=\value{@auth}%
+ \setcounter{@auth}{1}%
+{\lineskip .5em
+\noindent\ignorespaces
+\@author\vskip.35cm}
+ {\small\institutename}
+ \end{center}%
+ }
+
+% definition of the "\spnewtheorem" command.
+%
+% Usage:
+%
+%     \spnewtheorem{env_nam}{caption}[within]{cap_font}{body_font}
+% or  \spnewtheorem{env_nam}[numbered_like]{caption}{cap_font}{body_font}
+% or  \spnewtheorem*{env_nam}{caption}{cap_font}{body_font}
+%
+% New is "cap_font" and "body_font". It stands for
+% fontdefinition of the caption and the text itself.
+%
+% "\spnewtheorem*" gives a theorem without number.
+%
+% A defined spnewthoerem environment is used as described
+% by Lamport.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\@thmcountersep{}
+\def\@thmcounterend{.}
+
+\def\spnewtheorem{\@ifstar{\@sthm}{\@Sthm}}
+
+% definition of \spnewtheorem with number
+
+\def\@spnthm#1#2{%
+  \@ifnextchar[{\@spxnthm{#1}{#2}}{\@spynthm{#1}{#2}}}
+\def\@Sthm#1{\@ifnextchar[{\@spothm{#1}}{\@spnthm{#1}}}
+
+\def\@spxnthm#1#2[#3]#4#5{\expandafter\@ifdefinable\csname #1\endcsname
+   {\@definecounter{#1}\@addtoreset{#1}{#3}%
+   \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand
+     \csname the#3\endcsname \noexpand\@thmcountersep \@thmcounter{#1}}%
+   \expandafter\xdef\csname #1name\endcsname{#2}%
+   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}%
+                              \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@spynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
+   {\@definecounter{#1}%
+   \expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
+   \expandafter\xdef\csname #1name\endcsname{#2}%
+   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#3}{#4}}%
+                               \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@spothm#1[#2]#3#4#5{%
+  \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}%
+  {\expandafter\@ifdefinable\csname #1\endcsname
+  {\global\@namedef{the#1}{\@nameuse{the#2}}%
+  \expandafter\xdef\csname #1name\endcsname{#3}%
+  \global\@namedef{#1}{\@spthm{#2}{\csname #1name\endcsname}{#4}{#5}}%
+  \global\@namedef{end#1}{\@endtheorem}}}}
+
+\def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@
+\refstepcounter{#1}%
+\@ifnextchar[{\@spythm{#1}{#2}{#3}{#4}}{\@spxthm{#1}{#2}{#3}{#4}}}
+
+\def\@spxthm#1#2#3#4{\@spbegintheorem{#2}{\csname the#1\endcsname}{#3}{#4}%
+                    \ignorespaces}
+
+\def\@spythm#1#2#3#4[#5]{\@spopargbegintheorem{#2}{\csname
+       the#1\endcsname}{#5}{#3}{#4}\ignorespaces}
+
+\def\@spbegintheorem#1#2#3#4{\trivlist
+                 \item[\hskip\labelsep{#3#1\ #2\@thmcounterend}]#4}
+
+\def\@spopargbegintheorem#1#2#3#4#5{\trivlist
+      \item[\hskip\labelsep{#4#1\ #2}]{#4(#3)\@thmcounterend\ }#5}
+
+% definition of \spnewtheorem* without number
+
+\def\@sthm#1#2{\@Ynthm{#1}{#2}}
+
+\def\@Ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
+   {\global\@namedef{#1}{\@Thm{\csname #1name\endcsname}{#3}{#4}}%
+    \expandafter\xdef\csname #1name\endcsname{#2}%
+    \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@
+\@ifnextchar[{\@Ythm{#1}{#2}{#3}}{\@Xthm{#1}{#2}{#3}}}
+
+\def\@Xthm#1#2#3{\@Begintheorem{#1}{#2}{#3}\ignorespaces}
+
+\def\@Ythm#1#2#3[#4]{\@Opargbegintheorem{#1}
+       {#4}{#2}{#3}\ignorespaces}
+
+\def\@Begintheorem#1#2#3{#3\trivlist
+                           \item[\hskip\labelsep{#2#1\@thmcounterend}]}
+
+\def\@Opargbegintheorem#1#2#3#4{#4\trivlist
+      \item[\hskip\labelsep{#3#1}]{#3(#2)\@thmcounterend\ }}
+
+\if@envcntsect
+   \def\@thmcountersep{.}
+   \spnewtheorem{theorem}{Theorem}[section]{\bfseries}{\itshape}
+\else
+   \spnewtheorem{theorem}{Theorem}{\bfseries}{\itshape}
+   \if@envcntreset
+      \@addtoreset{theorem}{section}
+   \else
+      \@addtoreset{theorem}{chapter}
+   \fi
+\fi
+
+%definition of divers theorem environments
+\spnewtheorem*{claim}{Claim}{\itshape}{\rmfamily}
+\spnewtheorem*{proof}{Proof}{\itshape}{\rmfamily}
+\if@envcntsame % alle Umgebungen wie Theorem.
+   \def\spn@wtheorem#1#2#3#4{\@spothm{#1}[theorem]{#2}{#3}{#4}}
+\else % alle Umgebungen mit eigenem Zaehler
+   \if@envcntsect % mit section numeriert
+      \def\spn@wtheorem#1#2#3#4{\@spxnthm{#1}{#2}[section]{#3}{#4}}
+   \else % nicht mit section numeriert
+      \if@envcntreset
+         \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
+                                   \@addtoreset{#1}{section}}
+      \else
+         \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
+                                   \@addtoreset{#1}{chapter}}%
+      \fi
+   \fi
+\fi
+\spn@wtheorem{case}{Case}{\itshape}{\rmfamily}
+\spn@wtheorem{conjecture}{Conjecture}{\itshape}{\rmfamily}
+\spn@wtheorem{corollary}{Corollary}{\bfseries}{\itshape}
+\spn@wtheorem{definition}{Definition}{\bfseries}{\itshape}
+\spn@wtheorem{example}{Example}{\itshape}{\rmfamily}
+\spn@wtheorem{exercise}{Exercise}{\itshape}{\rmfamily}
+\spn@wtheorem{lemma}{Lemma}{\bfseries}{\itshape}
+\spn@wtheorem{note}{Note}{\itshape}{\rmfamily}
+\spn@wtheorem{problem}{Problem}{\itshape}{\rmfamily}
+\spn@wtheorem{property}{Property}{\itshape}{\rmfamily}
+\spn@wtheorem{proposition}{Proposition}{\bfseries}{\itshape}
+\spn@wtheorem{question}{Question}{\itshape}{\rmfamily}
+\spn@wtheorem{solution}{Solution}{\itshape}{\rmfamily}
+\spn@wtheorem{remark}{Remark}{\itshape}{\rmfamily}
+
+\def\@takefromreset#1#2{%
+    \def\@tempa{#1}%
+    \let\@tempd\@elt
+    \def\@elt##1{%
+        \def\@tempb{##1}%
+        \ifx\@tempa\@tempb\else
+            \@addtoreset{##1}{#2}%
+        \fi}%
+    \expandafter\expandafter\let\expandafter\@tempc\csname cl@#2\endcsname
+    \expandafter\def\csname cl@#2\endcsname{}%
+    \@tempc
+    \let\@elt\@tempd}
+
+\def\theopargself{\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
+      \item[\hskip\labelsep{##4##1\ ##2}]{##4##3\@thmcounterend\ }##5}
+                  \def\@Opargbegintheorem##1##2##3##4{##4\trivlist
+      \item[\hskip\labelsep{##3##1}]{##3##2\@thmcounterend\ }}
+      }
+
+\renewenvironment{abstract}{%
+      \list{}{\advance\topsep by0.35cm\relax\small
+      \leftmargin=1cm
+      \labelwidth=\z@
+      \listparindent=\z@
+      \itemindent\listparindent
+      \rightmargin\leftmargin}\item[\hskip\labelsep
+                                    \bfseries\abstractname]}
+    {\endlist}
+
+\newdimen\headlineindent             % dimension for space between
+\headlineindent=1.166cm              % number and text of headings.
+
+\def\ps@headings{\let\@mkboth\@gobbletwo
+   \let\@oddfoot\@empty\let\@evenfoot\@empty
+   \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
+                  \leftmark\hfil}
+   \def\@oddhead{\normalfont\small\hfil\rightmark\hspace{\headlineindent}%
+                 \llap{\thepage}}
+   \def\chaptermark##1{}%
+   \def\sectionmark##1{}%
+   \def\subsectionmark##1{}}
+
+\def\ps@titlepage{\let\@mkboth\@gobbletwo
+   \let\@oddfoot\@empty\let\@evenfoot\@empty
+   \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
+                  \hfil}
+   \def\@oddhead{\normalfont\small\hfil\hspace{\headlineindent}%
+                 \llap{\thepage}}
+   \def\chaptermark##1{}%
+   \def\sectionmark##1{}%
+   \def\subsectionmark##1{}}
+
+\if@runhead\ps@headings\else
+\ps@empty\fi
+
+\setlength\arraycolsep{1.4\p@}
+\setlength\tabcolsep{1.4\p@}
+
+\endinput
+%end of file llncs.cls

diff --git a/helm/mathql/doc/mathql.tex b/helm/mathql/doc/mathql.tex
index 1dde6905fe32bfff176a73f61bb31ede7c80a081..ed9a96021736fa05b3ea5c2426e8f9ece81ea998 100644 (file)
--- a/helm/mathql/doc/mathql.tex
+++ b/helm/mathql/doc/mathql.tex
@@ -1,27 +1,32 @@
-\documentclass[10pt]{article}
+\documentclass{llncs}

 
 \usepackage{mathql_macros}
 
 
 \usepackage{mathql_macros}
 

-\addtolength{\textheight}{2.5cm}
-\addtolength{\oddsidemargin}{-1.0cm}
-\addtolength{\evensidemargin}{-1.0cm}
-\addtolength{\textwidth}{2.0cm}
-\addtolength{\topmargin}{-1.0cm}
-

 \title{MathQL-1 Version 4\\Reference Documentation}
 \title{MathQL-1 Version 4\\Reference Documentation}

-\author{Ferruccio Guidi}
+\author{Ferruccio Guidi%
+\thanks{This work has been partially supported by
+MoWGLI (European FET Project IST-2001-33562).}
+}
+
+\institute{Department of Computer Science\\
+Mura Anteo Zamboni 7, 40127 Bologna, ITALY.\\
+\email{fguidi@cs.unibo.it}}

 
 

-\bibliographystyle{numeric}
+\date{ }

 
 \begin{document}
 
 \maketitle
 
 
 \begin{document}
 
 \maketitle
 

+\begin{abstract}
+\end{abstract}
+

 \tableofcontents
 
 \input{mathql_overview}
 \input{mathql_introduction}
 \input{mathql_operational}
 \tableofcontents
 
 \input{mathql_overview}
 \input{mathql_introduction}
 \input{mathql_operational}

+\input{mathql_tests}

 \input{mathql_bib}
 
 \end{document}
 \input{mathql_bib}
 
 \end{document}

diff --git a/helm/mathql/doc/mathql_bib.tex b/helm/mathql/doc/mathql_bib.tex
index 32b71ed4077e27cc0d0f6470b08510fa20d80aa2..be28be8ff24f111e8c53eecafbce7e4f22dd5d9f 100644 (file)
--- a/helm/mathql/doc/mathql_bib.tex
+++ b/helm/mathql/doc/mathql_bib.tex
@@ -38,7 +38,6 @@ FrancoAngeli, 1998.
 D. Lordi:
 \emph{Sperimentazione e Sviluppo di Strumenti per la gestione di metadati}. \\
 Master Thesis in Computer Science, University of Bologna, 2002.
 D. Lordi:
 \emph{Sperimentazione e Sviluppo di Strumenti per la gestione di metadati}. \\
 Master Thesis in Computer Science, University of Bologna, 2002.

-Advisor: A. Asperti.

 
 \bibitem {RDF}
 \emph{Resource Description Framework (RDF) Model and Syntax Specification}.
 
 \bibitem {RDF}
 \emph{Resource Description Framework (RDF) Model and Syntax Specification}.

diff --git a/helm/mathql/doc/mathql_introduction.tex b/helm/mathql/doc/mathql_introduction.tex
index 61cc88c0244ba3514408efca64337cbf02a2aad0..0fad196e03dc62ffd389824f17c0fb102e715422 100644 (file)
--- a/helm/mathql/doc/mathql_introduction.tex
+++ b/helm/mathql/doc/mathql_introduction.tex
@@ -1,15 +1,15 @@
-\section{Introduction}
+\section{The language}

 
 This paper presents {\MathQL} version 4 which is the latest version of the
 
 This paper presents {\MathQL} version 4 which is the latest version of the

-language, fully developed by Ferruccio Guidi.  
+language, fully developed by the Author.

 For a description of the previous versions of {\MathQL} see: \cite{Gui03}
 (version 3), \cite{GS03} (version 2), \cite{Lor02} (version 1).
 The main novelties of this version are the elimination of some cast operators
 For a description of the previous versions of {\MathQL} see: \cite{Gui03}
 (version 3), \cite{GS03} (version 2), \cite{Lor02} (version 1).
 The main novelties of this version are the elimination of some cast operators

-(producing a substantial simplification in the query structure and semantics,
-see \secref{Operational}), a clear distinction between the core language and
-the auxiliary functions of the basic library, a support for query generating
-functions, the possibility of extending the language adding new libraries of
-functions and a more uniform textual syntax. 
+(producing a substantial simplification in the query structure and semantics),
+a clear distinction between the core language and the auxiliary functions of
+the basic library, a support for query generating functions, the possibility
+of extending the language adding new libraries of functions and a more uniform
+textual syntax. 

 {\MathQL}.4 incorporates the features of {\MathQL}.3 not documented on paper%
 \footnote
 {See the ``what's new'' section of {\MathQL} Web Site:
 {\MathQL}.4 incorporates the features of {\MathQL}.3 not documented on paper%
 \footnote
 {See the ``what's new'' section of {\MathQL} Web Site:


@@ -21,4 +21,4 @@ the query results.
 \input{mathql_introduction_property}
 \input{mathql_introduction_core}
 \input{mathql_introduction_basic}
 \input{mathql_introduction_property}
 \input{mathql_introduction_core}
 \input{mathql_introduction_basic}

-% \input{mathql_introduction_textual}
+\input{mathql_introduction_textual}

diff --git a/helm/mathql/doc/mathql_introduction_avsets.tex b/helm/mathql/doc/mathql_introduction_avsets.tex
index d9943f1cf95fecb16ea8b8a9aff10c62a0cb014b..20e826403421c1b501b9509c327edc7dd155e540 100644 (file)
--- a/helm/mathql/doc/mathql_introduction_avsets.tex
+++ b/helm/mathql/doc/mathql_introduction_avsets.tex
@@ -1,4 +1,4 @@
-\subsection {Sets of attributed values.}
+\subsection {Sets of attributed values.} \label{AVSets}

 
 The data representation model used by {\MathQL} relies on the notion of 
 \emph{set of attributed values} ({\av} set for short) that is, in practice,
 
 The data representation model used by {\MathQL} relies on the notion of 
 \emph{set of attributed values} ({\av} set for short) that is, in practice,


@@ -10,7 +10,7 @@ should be driven from the {\RDFS} class system. This may be a future
 improvement.}
 Each {\av} in an {\av} set consists of a string% 
 \footnote{When we say \emph{string}, we mean a finite sequence of characters.}
 improvement.}
 Each {\av} in an {\av} set consists of a string% 
 \footnote{When we say \emph{string}, we mean a finite sequence of characters.}

-(that we call the \emph{head string} or \emph{value}) and a (possibly emty)
+(that we call the \emph{head string} or \emph{value}) and a (possibly empty)

 multiset of named attributes whose content is a set of strings.
 Attribute names are made of a (possibly empty) list of string components, so
 they can be hierarchically structured. 
 multiset of named attributes whose content is a set of strings.
 Attribute names are made of a (possibly empty) list of string components, so
 they can be hierarchically structured. 


@@ -18,7 +18,7 @@ Moreover the attributes of a value are partitioned into a set of \emph{groups}
 ({\ie} subsets) to improve its structure.
 
 In the above description a \emph{set} is an \emph{unordered} finite
 ({\ie} subsets) to improve its structure.
 
 In the above description a \emph{set} is an \emph{unordered} finite

-sequence \emph{without} repetitions wheras a \emph{multiset} is an
+sequence \emph{without} repetitions whereas a \emph{multiset} is an

 \emph{unordered} finite sequence \emph{with} repetitions.
 
 In the present context repetitions are defined as follows:
 \emph{unordered} finite sequence \emph{with} repetitions.
 
 In the present context repetitions are defined as follows:


@@ -33,7 +33,7 @@ definition of an {\av} set is just the right one among the many alternatives
 that were tried.} 
 
 As we said, {\MathQL}.4 uses {\av} sets to represent many kinds of
 that were tried.} 
 
 As we said, {\MathQL}.4 uses {\av} sets to represent many kinds of

-information, namely:
+information:

 
 \begin{enumerate}
 
 
 \begin{enumerate}
 


@@ -50,26 +50,25 @@ objects of repeated predicates.
 Moreover structured attribute names can encode various components of
 structured properties preserving their semantics.
 
 Moreover structured attribute names can encode various components of
 structured properties preserving their semantics.
 

-\begin{figure}[ht]
+\begin{figure}

 \begin{footnotesize} \begin{verbatim}
 The RDF triples:
 \begin{footnotesize} \begin{verbatim}
 The RDF triples:

-("http://www.w3.org/2002/01/rdf-databases/protocol", "dc:creator", "Sandro Hawke")
-("http://www.w3.org/2002/01/rdf-databases/protocol", "dc:creator", "Eric Prud'hommeaux")
-("http://www.w3.org/2002/01/rdf-databases/protocol", "dc:date", "2002-01-08")
+ ("protocol", "dc:creator", "Sandro Hawke")
+ ("protocol", "dc:creator", "Eric Prud'hommeaux")
+ ("protocol", "dc:date", "2002-01-08")

 
 The corresponding attributed value:
 
 The corresponding attributed value:

-"http://www.w3.org/2002/01/rdf-databases/protocol" attr
-             {"dc:creator" = {"Sandro Hawke", "Eric Prud'hommeaux"}; "dc:date" = "2002-01-08"}
+ "protocol" attr {/"dc:creator" = {"Sandro Hawke", "Eric Prud'hommeaux"};
+                  /"dc:date" = "2002-01-08"}

 \end{verbatim} \end{footnotesize}
 \end{verbatim} \end{footnotesize}

-\vskip-1pc
+\vspace{-1pc}

 \caption{The representation of a pool of {\RDF} triples} \label{AVOne}
 \end{figure}
 
 \figref{AVOne} shows how a set of triples can be coded in an {\av}.
 \caption{The representation of a pool of {\RDF} triples} \label{AVOne}
 \end{figure}
 
 \figref{AVOne} shows how a set of triples can be coded in an {\av}.

-Note that the word \emph{attr} separates the head string from its attributes,
+Note that the word \TT{attr} separates the head string from its attributes,

 braces enclose an attribute group in which attributes are separated by
 braces enclose an attribute group in which attributes are separated by

-semicolons, and an equal sign separates an attribute name from its contents
-(see \subsecref{Textual} for the complete {\av} syntax).
+semicolons, and an equal sign separates an attribute name from its contents.

 
 In this setting the grouping feature can be used to separate semantically
 different classes of properties associated to a resource (as for instance
 
 In this setting the grouping feature can be used to separate semantically
 different classes of properties associated to a resource (as for instance


@@ -77,7 +76,7 @@ Dublin Core metadata, Euler metadata and user-defined metadata).
 
 \item
 A pool of arbitrarily chosen {\RDF} triples is encoded in an {\av} set 
 
 \item
 A pool of arbitrarily chosen {\RDF} triples is encoded in an {\av} set 

-placing different {\av}'s the subset of triples sharing the same subject.
+placing in each {\av} the subset of triples sharing the same head string.

 
 Note that the use of {\av} sets to build query results allows {\MathQL} queries
 to return sets of {\RDF} triples instead of mere sets of resources, in the
 
 Note that the use of {\av} sets to build query results allows {\MathQL} queries
 to return sets of {\RDF} triples instead of mere sets of resources, in the


@@ -90,22 +89,19 @@ which holds the head strings).
 \figref{Table} shows an {\av} set describing the properties of two resources
 ``A'' and ``B'' giving its table representation, in which the columns
 corresponding to attributes in the same group are clustered between
 \figref{Table} shows an {\av} set describing the properties of two resources
 ``A'' and ``B'' giving its table representation, in which the columns
 corresponding to attributes in the same group are clustered between

-double-line delimiters%
+double-line delimiters.%

 \footnote{A table with grouped labelled columns like the one above resembles a
 \footnote{A table with grouped labelled columns like the one above resembles a

-set of relational database tables.}.   
+set of relational database tables.}   

 
 

-%Another possible use of a {\MathQL} query result is for the encoding of a
-%relational database table: in this sense the indexed column is stored in the
-%subject strings, the names of the other columns are stored in attribute names
-%and cell contents are stored in attribute values.
-
-\begin{figure}[ht]
+\begin{figure}

 \begin{footnotesize} \begin{verbatim}
 \begin{footnotesize} \begin{verbatim}

-"A" attr {"major" = "1"; "minor" = "2"}, {"first" = "2002-01-01"; "modified" = "2002-03-01"};
-"B" attr {"major" = "1"; "minor" = "7"}, {"first" = "2002-02-01"; "modified" = "2002-04-01"}
+"A" attr {/"major" = "1"; /"minor" = "2"}, 
+         {/"first" = "2002-01-01"; /"modified" = "2002-03-01"};
+"B" attr {/"major" = "1"; /"minor" = "7"}, 
+         {/"first" = "2002-02-01"; /"modified" = "2002-04-01"}

 \end{verbatim}
 \begin{center} \begin{tabular}{|c||c|c||c|c||}
 \end{verbatim}
 \begin{center} \begin{tabular}{|c||c|c||c|c||}

-\hline   & {\bf ``major''} & {\bf ``minor''} & {\bf ``first''} & {\bf ``modified''} \\
+\hline   & \textbf{``major''} & \textbf{``minor''} & \textbf{``first''} & \textbf{``modified''} \\

 \hline ``A'' & ``1'' & ``2'' & ``2002-01-01'' & ``2002-03-01'' \\
 \hline ``B'' & ``1'' & ``7'' & ``2002-02-01'' & ``2002-04-01'' \\
 \hline
 \hline ``A'' & ``1'' & ``2'' & ``2002-01-01'' & ``2002-03-01'' \\
 \hline ``B'' & ``1'' & ``7'' & ``2002-02-01'' & ``2002-04-01'' \\
 \hline


@@ -118,15 +114,14 @@ a query result) which fits in 4 dimensions: namely we can extend independently
 the set of the head strings (dimension 1), the attributes in each group
 (dimension 2), the groups in each {\av} (dimension 3) and the contents of each
 attribute (dimension 4).
 the set of the head strings (dimension 1), the attributes in each group
 (dimension 2), the groups in each {\av} (dimension 3) and the contents of each
 attribute (dimension 4).

-

 The metadata defined in the table of \figref{Table} will be used in subsequent
 examples.
 The metadata defined in the table of \figref{Table} will be used in subsequent
 examples.

-For this purpose assume that \TT{first} and \TT{modified} are the components
-of a structured property \TT{date} available for the resources ``A'' and ``B''.
+For this purpose assume that ``first'' and ``modified'' are the components
+of a structured property ``date'' available for the resources ``A'' and ``B''.

 
 \item
 
 \item

-The value of an {\RDF} property is encoded in a single {\av} distinguishing
-three situations:
+The value of an {\RDF} property is encoded in an {\av} distinguishing three
+cases:

 
 \begin{itemize}
 
 
 \begin{itemize}
 


@@ -142,49 +137,49 @@ the content of this component is placed in the {\av} head string and the
 other components are stored in the {\av} attributes as in the case 1.
 
 \item
 other components are stored in the {\av} attributes as in the case 1.
 
 \item

-If the property is structured and its value does not have a main component,
-the {\av} head string is empty and the components are stored in the
-attributes.
+For the value of a structured property without a main component, the head
+string is empty and the components are stored in the attributes.

 
 \end{itemize}
 
 
 \end{itemize}
 

-\begin{figure}[ht]
+\begin{figure}

 \begin{footnotesize} \begin{verbatim}
 First example, one instance:
 \begin{footnotesize} \begin{verbatim}
 First example, one instance:

-"" attr {"major" = "1"; "minor" = "2"};  no main component
-"1" attr {"minor" = "2"};                main component is "major"
-"2" attr {"major" = "1"}                 main component is "minor"
+ "" attr {/"major" = "1"; /"minor" = "2"} no main component
+ "1" attr {/"minor" = "2"} main component is "major"
+ "2" attr {/"major" = "1"} main component is "minor"

 
 Second example: two separate instances:
 
 Second example: two separate instances:

-"" attr {"major" = "1"; "minor" = "2"}, {"major" = "1"; "minor" = "7"}; no main component
-"1" attr {"minor" = "2"}, {"minor" = "7"}                            main component is "major"
+ "" attr {/"major" = "1"; /"minor" = "2"}, 
+         {/"major" = "1"; /"minor" = "7"} no main component
+ "1" attr {/"minor" = "2"}, {/"minor" = "7"} main component is "major"

 
 Third example: two mixed instances:
 
 Third example: two mixed instances:

-"" attr {"major" = "3", "6"; "minor" = "4", "9"} no main component
+ "" attr {/"major" = "3", "6"; /"minor" = {"4", "9"}} no main component

 \end{verbatim} \end{footnotesize}
 \end{verbatim} \end{footnotesize}

-\vskip-1pc
+\vspace{-1pc}

 \caption{The representation of the structured value of a property}
 \label{AVTwo}
 \end{figure}
 
 \figref{AVTwo} (first example) shows three possible ways of representing in
 \caption{The representation of the structured value of a property}
 \label{AVTwo}
 \end{figure}
 
 \figref{AVTwo} (first example) shows three possible ways of representing in

-{\av}'s an instance of a structured property \TT{id} whose value has two
-fields ({\ie} properties) \TT{major} and \TT{minor}.
-In this instance, \TT{major} is set to ``1'' and \TT{minor} is set to ``2''.
-The representations depend on which component of \TT{id} is chosen as the
-main component (none, \TT{major} or \TT{minor} respectively).
+{\av}'s an instance of a structured property ``id'' whose value has two
+fields ({\ie} properties) ``major'' and ``minor''.
+In this instance, ``major'' is set to ``1'' and ``minor'' is set to ``2''.
+The representations depend on which component of ``id'' is chosen as the
+main component (none, ``major'' or ``minor'' respectively).

 Several structured property values sharing a common main component can be
 encodes in a single {\av} exploiting the grouping facility: in this case the
 attributes of every instance are enclosed in separate groups.
 \figref{AVTwo} (second example) shows the representations of two instances of
 Several structured property values sharing a common main component can be
 encodes in a single {\av} exploiting the grouping facility: in this case the
 attributes of every instance are enclosed in separate groups.
 \figref{AVTwo} (second example) shows the representations of two instances of

-\TT{id}: the previous one and a new one for which \TT{major} is ``1'' and
-\TT{minor} is ``7''.
+``id'': the former and a new one for which ``major'' is ``1'' and ``minor'' is
+``7''.

 
 Note that if the attributes of the two groups are encoded in a single group,
 the notion of which components belong to the same property value can not be
 recovered in the general case because the values of an attribute form a set
 
 Note that if the attributes of the two groups are encoded in a single group,
 the notion of which components belong to the same property value can not be
 recovered in the general case because the values of an attribute form a set

-and thus are unordered. \newline
-As an example think of two instances of \TT{id} encoded as in \figref{AVTwo}
+and thus are unordered.
+As an example think of two instances of ``id'' encoded as in \figref{AVTwo}

 (third example).
 
 \item
 (third example).
 
 \item


@@ -199,7 +194,7 @@ head string and no attributes.
 
 \end{enumerate}
 
 
 \end{enumerate}
 

-{\MathQL} defines five binary operations on {\av} sets: two unions, two
+{\MathQL} defines five core binary operations on {\av} sets: two unions, two

 intersections and a difference. The first four are defined in terms of an
 operation, that we call \emph{addition}, involving two {\av}'s with the same
 head string.
 intersections and a difference. The first four are defined in terms of an
 operation, that we call \emph{addition}, involving two {\av}'s with the same
 head string.


@@ -209,47 +204,47 @@ two ways to compose the attribute groups:
 \begin{itemize}
 
 \item
 \begin{itemize}
 
 \item

-With the \emph{set-theoretic} addition, the set of attribute groups in the
+with the \emph{set-theoretic} addition, the set of attribute groups in the

 resulting {\av} is the set-theoretic union of the sets of attribute groups in
 resulting {\av} is the set-theoretic union of the sets of attribute groups in

-the operands.
+the operands;

 
 \item
 
 \item

-With the \emph{distributive} addition, the set of attribute groups in the
+with the \emph{distributive} addition, the set of attribute groups in the

 resulting {\av} is the ``Cartesian product'' of the sets of attribute groups
 in the two operands. 
 resulting {\av} is the ``Cartesian product'' of the sets of attribute groups
 in the two operands. 

-In this context, an element of the ``Cartesian product'' is not a pair of
-groups but it is the set-theoretic union of these groups where the contents of
-homonymous attributes are clustered together using set-theoretic unions.
+Here an element of the ``Cartesian product'' is not a pair of groups but it is
+the set-theoretic union of these groups where the contents of homonymous
+attributes are clustered together using set-theoretic unions.

 
 \end{itemize}
 
 \figref{Addition} shows an example of the two kinds of addition.
 
 
 \end{itemize}
 
 \figref{Addition} shows an example of the two kinds of addition.
 

-\begin{figure}[ht]
+\begin{figure}

 \begin{footnotesize} \begin{verbatim}
 Attributed values used as operands for the addition:
 \begin{footnotesize} \begin{verbatim}
 Attributed values used as operands for the addition:

-"1" attr {"A" = "a"}, {"B" = "b1"}
-"1" attr {"A" = "a"}, {"B" = "b2"}
+ "1" attr {/"A" = "a"}, {/"B" = "b1"}
+ "1" attr {/"A" = "a"}, {/"B" = "b2"}

 
 Set-theoretic addition:
 
 Set-theoretic addition:

-"1" attr {"A" = "a"}, {"B" = "b1"}, {"B" = "b2"}
+" 1" attr {/"A" = "a"}, {/"B" = "b1"}, {/"B" = "b2"}

 
 Distributive addition:
 
 Distributive addition:

-"1" attr {"A" = "a"}, {"A" = "a"; "B" = "b2"}, {"B" = "b1"; "A" = "a"}, {"B" = {"b1", "b2"}}
+ "1" attr {/"A" = "a"}, {/"A" = "a"; /"B" = "b2"}, 
+          {/"B" = "b1"; /"A" = "a"}, {/"B" = {"b1", "b2"}}

 \end{verbatim} \end{footnotesize}
 \end{verbatim} \end{footnotesize}

-\vskip-1pc
+\vspace{-1pc}

 \caption{The addition of attributed values}
 \label{Addition}
 \end{figure}
 
 \caption{The addition of attributed values}
 \label{Addition}
 \end{figure}
 

-Now we can discuss the five operations between {\av} sets that we mentioned
-above:
+Now we can discuss the five operations between {\av} sets:

 
 \begin{itemize}
 
 \item
 
 \begin{itemize}
 
 \item

-The two unions ocorresponds to the set-theoretic union of their operand where
-the {\av}'s sharing the head string are are added either set-theoretically or
+The two unions corresponds to the set-theoretic union of their operand where
+the {\av}'s sharing the head string are added either set-theoretically or

 distributively as explained above (thus we have a set-theoretic union and a
 distributive union in the two cases). In this context the empty {\av} set
 plays the role of the neutral element. 
 distributively as explained above (thus we have a set-theoretic union and a
 distributive union in the two cases). In this context the empty {\av} set
 plays the role of the neutral element. 


@@ -258,8 +253,8 @@ compose the attributes of the operands preserving their group structure.
 
 \item
 The two intersections are the dual of the above unions: they contain the
 
 \item
 The two intersections are the dual of the above unions: they contain the

-{\av}'s whose head string appears in each argument where {\av}'s sharing the
-head string are added either set-theoretically or distributively as before.
+{\av}'s whose head string appears in each argument where the {\av}'s sharing
+the head string are added either set-theoretically or distributively as before.

 
 The distributive intersection has the double benefit of filtering the
 common values of the given {\av} sets, and of merging their attribute groups
 
 The distributive intersection has the double benefit of filtering the
 common values of the given {\av} sets, and of merging their attribute groups


@@ -274,28 +269,28 @@ argument whose head string does not appear in the second argument.
 
 \figref{Binary} shows how the above operations work in a simple example.
 
 
 \figref{Binary} shows how the above operations work in a simple example.
 

-\begin{figure}[ht]
+\begin{figure}

 \begin{footnotesize} \begin{verbatim}
 Sets of attributed values used as operands for the operations:
 \begin{footnotesize} \begin{verbatim}
 Sets of attributed values used as operands for the operations:

-"1" attr {"A" = "a"}; "2" attr {"B" = "b1"} 
-"2" attr {"B" = "b2"}
+ "1" attr {/"A" = "a"}; "2" attr {/"B" = "b1"} 
+ "2" attr {/"B" = "b2"}

 
 Set-theoretic union:
 
 Set-theoretic union:

-"1" attr {"A" = "a"}; "2" attr {"B" = "b1"}, {"B" = "b2"}
+ "1" attr {/"A" = "a"}; "2" attr {/"B" = "b1"}, {/"B" = "b2"}

 
 Distributive union:
 
 Distributive union:

-"1" attr {"A" = "a"}; "2" attr {"B" = {"b1", "b2"}}
+ "1" attr {/"A" = "a"}; "2" attr {/"B" = {"b1", "b2"}}

 
 Set-theoretic intersection:
 
 Set-theoretic intersection:

-"2" attr {"B" = "b1"}, {"B" = "b2"}
+ "2" attr {/"B" = "b1"}, {/"B" = "b2"}

 
 Distributive intersection:
 
 Distributive intersection:

-"2" attr {"B" = {"b1", "b2"}}
+ "2" attr {/"B" = {"b1", "b2"}}

 
 Difference:
 
 Difference:

-"1" attr {"A" = "a"}
+ "1" attr {/"A" = "a"}

 \end{verbatim} \end{footnotesize}
 \end{verbatim} \end{footnotesize}

-\vskip-1pc
+\vspace{-1pc}

 \caption{The binary operations on sets of attributed values}
 \label{Binary}
 \end{figure}
 \caption{The binary operations on sets of attributed values}
 \label{Binary}
 \end{figure}

diff --git a/helm/mathql/doc/mathql_introduction_basic.tex b/helm/mathql/doc/mathql_introduction_basic.tex
new file mode 100644 (file)
index 0000000..ccf13f2
--- /dev/null
+++ b/helm/mathql/doc/mathql_introduction_basic.tex
@@ -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}
+

diff --git a/helm/mathql/doc/mathql_introduction_core.tex b/helm/mathql/doc/mathql_introduction_core.tex
index c277f1852918461e2e2848a9d631261eb51b985e..05f9e9fd93f8836e90b6e90c0a676171557a7a28 100644 (file)
--- a/helm/mathql/doc/mathql_introduction_core.tex
+++ b/helm/mathql/doc/mathql_introduction_core.tex
@@ -3,107 +3,96 @@
 {\MathQL}.4 consists of a core language and of a basic library. Other
 user-defined libraries can be added at will. The core language includes the
 \TT{property} operator mentioned in \subsecref{HighAccess} that queries the
 {\MathQL}.4 consists of a core language and of a basic library. Other
 user-defined libraries can be added at will. The core language includes the
 \TT{property} operator mentioned in \subsecref{HighAccess} that queries the

-underlying {\RDF} database and the infrastructure to post-process the
+underlying {\RDF} database, and the infrastructure to post-process the

 query results. The components of this infrastructure are listed below:
 
 \begin{itemize}
 
 \item 
 query results. The components of this infrastructure are listed below:
 
 \begin{itemize}
 
 \item 

-Explicit sets of attributed values.
-
+\textbf{Explicit sets of attributed values.}

 An explicit {\av} set can be placed in a query in two forms: 
 An explicit {\av} set can be placed in a query in two forms: 

-as a single quoted string, like \verb+"this is a query result"+, that
-evaluates in a single {\av} with that value and no attributes, or as a full
-{\av} set in the syntax shown in the previous sections but sorrounded by
-square brackets, like \verb+["head" attr {"attribute-name" = "contents"}]+.
-\newline
-In the second form, the contents of an attribute can be the result of a query,
-like
-\verb+["head" attr {"attribute-name" = property /"metadata" of "resource"}]+.
+as a quoted string, like \verb+"this is a query result"+, that evaluates in a
+single {\av} with that value and no attributes, or as a full {\av} set in the
+syntax shown in the previous sections but surrounded by square brackets, like 
+\verb+["head" attr {/"attribute" = "contents"}]+.

 \newline
 \newline

-In this case the contents of the attribute are the head strings of the query
-result, whose attributes (if any) are discarded. 
+In the second form, the contents of an attribute can be the result of a query
+and in this case the contents of the attribute are the head strings of the
+query result, whose attributes (if any) are discarded. 
+\end{itemize}

 
 

-\item 
-Variable assignment.
+\begin{center}
+\verb+["head" attr {/"attribute" = property /"metadata" of "resource"}]+
+\end{center}
+
+\begin{itemize}

 
 

+\item 
+\textbf{Variable assignment.}

 Variables for {\av} sets (preceded by a \TT{\$} sign and called
 \emph{set variables}) can be assigned using a standard \emph{let-in}
 construction and may appear wherever an {\av} set ({\ie} a query result) is
 allowed.  
 Variables for {\av} sets (preceded by a \TT{\$} sign and called
 \emph{set variables}) can be assigned using a standard \emph{let-in}
 construction and may appear wherever an {\av} set ({\ie} a query result) is
 allowed.  

-\newline

 The assignment has the form: 
 \TT{let \$}\EM{variable} \TT{=} \EM{av-set} \TT{in} \EM{av-set}
 so we can write:
 \newline
 The assignment has the form: 
 \TT{let \$}\EM{variable} \TT{=} \EM{av-set} \TT{in} \EM{av-set}
 so we can write:
 \newline

-\verb+let $var = "contents" in ["head" attr {"attribute-name" = $var}]+.
+\verb+let $var = "contents" in ["head" attr {/"attribute" = $var}]+.

 
 

-The scope rules of {\MathQL} variables are tipical for an imperative
-programming language and any case of assignment propagation will be indicated.
+The scope of {\MathQL} variables is typical for an imperative programming
+language and any case of assignment propagation will be indicated.

 
 \item 
 
 \item 

-Sequential composition.
-
+\textbf{Sequential composition.}

 This construction has the form: \EM{av-set} \TT{;;} \EM{av-set} and works as
 follows: the two {\av} sets are evaluated one after the other and the first
 one is discarded but the variables assigned in the first {\av} set are
 available to the second one.  
 
 \item 
 This construction has the form: \EM{av-set} \TT{;;} \EM{av-set} and works as
 follows: the two {\av} sets are evaluated one after the other and the first
 one is discarded but the variables assigned in the first {\av} set are
 available to the second one.  
 
 \item 

-Unbounded iteration.
-\newline
+\textbf{Unbounded iteration.}

 This construction comes in two forms:
 
 This construction comes in two forms:
 

-\TT{while} \EM{av-set} \TT{sup} \EM{av-set}:
-\newline
-iterates the evaluation of the second {\av} set until the first {\av set} is
-empty and returns the {\MathQL} set-theoretic union of all the evaluiations
-of the second {\av set}.
-
-\TT{while} \EM{av-set} \TT{inf} \EM{av-set}:
-\newline
-like the former but set-theoretic intersection is used instead of
+\TT{while} \EM{av-set-1} \TT{sup} \EM{av-set-2}:
+iterates the evaluation of \EM{av-set-2} until \EM{av-set-1} is empty and
+returns the {\MathQL} set-theoretic union of all the evaluations of
+\EM{av-set-2}.
+\TT{while} \EM{av-set-1} \TT{inf} \EM{av-set-2}:
+like the former but the set-theoretic intersection is used instead of the

 set-theoretic union.
 
 set-theoretic union.
 

-In order for \TT{while} to work as expected, both {\av} sets are evaluaed in
+In order for \TT{while} to work as expected, both {\av} sets are evaluated in

 a common context during the iteration ({\ie} the variables defined in both
 a common context during the iteration ({\ie} the variables defined in both

-are alailable to both) and this context is also propagated outside the
-\TT{while} for convenience. 
+are available to both) and this context is also propagated outside the
+\TT{while}. 

 
 \item 
 
 \item 

-Bounded iteration.
-\newline
+\textbf{Bounded iteration.}

 Also this construction comes in two forms:
 
 \TT{for @}\EM{variable} \TT{in} \EM{av-set} \TT{sup} \EM{av-set}:
 Also this construction comes in two forms:
 
 \TT{for @}\EM{variable} \TT{in} \EM{av-set} \TT{sup} \EM{av-set}:

-\newline

 iterates the evaluation of the second \EM{av-set} assigning the \EM{variable} 
 to each element in the first \EM{av-set} and builds the {\MathQL}
 set-theoretic union of the obtained results.
 
 \TT{for @}\EM{variable} \TT{in} \EM{av-set} \TT{inf} \EM{av-set}:
 iterates the evaluation of the second \EM{av-set} assigning the \EM{variable} 
 to each element in the first \EM{av-set} and builds the {\MathQL}
 set-theoretic union of the obtained results.
 
 \TT{for @}\EM{variable} \TT{in} \EM{av-set} \TT{inf} \EM{av-set}:

-\newline
-like the former but set-theoretic intersection is used instead of
+like the former but the set-theoretic intersection is used instead of the

 set-theoretic union.
 
 The variables for attributed values (preceded by a \TT{@} sign and called 
 \emph{element variables}) may appear wherever an {\av} set is allowed and
 and in some additional places. 
 set-theoretic union.
 
 The variables for attributed values (preceded by a \TT{@} sign and called 
 \emph{element variables}) may appear wherever an {\av} set is allowed and
 and in some additional places. 

-\newline

 The element variables are kept distinct from the set variables (therefore
 \TT{\$variable} and \TT{@variable} may appear in the same query without
 The element variables are kept distinct from the set variables (therefore
 \TT{\$variable} and \TT{@variable} may appear in the same query without

-abiguity).
-
+ambiguity).

 Concerning the scope rules used in these constructions, the variables
 assigned by the first {\av} set are available to the second {\av} set during
 the iteration and the variables assigned by both {\av} sets are available 
 outside the \TT{for} as in the previous case. 
 
 \item
 Concerning the scope rules used in these constructions, the variables
 assigned by the first {\av} set are available to the second {\av} set during
 the iteration and the variables assigned by both {\av} sets are available 
 outside the \TT{for} as in the previous case. 
 
 \item

-Addition of groups.
-
+\textbf{Addition of groups.}

 \TT{add} \EM{optional-flag} \EM{attribute-groups} \TT{in} \EM{av-set}
 \TT{add} \EM{optional-flag} \EM{attribute-groups} \TT{in} \EM{av-set}

-\newline

 builds an {\av} set adding the specified \EM{attribute-groups} to each element
 of the given {\av} set.
 If no \EM{flag} is specified the addition is set-theoretic, whereas with the
 builds an {\av} set adding the specified \EM{attribute-groups} to each element
 of the given {\av} set.
 If no \EM{flag} is specified the addition is set-theoretic, whereas with the


@@ -115,22 +104,21 @@ considered.
 
 \figref{Add} shows how to build a one-element {\av} set using \TT{add}.
 
 
 \figref{Add} shows how to build a one-element {\av} set using \TT{add}.
 

-\begin{figure}[ht]
+\begin{figure}

 \begin{footnotesize} \begin{verbatim}
 The set of attributed values given explicitly:
 \begin{footnotesize} \begin{verbatim}
 The set of attributed values given explicitly:

-["head" attr {"attribute-name" = property /"metadata" of "resource"}]
+ ["head" attr {/"attribute" = property /"metadata" of "resource"}]

 
 

-The same set built with the add operator
-add {"attribute-name" = property /"metadata" of "resource"} in "head"
+The same set built with the add operator:
+ add {/"attribute" = property /"metadata" of "resource"} in "head"

 \end{verbatim} \end{footnotesize}
 \end{verbatim} \end{footnotesize}

-\vskip-1pc
+\vspace{-1pc}

 \caption{A simple use of the add operator}
 \label{Add}
 \end{figure}
 
 \item 
 \caption{A simple use of the add operator}
 \label{Add}
 \end{figure}
 
 \item 

-Existential test.
-
+\textbf{Existential test.}

 The existential test has the form \TT{ex} \EM{av-set} where the
 specification of the {\av} set contains some instances of the construction
 \TT{@}\EM{variable}\TT{.}\EM{attribute-name}, and runs as follows:
 The existential test has the form \TT{ex} \EM{av-set} where the
 specification of the {\av} set contains some instances of the construction
 \TT{@}\EM{variable}\TT{.}\EM{attribute-name}, and runs as follows:


@@ -138,15 +126,13 @@ the given {\av} set is evaluated replacing each
 \TT{@}\EM{variable}\TT{.}\EM{attribute-name}
 with the contents of \EM{attribute-name} in an attribute group of the {\av}
 stored in \TT{@}\EM{variable} and the evaluation is repeated for every
 \TT{@}\EM{variable}\TT{.}\EM{attribute-name}
 with the contents of \EM{attribute-name} in an attribute group of the {\av}
 stored in \TT{@}\EM{variable} and the evaluation is repeated for every

-possible choice of the groups (recall that different groups are allowed to
+possible choice of these groups (recall that different groups are allowed to

 contain attributes with the same name). If one evaluation gives a non empty
 contain attributes with the same name). If one evaluation gives a non empty

-result, the defaut representation of \emph{true} is returned (the test
-succeded) in the other case the empty {\av} set, {\ie} \emph{false}, is
-returned (the test failed).
+result, the default representation of \emph{true} is returned, in the other
+case the empty {\av} set, {\ie} \emph{false}, is returned.

 
 \item
 
 \item

-Function invocation:
-
+\textbf{Function invocation.}

 The core language allows to invoke two kinds of external functions (with
 which a language extension may be provided): the functions of the first kind 
 return an {\av} set, the functions of the second kind return a piece of 
 The core language allows to invoke two kinds of external functions (with
 which a language extension may be provided): the functions of the first kind 
 return an {\av} set, the functions of the second kind return a piece of 


@@ -156,23 +142,21 @@ code generator). In particular:
 \EM{function-name} \verb+{+ 
 \EM{name} \TT{,} $\cdots$ \TT{,} \EM{name} \verb+} {+
 \EM{av-set} \TT{,} $\cdots$ \TT{,} \EM{av-set} \verb+}+
 \EM{function-name} \verb+{+ 
 \EM{name} \TT{,} $\cdots$ \TT{,} \EM{name} \verb+} {+
 \EM{av-set} \TT{,} $\cdots$ \TT{,} \EM{av-set} \verb+}+

-\newline
-invokes the specified function of the firs kind on the given arguments and
-returns it result. The \EM{name} argument are {\MathQL} paths and usually
+invokes a function of the first kind on the given arguments and returns its
+result. The \EM{name} arguments are {\MathQL} paths and usually

 represent attribute names.
 
 \TT{gen} \EM{function-name} \verb+{+
 \EM{av-set} \TT{,} $\cdots$ \TT{,} \EM{av-set} \verb+}+
 represent attribute names.
 
 \TT{gen} \EM{function-name} \verb+{+
 \EM{av-set} \TT{,} $\cdots$ \TT{,} \EM{av-set} \verb+}+

-\newline
-invokes the specified function of the second kind on the given arguments and
-replaces the function invocation with its result.
+invokes a function of the second kind on the given arguments and replaces
+itself with the function result.

 
 

-The function names are {\MathQL} paths exactly as the attribute nanes and the 
+The function names are {\MathQL} paths exactly as the attribute names and the 

 graph paths used by the \TT{property} operator. The names of the two kinds of
 functions are kept in distinct environments so they do not clash.
 
 {\MathQL}.4 comes with a basic library of functions of the first kind 
 graph paths used by the \TT{property} operator. The names of the two kinds of
 functions are kept in distinct environments so they do not clash.
 
 {\MathQL}.4 comes with a basic library of functions of the first kind 

-(see \subsecref{IBasic}) that integrate the core language providing several
-facilities to the user.
+(see \subsecref{Basic}) that integrate the core language providing several
+facilities.

 
 \end{itemize}
 
 \end{itemize}

diff --git a/helm/mathql/doc/mathql_introduction_property.tex b/helm/mathql/doc/mathql_introduction_property.tex
index f73f5bc781c99d420e2e99fca3f04634f151f800..5fffd727642dd6316edee64254e3957a4d74c69b 100644 (file)
--- a/helm/mathql/doc/mathql_introduction_property.tex
+++ b/helm/mathql/doc/mathql_introduction_property.tex
@@ -1,71 +1,67 @@
 \subsection{High level access to metadata} \label{HighAccess}
 
 {\MathQL} high level access to an {\RDF} database is \emph{graph-oriented} and
 \subsection{High level access to metadata} \label{HighAccess}
 
 {\MathQL} high level access to an {\RDF} database is \emph{graph-oriented} and

-is delegated to its \TT{property} operator, that formally accesses an {\RDF}
-graph%
-\footnote
-{When we say {\RDF} graph, we actually mean both the {\RDFM} graph and the
-{\RDFS} graph.}
-through an \emph{access relation} which is better understood by explaining
-the informal semantics of the operator itself.  
-
-This operator builds a \emph{result} {\av} set starting from two mandatory
-arguments: the \emph{source} {\av} set and the \emph{head path}.
+is delegated to its \TT{property} operator that builds a \emph{result} {\av}
+set starting from two mandatory arguments: the \emph{source} {\av} set and the
+\emph{head path}.

 Other optional arguments may be used to change its default behaviour or to
 request advanced functionalities. 
 Other optional arguments may be used to change its default behaviour or to
 request advanced functionalities. 

-Its textual syntax is (see \subsecref{Textual}):
+
+This operator has the following syntax, where a path has the structure of an
+attribute name ({\ie} a list of strings) and denotes a (possibly empty) finite
+sequence of contiguous arcs (describing properties in the {\RDF} graph%
+\footnote
+{When we say \emph{{\RDF} graph}, we actually mean both the {\RDFM} graph and
+the {\RDFS} graph.}%
+).

 
 \begin{center}
 \TT{property} \EM{optional-flags} \EM{head-path} \EM{optional-clauses} \TT{of}
 \EM{optional-flag} \EM{av-set}
 \end{center}
 
 
 \begin{center}
 \TT{property} \EM{optional-flags} \EM{head-path} \EM{optional-clauses} \TT{of}
 \EM{optional-flag} \EM{av-set}
 \end{center}
 

-A path has the structure of an attribute name ({\ie} a list of strings) and
-denotes a (possibly empty) finite sequence of contiguous arcs (describing
-properties in the {\RDF} graph).
-
-\begin{figure}[ht]
+\begin{figure}

 \begin{footnotesize} \begin{verbatim}
 \begin{footnotesize} \begin{verbatim}

-These examples refer to the resources "A" and "B" of Figure 2.
+ These examples refer to the resources "A" and "B" of Figure 2.

 
 Example 1: reading an unstructured property - simple case:
 
 Example 1: reading an unstructured property - simple case:

-property "id"/"major" of {"A", "B"}   returns   "1"
-property "id"/"minor" of {"A", "B"}   returns   "2"; "7"
+ property /"id"/"major" of {"A", "B"} gives "1"
+ property /"id"/"minor" of {"A", "B"} gives "2"; "7"

 
 Example 2: reading an unstructured property - use of pattern:
 
 Example 2: reading an unstructured property - use of pattern:

-property "id"/"minor" of pattern ".*"   returns   "2"; "7"
+ property /"id"/"minor" of pattern ".*" gives "2"; "7"

 
 Example 3: reading a structured property without main component:
 
 Example 3: reading a structured property without main component:

-property "id" attr "major", "minor" of {"A", "B"}  
-generates the following attributed values:
-"" attr {"major" = "1"; "minor" = "2"}; "" attr {"major" = "1"; "minor" = "7"}
-that are composed using MathQL-1 set-theoretic union giving the one-element set:
-"" attr {"major" = "1"; "minor" = "2"}, {"major" = "1"; "minor" = "7"} 
+ property /"id" attr /"major", /"minor" of {"A", "B"}  
+ generates the following attributed values:
+ "" attr {/"major" = "1"; /"minor" = "2"}; 
+ "" attr {/"major" = "1"; /"minor" = "7"}
+ that are composed with the set-theoretic union giving:
+ "" attr {/"major" = "1"; /"minor" = "2"}, 
+         {/"major" = "1"; /"minor" = "7"} 

 
 Example 4: reading a structured property specifying a main component:
 
 Example 4: reading a structured property specifying a main component:

-property "id" main "major" attr "minor" of {"A", "B"}   gives
-"1" attr {"minor" = "2"}, {"minor" = "7"} 
+ property /"id" main /"major" attr /"minor" of {"A", "B"} gives
+ "1" attr {/"minor" = "2"}, {/"minor" = "7"} 

 
 Example 5: the renaming mechanism:
 
 Example 5: the renaming mechanism:

-property "id" attr "minor" as "new-name" of {"A", "B"}   gives  
-"" attr {"new-name" = "2"}, {"new-name" = "7"}
+ property /"id" attr /"minor" as /"new-name" of {"A", "B"} gives  
+ "" attr {/"new-name" = "2"}, {/"new-name" = "7"}

 
 Example 6: imposing constraints on property values:
 
 Example 6: imposing constraints on property values:

-property "date" istrue "first" in "2002-01-01" attr "modified" of {"A", "B"}   and  
-property "date" istrue "first" match ".*01.*" attr "modified" of {"A", "B"}    give
-"" attr {"modified" = "2002-03-01"}
-Only the instance of "date" with "first" set to "2002-01-01" is considered.
+ property /"date" istrue /"first" in "2002-01-01" 
+                  attr /"modified" of {"A", "B"} and  
+ property /"date" istrue /"first" match ".*01.*" 
+                  attr /"modified" of {"A", "B"} give
+ "" attr {/"modified" = "2002-03-01"}
+ Only the instance of "date" with "first" set to "2002-01-01" 
+  is considered.

 
 Example 7: inverse traversal of the head path:
 
 Example 7: inverse traversal of the head path:

-property inverse "date" attr "first" in subj ""   gives
-"A" attr {"first" = "2002-01-01"}; "B" attr {"first" = "2002-02-01"}
-
-Example 8: some triples of an access relation:
-The triples formalizing the property "date" of the resource "A":
-("A", "date", "");
-("A", "date"/"first", "2002-01-01"); ("A", "date"/"modified", "2002-03-01")
+property inverse /"date" attr /"first" in "" gives
+"A" attr {/"first" = "2002-01-01"}; "B" attr {/"first" = "2002-02-01"}

 \end{verbatim} \end{footnotesize}
 \end{verbatim} \end{footnotesize}

-\vskip-1pc
+\vspace{-1pc}

 \caption{The ``property'' operator}
 \label{Property}
 \end{figure}
 \caption{The ``property'' operator}
 \label{Property}
 \end{figure}


@@ -81,10 +77,9 @@ the query engine, using the resources specified in the head strings of the
 source {\av} set (call them source resources) as start-nodes.
 
 \item
 source {\av} set (call them source resources) as start-nodes.
 
 \item

-The computation gives a set of nodes in the {\RDF} graph ({\ie} the end-nodes
-of the instantiated paths) which are the values of the instances of the
-(possibly compound) property specified by the path and concerning the source
-resources.
+The computation gives a set of nodes ({\ie} the end-nodes of the instantiated
+paths) which are the values of the instances of the (possibly compound)
+property specified by the path and concerning the source resources.

 
 \item
 These values, encoded into {\av}'s as explained above, are composed by means
 
 \item
 These values, encoded into {\av}'s as explained above, are composed by means


@@ -109,6 +104,7 @@ value's main component in the \TT{main} \EM{optional-clause} (this
 specification overrides the default setting inferred from the {\RDF} graph
 through the \emph{rdf:value} property) and the list of the value's secondary
 components in the \TT{attr} \EM{optional-clause}. 
 specification overrides the default setting inferred from the {\RDF} graph
 through the \emph{rdf:value} property) and the list of the value's secondary
 components in the \TT{attr} \EM{optional-clause}. 

+

 Note that if a secondary component is not listed in the \TT{attr} clause, it
 will not be read.
 Also recall that, when the result {\av}'s are formed, the main component is
 Note that if a secondary component is not listed in the \TT{attr} clause, it
 will not be read.
 Also recall that, when the result {\av}'s are formed, the main component is


@@ -123,8 +119,9 @@ path.
 Note that the name of an attribute, which by default is its defining path in
 the \TT{attr} clause, can be changed with an optional \TT{as} clause for the
 user's convenience. See for instance \figref{Property} (example 5).
 Note that the name of an attribute, which by default is its defining path in
 the \TT{attr} clause, can be changed with an optional \TT{as} clause for the
 user's convenience. See for instance \figref{Property} (example 5).

-The alternative could be a simple string but it needs to be a path for typing
-reasons. In any case a string can be seen as a one-element path.
+Note that the assigned name must be a path for typing reasons.
+The alternative could be to use a simple string but in any case a string can
+be seen as a one-element path.

 
 In the default case \TT{property} builds its result considering every
 component of the {\RDFM} graph ({\ie} every {\RDFM}) but we can constrain
 
 In the default case \TT{property} builds its result considering every
 component of the {\RDFM} graph ({\ie} every {\RDFM}) but we can constrain


@@ -140,7 +137,7 @@ its specification (appearing in the \TT{istrue} or \TT{isfalse} clause) is
 a path in the {\RDF} graph starting from the end-node of the head path.
 
 \TT{property} allows to access the {\RDFS} property hierarchy by specifying
 a path in the {\RDF} graph starting from the end-node of the head path.
 
 \TT{property} allows to access the {\RDFS} property hierarchy by specifying

-a flag named \TT{sub} or \TT{super}.
+a flag \TT{sub} or \TT{super}.

 If the \TT{sub} flag is present, \TT{property} inspects the instances of the
 default tree (made by the head path and by the \EM{optional-clauses} paths)
 and every other tree obtained by substituting an arc $ p $ with the arc of a
 If the \TT{sub} flag is present, \TT{property} inspects the instances of the
 default tree (made by the head path and by the \EM{optional-clauses} paths)
 and every other tree obtained by substituting an arc $ p $ with the arc of a


@@ -160,44 +157,9 @@ component is specified in head strings of the source {\av} set.
 \item
 It encodes the resources corresponding to the instances of the start-nodes into
 {\av}'s assigning the attributes obtained instantiating the attribute paths%
 \item
 It encodes the resources corresponding to the instances of the start-nodes into
 {\av}'s assigning the attributes obtained instantiating the attribute paths%

-\footnote{The path in \EM{optional-clauses} are never traversed backward.}
-and composes these {\av}'s using the {\MathQL} set-theoretic union to build
-the result set.
+\footnote{The paths in the \EM{optional-clauses} are never traversed backward.}
+and builds the result set composing these {\av}'s with the set-theoretic union.

 
 \end{enumerate}
 
 See for instance \figref{Property} (example 7).
 
 \end{enumerate}
 
 See for instance \figref{Property} (example 7).

-
-Now we can present \emph{access relations} which are the formal tools used by
-{\MathQL} semantics to access the {\RDF} graph.
-An access relation is a set of triples $ (r_1, p, r_2) $ where $ r_1 $ and
-$ r_2 $ are strings, $ p $ is a path (encoded as a list of strings). 
-Each triple is a sort of ``extended {\RDF} triple'' in the sense that $ r_1 $
-is is a resource for which metadata is provided, $ p $ is a path in the {\RDF}
-graph and $ r_2 $ is the main value of the end-node of the instance of $ p $
-starting from $ r_1 $ (this includes the instances of sub- and super-arcs of
-$ p $ if necessary).
-See for instance \figref{Property} (example 8).
-
-{\MathQL} does not provide for any built-in access relation so any query
-engine can freely define the access relations that are appropriate with
-respect to the metadata it can access.
-In particular, \secref{Interpreter} describes the access relations implemented
-by the {\HELM} query engine.
-
-It is worth remarking, as it was already stressed in \cite{GS03, Gui03}, that
-the concept of access relation corresponds to the abstract concept of
-property in the basic {\RDF} data model which draws on well established
-principles from various data representation communities.
-In this sense an {\RDF} property can be thought of either as an attribute of a
-resource (traditional attribute-value pairs model), or as a relation between
-a resource and a value (entity-relationship model).
-This observation leads us to conclude that {\MathQL} is sound and complete
-with respect to querying an abstract {\RDF} metadata model. 
-
-Finally note that access relations are close to {\RDF} entity-relationship
-model, but they do not work if we allow paths with an arbitrary number of
-loops ({\ie} with an arbitrary length) because this would lead to creating
-infinite sets of triples.
-If we want to handle this case, we need to turn these relations into
-multivalued functions.

diff --git a/helm/mathql/doc/mathql_introduction_textual.tex b/helm/mathql/doc/mathql_introduction_textual.tex
index 2899a24ce4054e5bbef19c1013e3b567690d8082..8e5878bac08f3faefef2f051619a369fa69dcb20 100644 (file)
--- a/helm/mathql/doc/mathql_introduction_textual.tex
+++ b/helm/mathql/doc/mathql_introduction_textual.tex
@@ -1,6 +1,8 @@
-\subsection{Textual syntax} \label{Textual}
+\section{Textual syntax} \label{Textual}

 
 

-The syntax of grammatical productions resembles BNF and POSIX notation:
+In this section we present {\MathQL}.4 textual syntax using the same notation
+that we adopted in \cite{GS03,Gui03}. In particular the grammatical
+productions we use resemble {\BNF} with some {\POSIX} formalism:

 
 \begin{itemize}
 
 
 \begin{itemize}
 


@@ -8,17 +10,13 @@ The syntax of grammatical productions resembles BNF and POSIX notation:
 \TT{::=} defines a grammatical production by means of a regular expression.
 
 Regular expressions are made of the following elements
 \TT{::=} defines a grammatical production by means of a regular expression.
 
 Regular expressions are made of the following elements

-(here \TT{...} is a placeholder):
-
-% \item
-% \TT{.} represents any character between U 0020 and U 007F inclusive;
+(\TT{...} is a placeholder):

 
 \item 
 \TT{`...`} represents any character in a character set;
 
 \item 
 
 \item 
 \TT{`...`} represents any character in a character set;
 
 \item 

-\verb+`^ ...`+ represents any character (U+0020 to U+007E) not in a character
-set;
+\verb+`^ ...`+ represents any character (U+20 to U+7E) not in a character set;

 
 \item 
 \TT{"..."} represents a string to be matched verbatim;
 
 \item 
 \TT{"..."} represents a string to be matched verbatim;


@@ -46,13 +44,7 @@ set;
 
 \end{itemize}
 
 
 \end{itemize}
 

-\noindent
-{\MathQL} Expressions can contain quoted constant strings with the syntax of
-\figref {StrTS}.%
-\footnote{Note that the first slash of the \GP{path} is not optional as
-in {\MathQL}.3.}
-
-\begin{figure}[ht]
+\begin{figure}

 \begin{footnotesize} \begin{verbatim}
 <dec>     ::= '0 - 9'
 <num>     ::= <dec> [ <dec> ]*
 \begin{footnotesize} \begin{verbatim}
 <dec>     ::= '0 - 9'
 <num>     ::= <dec> [ <dec> ]*


@@ -65,11 +57,7 @@ in {\MathQL}.3.}
 \caption{Textual syntax of numbers, strings and paths} \label{StrTS}
 \end{figure}
 
 \caption{Textual syntax of numbers, strings and paths} \label{StrTS}
 \end{figure}
 

-\noindent
-The meaning of the escaped sequences is shown in \figref{EscTS}
-(where $ .... $ is a 4-digit placeholder).
-
-\begin{figure}[ht]
+\begin{figure}

 \begin{footnotesize}
 \begin{center} \begin{tabular}{|l|l|c|}
 \hline {\bf Escape sequence} & {\bf Unicode character} & {\bf Text} \\
 \begin{footnotesize}
 \begin{center} \begin{tabular}{|l|l|c|}
 \hline {\bf Escape sequence} & {\bf Unicode character} & {\bf Text} \\


@@ -84,38 +72,43 @@ The meaning of the escaped sequences is shown in \figref{EscTS}
 \caption{Textual syntax of escaped characters} \label{EscTS}
 \end{figure}
 
 \caption{Textual syntax of escaped characters} \label{EscTS}
 \end{figure}
 

+Queries and results can contain quoted constant strings with the syntax of
+\figref {StrTS}%
+\footnote
+{Note that the first slash of the \GP{path} is not optional as in {\MathQL}.3.}
+and the meaning of the escaped sequences is shown in \figref{EscTS} (where 
+$ .... $ is a 4-digit placeholder).

 {\MathQL} character escaping syntax aims at complying with W3C character model
 for the World Wide Web \cite{W3Ca} which recommends a support for standard
 Unicode characters (U+0000 to U+FFFF) and escape sequences with start/end
 delimiters.
 In particular {\MathQL} escape delimiters (backslash and caret) are chosen
 {\MathQL} character escaping syntax aims at complying with W3C character model
 for the World Wide Web \cite{W3Ca} which recommends a support for standard
 Unicode characters (U+0000 to U+FFFF) and escape sequences with start/end
 delimiters.
 In particular {\MathQL} escape delimiters (backslash and caret) are chosen

-among the {\em unwise} characters for URI references (see \cite{URI}) because
-URI references are the natural content of constant strings and these
-characters should not be so frequent in them.
-
-Query expressions can contain variables for {\av}'s (production \GP{avar})
-and variables for {\av} sets, {\ie} for query results (production \GP{svar})
-according to the syntax of \figref{VarTS}.%
-\footnote{This syntax resembles the one of programming languages identifiers.}
+among the \emph{unwise} characters for {\URI} references (see \cite{URI}) 
+because {\URI} references are the natural content of constant strings and 
+these characters should not be so frequent in them.

 
 

-\begin{figure}[ht]
+\begin{figure}

 \begin{footnotesize} \begin{verbatim}
 <alpha> ::= [ 'A - Z' | 'a - z' | `_` ]+
 <id>    ::= <alpha> [ <alpha> | <dec> ]*
 \begin{footnotesize} \begin{verbatim}
 <alpha> ::= [ 'A - Z' | 'a - z' | `_` ]+
 <id>    ::= <alpha> [ <alpha> | <dec> ]*

-<avar>  ::= "@" <id>

 <svar>  ::= "$" <id>
 <svar>  ::= "$" <id>

+<evar>  ::= "@" <id>

 \end{verbatim}\end{footnotesize} %$
 \vskip-1pc
 \caption{Textual syntax of variables} \label{VarTS}
 \end{figure}
 
 \end{verbatim}\end{footnotesize} %$
 \vskip-1pc
 \caption{Textual syntax of variables} \label{VarTS}
 \end{figure}
 

-\noindent
-The syntax of query expressions (production \GP{query}) is described in
-\figref{QueryTS}.
+Queries can also contain \emph{set} variables (production \GP{svar}) and
+\emph{element} variables (production \GP{evar}) according to the syntax of
+\figref{VarTS}.%
+\footnote{This syntax resembles the one of programming languages identifiers.}
+A set variable holds an {\av} set, {\ie} a query result, while an element
+variable holds an {\av}.

 
 

-\begin{figure}[ht]
+\begin{figure}

 \begin{footnotesize} \begin{verbatim}
 \begin{footnotesize} \begin{verbatim}

-<qualifier> ::= [ "inverse" ]? [ "sub" | "super" ]? <path>
+<ref>       ::= [ "sub" | "super" ]?
+<qualifier> ::= [ "inverse" ]? <ref> <path>

 <main>      ::= [ "main" <path> ]? 
 <cons>      ::= <path> [ "in" | "match" ] <query>
 <istrue>    ::= [ "istrue" <cons> [ "," <cons> ]* ]?
 <main>      ::= [ "main" <path> ]? 
 <cons>      ::= <path> [ "in" | "match" ] <query>
 <istrue>    ::= [ "istrue" <cons> [ "," <cons> ]* ]?


@@ -124,16 +117,16 @@ The syntax of query expressions (production \GP{query}) is described in
 <sec>       ::= [ "attr" <exp> [ "," <exp> ]* ]?
 <opt_args>  ::= <main> <istrue> <isfalses> <sec>
 <source>    ::= [ "pattern" ]? <query>
 <sec>       ::= [ "attr" <exp> [ "," <exp> ]* ]?
 <opt_args>  ::= <main> <istrue> <isfalses> <sec>
 <source>    ::= [ "pattern" ]? <query>

-<paths>     ::= [ <path> [ "," <path> ]* ]?
+<paths>     ::= <path> [ "," <path> ]*

 <query>     ::= "(" <query> ")" | <string> | "[" <xavs> "]"
             |   "property" <qualifier> <opt_args> "of" <source>
             |   "let" <svar> "=" <query> "in" <query>
 <query>     ::= "(" <query> ")" | <string> | "[" <xavs> "]"
             |   "property" <qualifier> <opt_args> "of" <source>
             |   "let" <svar> "=" <query> "in" <query>

-            |   <query> ";;" <query> | <svar> | <avar> 
-            |   "ex" <query> | <avar> "." <path>
-            |   "add" [ "distr" ]? [ <xgroups> | <avar> ] "in" <query>
-            |   "for" <avar> "in" <query> [ "sup" | "inf" ] <query>
+            |   <query> ";;" <query> | <svar> | <evar> 
+            |   "ex" <query> | <evar> "." <path>
+            |   "add" [ "distr" ]? [ <xgroups> | <evar> ] "in" <query>
+            |   "for" <evar> "in" <query> [ "sup" | "inf" ] <query>

             |   "while" <query> [ "sup" | "inf" ] <query>
             |   "while" <query> [ "sup" | "inf" ] <query>

-            |   <path> "{" <paths> "}" "{" <queries> "}"
+            |   <path> "{" [ <paths> ]? "}" "{" <queries> "}"

             |   "gen" <path> [ "{" <queries> "}" | "in" <query> ] 
 <queries>   ::= [ <query> [ "," <query> ]* ]?
 <xattr>     ::= <path> "=" <query>
             |   "gen" <path> [ "{" <queries> "}" | "in" <query> ] 
 <queries>   ::= [ <query> [ "," <query> ]* ]?
 <xattr>     ::= <path> "=" <query>


@@ -146,11 +139,7 @@ The syntax of query expressions (production \GP{query}) is described in
 \caption{Textual syntax of queries} \label{QueryTS}
 \end{figure}
 
 \caption{Textual syntax of queries} \label{QueryTS}
 \end{figure}
 

-\noindent
-The syntax of result expressions (production \GP{avs}) is described in
-\figref{ResultTS}.
-
-\begin{figure}[ht]
+\begin{figure}

 \begin{footnotesize} \begin{verbatim}
 <attr>  ::= <path> "=" <string> | "{" <string> [ "," <string> ]* "}" 
 <group> ::= "{" <attr> [ ";" <attr> ]* "}"
 \begin{footnotesize} \begin{verbatim}
 <attr>  ::= <path> "=" <string> | "{" <string> [ "," <string> ]* "}" 
 <group> ::= "{" <attr> [ ";" <attr> ]* "}"


@@ -161,19 +150,29 @@ The syntax of result expressions (production \GP{avs}) is described in
 \caption{Textual syntax of results} \label{ResultTS}
 \end{figure}
 
 \caption{Textual syntax of results} \label{ResultTS}
 \end{figure}
 

-The textual syntax of the language extension provided by the basic library
-is in \figref{BasicTS}.
-
-\begin{figure}[ht]
+\begin{figure}

 \begin{footnotesize} \begin{verbatim}
 <query> ::= "empty" | "false" | "true"
 \begin{footnotesize} \begin{verbatim}
 <query> ::= "empty" | "false" | "true"

-        |   "not" <query>
-        |   <query> [ "and" | "or" | "xor"| "sub" | "meet" | "eq" | "le"| "lt" ] <query>
-        |   <query> [ "union" | "intersect" ] <query> | { <queries> }  
+        |   [ "not" | "count" | "proj" <path> "of" ] <query>
+        |   <query> [ "and" | "or" | "xor" ] <query>
+        |   <query> [ "sub" | "meet" | "eq" | "le" | "lt" ] <query> 
+        |   <query> [ "union" | "intersect" | "diff" ] <query> 
+        |   "{" <queries> "}"  
+        |   "keep" [ "allbut" ]? [ <paths> "in" ]? <query> 

         |   "if" <query> "then" <query> "else" <query>
         |   "if" <query> "then" <query> "else" <query>

-        |   "select" <avar> "from" <query> "where" <query>
+        |   "select" <evar> "from" <query> "where" <query>

 \end{verbatim} \end{footnotesize}
 \vskip-1pc
 \end{verbatim} \end{footnotesize}
 \vskip-1pc

-\caption{Textual syntax of basic extension} \label{BasicTS}
+\caption{Textual syntax of the basic extension} \label{BasicTS}

 \end{figure}
 
 \end{figure}
 

+The core infrastructure of {\MathQL}.4 defines a syntax for queries 
+(\figref{QueryTS}, production \GP{query}) and a syntax for results 
+(\figref{ResultTS}, production \GP{avs}).
+A syntax extension for the most common functions of the basic library is
+also provided for the user's convenience and for backward compatibility with 
+{\MathQL}.3. The syntax extension concerning the functions covered in this
+paper is shown in \figref{BasicTS}.
+Note that this extension makes \GP{avs} an instance of \GP{xavs}.
+
+

diff --git a/helm/mathql/doc/mathql_macros.sty b/helm/mathql/doc/mathql_macros.sty
index 01b563f8d00de16d5a245b0a22fbee7a9cf0ffc5..de81655d4be40bec1eb133a188ab025466283000 100644 (file)
--- a/helm/mathql/doc/mathql_macros.sty
+++ b/helm/mathql/doc/mathql_macros.sty
@@ -1,9 +1,39 @@
-\usepackage{fguidi-defs} 
+\usepackage{amssymb}

 
 

-\newcommand{\secref}[1]{Section~\ref{#1}}
-\newcommand{\subsecref}[1]{Subsection~\ref{#1}}
-\newcommand{\figref}[1]{Figure~\ref{#1}}
+\newcommand\CURI[1]{\texttt{<#1>}}
+\newcommand\EM[1]{\noindent\hbox{\frenchspacing\em #1}}
+\newcommand\TT[1]{\noindent\hbox{\frenchspacing\tt #1}}
+\newcommand\RM[1]{\noindent\hbox{\frenchspacing\rm #1}}
+\newcommand\secref[1]{Section~\ref{#1}}
+\newcommand\subsecref[1]{Subsection~\ref{#1}}
+\newcommand\figref[1]{Figure~\ref{#1}}
+\newcommand\ie{{\frenchspacing i.e.}}
+\newcommand\oft{\mathrel :}
+\newcommand\lex{\exists}
+\newcommand\lall{\forall}
+\newcommand\sub{\subseteq}
+\newcommand\meet{\between}
+\newcommand\sand{\cap}
+\newcommand\sdor{\sqcup}
+\newcommand\sor{\cup}
+\newcommand\bigsor{\bigcup}
+\newcommand\app{\mathbin @}
+\newcommand\fa{\phi}
+\newcommand\fb{\psi}
+\newcommand\st{\mathrel |}
+\newcommand\p{{^\prime}}
+\newcommand\jolly{\mathbin\square}
+\newcommand\gdlap[2]{\vbox to 0pt {\vskip#2\hbox{#1}\vss}}
+\newcommand\setnames@[2]{&\gdlap{\kern2pt$#1$}{#2}} 
+\newcommand\imain[1]{{\offinterlineskip\lineskip=2pt\noindent
+  $\vcenter{\halign{\hss$##$\hss&##\hss\cr#1\crcr}}$}}
+\newcommand\iname[1]{\cr\hrulefill\setnames@{#1}{-1.0ex}\cr}
+\newcommand\irule[3]{\imain{#1 \iname{#2} #3}}
+\newcommand\spc{\hspace{1em}}
+\newcommand\icr{\cr}
+\newcommand\Nop{\noindent\hbox to 0pt{\vbox to 1ex{\vfil}\hfil}}

 
 

+\newcommand\BNF{\textsc{bnf}}

 \newcommand\CAML{\textsc{caml}}
 \newcommand\Galax{\textsc{galax}}
 \newcommand\HELM{\textsc{helm}}
 \newcommand\CAML{\textsc{caml}}
 \newcommand\Galax{\textsc{galax}}
 \newcommand\HELM{\textsc{helm}}


@@ -19,45 +49,49 @@
 \newcommand\XML{\textsc{xml}}
 \newcommand\XQuery{\textsc{xquery}}
 
 \newcommand\XML{\textsc{xml}}
 \newcommand\XQuery{\textsc{xquery}}
 

-\def\av{{\frenchspacing a.v.}}
+\newcommand\av{{\frenchspacing a.v.}}

 
 

-\def\D{\Delta}
-\def\G{\Gamma}
-\def\ES{\emptyset}
-\def\bigsum{\bigoplus}
-\def\daq{\mathrel{\Downarrow_q}}
-\def\dar{\mathrel{\Downarrow_r}}
-\def\distr{\mathbin\odot}
-\def\dprod{\mathbin\boxtimes} 
-\def\dsum{\mathbin\boxplus} 
-\def\g{(\G_s, \G_a, \G_g)}
-\def\get#1#2{#1(#2)}
-\def\prod{\mathbin\otimes} 
-\def\set#1#2#3{#1[#2 \gets #3]}
-\def\sum{\mathbin\oplus}
+\newcommand\D{\Delta}
+\newcommand\G{\Gamma}
+\newcommand\ES{\emptyset}
+\newcommand\bigsum{\bigoplus}
+\newcommand\daq{\mathrel{\Downarrow_q}}
+\newcommand\dar{\mathrel{\Downarrow_r}}
+\newcommand\distr{\mathbin\odot}
+\newcommand\dprod{\mathbin\boxtimes} 
+\newcommand\dsum{\mathbin\boxplus} 
+\newcommand\g{(\G_s, \G_e, \G_g)}
+\newcommand\get[2]{#1(#2)}
+\newcommand\sdiff{\mathbin\ominus} 
+\newcommand\set[3]{#1[#2 \gets #3]}
+\newcommand\sprod{\mathbin\otimes} 
+\newcommand\ssum{\mathbin\oplus}

 
 

-\def\Boole{\TT{Boole}}
-\def\Listof{\TT{ListOf}}
-\def\Setof{\TT{SetOf}}
-\def\Str{\TT{String}}
-\def\Num{\TT{Num}}
+\newcommand\Boole{\TT{Boole}}
+\newcommand\Listof{\TT{ListOf}}
+\newcommand\Setof{\TT{SetOf}}
+\newcommand\Str{\TT{Str}}
+\newcommand\Num{\TT{Num}}

 
 

-\def\All{\TT{All}}
-\def\Exp{\TT{Exp}}
-\def\F{\TT{F}}
-\def\For{\TT{For}}
-\def\Fst{\TT{Fst}}
-\def\Fsts{\TT{Fsts}}
-\def\Fun{\TT{Fun}}
-\def\Gen{\TT{Gen}}
-\def\Istrue{\TT{IsTrue}}
-\def\Match{\TT{Match}}
-\def\Name{\TT{Name}}
-\def\Pattern{\TT{Pattern}}
-\def\Property{\TT{Property}}
-\def\Snd{\TT{Snd}}
-\def\Src{\TT{Src}}
-\def\Unquote{\TT{Unq}}
-\def\T{\TT{T}}
+\newcommand\All{\TT{All}}
+\newcommand\Exp{\TT{Exp}}
+\newcommand\F{\TT{F}}
+\newcommand\For{\TT{For}}
+\newcommand\Fst{\TT{Fst}}
+\newcommand\Fsts{\TT{Fsts}}
+\newcommand\Fun{\TT{Fun}}
+\newcommand\Gen{\TT{Gen}}
+\newcommand\Head{\TT{Head}}
+\newcommand\Istrue{\TT{IsT}}
+\newcommand\Keep{\TT{Keep}}
+\newcommand\Match{\TT{Match}}
+\newcommand\Name{\TT{Name}}
+\newcommand\Pattern{\TT{Pattern}}
+\newcommand\Proj{\TT{Proj}}
+\newcommand\Property{\TT{Property}}
+\newcommand\Snd{\TT{Snd}}
+\newcommand\Src{\TT{Src}}
+\newcommand\Unquote{\TT{Unq}}
+\newcommand\T{\TT{T}}

 
 

-\def\GP#1{\TT{<#1>}}
+\newcommand\GP[1]{\TT{<#1>}}

diff --git a/helm/mathql/doc/mathql_operational.tex b/helm/mathql/doc/mathql_operational.tex
index 7868d3545744b105b808924dcb239bc9625d58d8..32be697a50486a2ac4b99142a91c26613e9ccba4 100644 (file)
--- a/helm/mathql/doc/mathql_operational.tex
+++ b/helm/mathql/doc/mathql_operational.tex
@@ -5,10 +5,10 @@ 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.
 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.

 
 \input{mathql_operational_background}
 \input{mathql_operational_core}
 
 \input{mathql_operational_background}
 \input{mathql_operational_core}

-\input{mathql_operational_library}
+\input{mathql_operational_basic}

 
 

diff --git a/helm/mathql/doc/mathql_operational_background.tex b/helm/mathql/doc/mathql_operational_background.tex
index 0c831f812eda5afc4dd427179a5626d49f9a4ea7..ad0be5122dec7577e77532d6bc0228dce579b75e 100644 (file)
--- a/helm/mathql/doc/mathql_operational_background.tex
+++ b/helm/mathql/doc/mathql_operational_background.tex
@@ -1,33 +1,33 @@
 \subsection {Mathematical background}
 
 \subsection {Mathematical background}
 

-As a mathematical background for the semantics, we take the one presented in
-\cite{Gui03}.
+As background for the semantics, we revise the one presented in
+\cite{Gui03,GS03}.

 
 {\Str} denotes the type of strings and its elements are the finite sequences
 of Unicode \cite{Unicode} characters.
 
 {\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.
+Grammatical productions 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.
+{\Num} denotes the type of numbers and is the subtype of {\Str} defined by 
+\GP{num}. In this type, numbers are represented by their decimal expansion.

 
 $ \Setof\ Y $ denotes the type of finite sets ({\ie} unordered finite
 
 $ \Setof\ Y $ denotes the type of finite sets ({\ie} unordered finite

-sequences without repetitions) over $ Y $.
+sequences without repetitions) over $ Y $ and

 $ \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 
 $ \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 $.
+are $ y_1, \cdots, y_m $ ($ \{y_1, \cdots, y_m\} $ will denote a set as
+usual).

 
 

-{\Boole}, the type of Boolean values, is defined as
-$ \{\ES, \{("", \ES)\}\} \oft \Setof\ \Setof\ (\Str \times \Setof\ Y) $ 
+{\Boole}, the type of Boolean values, is defined as the set
+$ \{\ES, \{("", \ES)\}\} $ of type $ \Setof\ \Setof\ (\Str \times \Setof\ Y) $ 

 where the first element stands for \emph{false} (denoted by {\F}) and the
 where the first element stands for \emph{false} (denoted by {\F}) and the

-second element stands for \emph{true} (denoted by {\T}).
+second element stands for \emph{true} (denoted by {\T}).%
+\footnote{This definition allows to treat a Boolean value as an {\av} set.}

 
 $ 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 \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}.
 $ 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}.


@@ -55,7 +55,7 @@ $ {\sub} \oft (\Setof\ Y) \to (\Setof\ Y) \to \Boole $ (infix)
 \item
 $ {\meet} \oft (\Setof\ Y) \to (\Setof\ Y) \to \Boole $ (infix)
 
 \item
 $ {\meet} \oft (\Setof\ Y) \to (\Setof\ Y) \to \Boole $ (infix)
 

-%\item
+\item

 $ {\sand} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $ (infix)
 
 \item
 $ {\sand} \oft (\Setof\ Y) \to (\Setof\ Y) \to (\Setof\ Y) $ (infix)
 
 \item


@@ -92,17 +92,15 @@ $ 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%
 $ 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) $.}.
-
+\footnote{As for the Boolean condition $ \fa \lor \fb $ which may have a more
+efficient implementation than $ \lnot(\lnot \fa \land \lnot \fb) $.}.

 $ 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}.
 
 $ 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:
+Sets of couples play a central role in our presentation and we will use:

 
 \begin{itemize}
 
 
 \begin{itemize}
 


@@ -125,7 +123,7 @@ 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) $.
 \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 \\
+The type of this operator is

 $ (\Setof\ (Y \times Z)) \to Y \to Z \to (\Setof\ (Y \times Z)) $.  
 
 \item 
 $ (\Setof\ (Y \times Z)) \to Y \to Z \to (\Setof\ (Y \times Z)) $.  
 
 \item 

diff --git a/helm/mathql/doc/mathql_operational_basic.tex b/helm/mathql/doc/mathql_operational_basic.tex
new file mode 100644 (file)
index 0000000..cc309f7
--- /dev/null
+++ b/helm/mathql/doc/mathql_operational_basic.tex
@@ -0,0 +1,298 @@
+\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{<path>} \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{<path>} \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{<path>} \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}

diff --git a/helm/mathql/doc/mathql_operational_core.tex b/helm/mathql/doc/mathql_operational_core.tex
index f9471292bda99135d6cc49aa638063bea94c68c8..ed03917528c3890363feafa39197255bb6d7de2d 100644 (file)
--- a/helm/mathql/doc/mathql_operational_core.tex
+++ b/helm/mathql/doc/mathql_operational_core.tex
@@ -1,32 +1,32 @@
-\subsection {The core language}
+\subsection {The core language} \label{OCore}

 
 \subsubsection*{Preliminaries}
 
 
 \subsubsection*{Preliminaries}
 

-Wih the above background we are able to type the main objects needed in the
+With the above background we are able to type the main objects needed in the

 formalization:
 
 \begin{itemize}
 
 \item
 formalization:
 
 \begin{itemize}
 
 \item

-A path $ s $ is a list of strings therefore its type is
+A path $ p $ is a list of strings therefore its type is

 $ T_{0a} = \Listof\ \Str $.
 
 \item
 $ T_{0a} = \Listof\ \Str $.
 
 \item

-A multiple string value $ V $ is an object of type $ T_{0b} = \Setof\ \Str $.
+The attribute contents $ V $ are an object of type $ T_{0b} = \Setof\ \Str $.

 
 \item
 
 \item

-A attribute group $ G $ is an association set connecting the attribute names
-to their values, therefore its type is
+An attribute group $ G $ is an association set connecting the attribute names
+to their contents, therefore its type is

 $ T_1 = \Setof\ (T_{0a} \times T_{0b}) $. 
 
 \item
 $ T_1 = \Setof\ (T_{0a} \times T_{0b}) $. 
 
 \item

-A subject string $ r $ is an object of type $ \Str $.
+A head 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
 
 \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
+An {\av}, {\ie} a head string with its attribute groups, has type

 $ T_3 = \Str \times T_2 $. 
 
 \item
 $ T_3 = \Str \times T_2 $. 
 
 \item


@@ -40,8 +40,7 @@ $ T_5 = \Str \times \Str \times (T_{0a} \to \Str) $.
 
 When a constant string appearing in a {\MathQL} expression is unquoted, the
 surrounding double quotes are deleted and each escaped sequence is translated
 
 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}.
-
+according to \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
 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


@@ -53,14 +52,15 @@ 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
 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.
+set variables to {\av} sets, element variables to {\av}'s and element
+variables to attribute groups.

 Therefore the type $ K $ of the context $ \G $ is:
 
 \begin{footnotesize} \begin{center}
 $ 
 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)
+\Setof\ (\GP{svar} \times T_4) \times
+\Setof\ (\GP{evar} \times T_3) \times % $ \\ $ \times\
+\Setof\ (\GP{evar} \times T_1)

 $
 \end{center} \end{footnotesize}
 
 $
 \end{center} \end{footnotesize}
 


@@ -73,7 +73,7 @@ $ \mathord{\daq} \oft (K \times \GP{query}) \times (K \times T_4) \to \Boole $.
 \end{tabular} \end{center}
 \end{footnotesize}
 
 \end{tabular} \end{center}
 \end{footnotesize}
 

-The context components $ \G_s $ and $ \G_a $ are used to store the contents of
+The context components $ \G_s $ and $ \G_e $ are used to store the contents of

 variables, while $ \G_g $ is used by the \TT{ex} operator to be presented
 below.
 
 variables, while $ \G_g $ is used by the \TT{ex} operator to be presented
 below.
 


@@ -86,15 +86,15 @@ to an {\av} set.
 
 \subsubsection*{Queries}
 
 
 \subsubsection*{Queries}
 

-The first \GP{query} expressions include explicit {\av} sets and syntactic
-grouping:
+The first group of \GP{query} expressions include the representation of
+explicit {\av} sets and the syntactic grouping facility:

 
 \begin{itemize}
 
 \item 
 The syntactic grouping is obtained enclosing a \GP{query} between \TT{(}
 and \TT{)}.    
 
 \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
+An explicit {\av} set can be represented either 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
 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


@@ -110,21 +110,21 @@ evaluated using the rules given below.
 \begin{center} 
 %
 \irule{x_1, \cdots, x_m \in \GP{xav} \spc 
 \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}
+       (\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 \ssum \cdots \ssum S_m}

 %
 \end{center} 
 \begin{center} 
 %
 %
 \end{center} 
 \begin{center} 
 %

-\irule{q \in \GP{string} \spc g_1, \cdots, g_m \in \GP{xgroup} \spc
+\irule{q \in \GP{string} \spc g_1, \cdots, g_m \in \GP{xgroup} \icr

        (\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{]}) \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}
+      {(\G, \TT{[} q\ \TT{attr}\ g_1 \TT{,} \cdots \TT{,} g_m \TT{]}) \daq S_1 \ssum \cdots \ssum S_m}

 %
 \end{center} 
 \begin{center} 
 %
 %
 \end{center} 
 \begin{center} 
 %

-\irule{q \in \GP{string} \spc a_1, \cdots, a_m \in \GP{xatr} \spc
+\irule{q \in \GP{string} \spc a_1, \cdots, a_m \in \GP{xatr} \icr

        (\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}
        (\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}


@@ -139,17 +139,16 @@ evaluated using the rules given below.
 \end{center} 
 \end{footnotesize}
 
 \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.
+$ \dsum $ and $ \ssum $ are helper functions describing the two union
+operations on {\av} sets: with and without attribute distribution respectively.

 
 \begin{footnotesize}
 \begin{center} \begin{tabular}{lrll}
 %
 1a &
 
 \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 $ \\ 
+$ (S_1 \sdor \{(r, A_1)\}) \ssum (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
+$ (S_1 \ssum S_2) \sor \{(r, A_1 \sor A_2)\} $ \\
+1b & $ S_1 \ssum 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)\} $ \\
 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)\} $ \\


@@ -158,14 +157,14 @@ $ (S_1 \dsum S_2) \sor \{(r, A_1 \distr A_2)\} $ \\
 \end{tabular} \end{center}
 \end{footnotesize}
 
 \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\} $.
+Rules 1a, 2a override 1b, 2b and
+$ A_1 \distr A_2 = \{G_1 \ssum G_2 \st G_1 \in A_1, G_2 \in A_2\} $.

 
 \item 
 
 \item 

-The semantics of \TT{property} operator is described below.
+The semantics of the \TT{property} operator is described below.

 
 In the following rule,
 
 In the following rule,

-$s$ is ``$ \TT{property}\ h\ p_1\ \TT{main}\ p_2\ \RM{attr}\ e_1, \cdots,
+$s$ is ``$ \TT{property}\ h\ p_1\ \TT{main}\ p_2\ \TT{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\}\} $:
 
 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\}\} $:
 


@@ -173,7 +172,7 @@ $A_2$ is $ \{ \Exp\ P\ p_1\ r_1\ \{e_1, \cdots, e_m\}\} $:
 \begin{center}
 %
 \irule
 \begin{center}
 %
 \irule

-{h \oft \GP{refine} \spc p_1, p_2 \oft \GP{path} \spc 
+{h \oft \GP{ref} \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}
  e_1, \cdots, e_m \oft \GP{exp} \spc k \in \TT{["pattern"]?} \spc 
  (\G, x) \daq S
 }{A}


@@ -188,12 +187,17 @@ $A_2$ is $ \{ \Exp\ P\ p_1\ r_1\ \{e_1, \cdots, e_m\}\} $:
 When the \TT{main} clause is not present, we assume $ p_2 = \TT{/} $.
 
 Here $ \Property\ h $ gives the appropriate access relation according to
 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{HighAccess}). 
-
+the $ h $ flag (this is the primitive function that inspects the {\RDF}
+graph, see \subsecref{HighAccess}).
+ 

 $ \Src\ k\ P\ V $ is a helper function giving the source set
 according to the $ k $ flag. $ \Src $ is based on $ \Match $, the helper
 $ \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:
+function handling {\POSIX} regular expressions.
+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{In {\POSIX} 1003.1-2001:
+\CURI{http://www.unix-systems.org/version3/ieee\_\,std.html}.}
+regular expression $ \verb+"^"+ \app s \app \TT{"\$"} $.

 
 \begin{footnotesize}
 \begin{center} \begin{tabular}{rll}
 
 \begin{footnotesize}
 \begin{center} \begin{tabular}{rll}


@@ -206,31 +210,22 @@ $ \Match\ W\ V $ & rewrites to & $ \bigsor \{\Pattern\ W\ s \st s \in V\} $
 \end{tabular} \end{center}
 \end{footnotesize}
 
 \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:
-\CURI{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
+$ \Exp\ P\ p_1\ r_1\ E $ is the helper function that builds the group of

 attributes specified in the \TT{attr} clause.
 attributes specified in the \TT{attr} clause.

-$ \Exp $ is based on $ \Exp\p $ which handles a single attribute. Formally:
+$ \Exp $ is based on $ \Exp\p $ which handles a single attribute. Formally,
+if $ p, p\p \oft \GP{path} $ and $ E \oft \Setof\ \GP{exp} $:

 
 \begin{footnotesize}
 
 \begin{footnotesize}

-\begin{center} \begin{tabular}{rlll}
+\begin{center} \begin{tabular}{rll}

 %
 $ f\ P\ r_1\ p_1\ p $ & rewrites to &
 %
 $ 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} $ \\
+$ \{ r_2 \st (r_1, p_1 \app (\Name\ p), r_2) \in P \} $ \\

 $ \Exp\p\ P\ r_1\ p_1\ p $ & rewrites to &
 $ \Exp\p\ P\ r_1\ p_1\ p $ & rewrites to &

-$ \{ (\Name\ p, f\ P\ r_1\ p_1\ p) \} $ & 
-with $ p \oft \GP{path} $ \\
+$ \{ (\Name\ p, f\ P\ r_1\ p_1\ p) \} $ \\

 $ \Exp\p\ P\ r_1\ p_1\ (p\ \TT{as}\ p\p) $ & rewrites to &
 $ \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} $ \\
+$ \{ (\Name\ p\p, f\ P\ r_1\ p_1\ p) \} $ \\

 $ \Exp\ P\ r_1\ p_1\ E $ & rewrites to &
 $ \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} $ 
+$ \bigsum \{ \Exp\p\ P\ r_1\ p_1\ e \st e \in E \} $ \\ 

 \end{tabular} \end{center}
 \end{footnotesize}
 
 \end{tabular} \end{center}
 \end{footnotesize}
 


@@ -258,7 +253,7 @@ $ (\lall c \in W)\ \Istrue\p\ P\ r_1\ p_1\ c $
 \end{footnotesize}
 
 For each clause ``\TT{isfalse} $ c_1, \cdots, c_n $'' the set $ P $
 \end{footnotesize}
 
 For each clause ``\TT{isfalse} $ c_1, \cdots, c_n $'' the set $ P $

-must be replaced with
+must be replaced with \newline

 $ \{ (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.
 $ \{ (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.


@@ -269,8 +264,7 @@ $ \{ (r_2, p, r_1) \st (r_1, p, r_2) \in P \} $.
 
 \end{itemize}
 
 
 \end{itemize}
 

-The second group of \GP{query} expressions includes the context manipulation
-facilities:
+The second group of \GP{query} expressions allows the context manipulation:

 
 \begin{itemize}
 
 
 \begin{itemize}
 


@@ -280,54 +274,53 @@ The operators for reading variables:
 \begin{footnotesize} \begin{center}
 %
 \irule{i \oft \GP{svar}}{}{(\g, i) \daq \get{\G_s}{i}} \spc
 \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}\}}
+\irule{i \oft \GP{evar}}{}{(\g, i) \daq \{\get{\G_e}{i}\}}

 %
 \end{center} \end{footnotesize}
 
 %
 \end{center} \end{footnotesize}
 

-$ \get{\G_s}{i} $ and $ \{\get{\G_a}{i}\} $ mean $ \ES $ if $ i $ is not defined.
+$ \get{\G_s}{i} $ and $ \{\get{\G_e}{i}\} $ mean $ \ES $ if $ i $ is not defined.

 
 \item 
 
 \item 

-The \TT{let} operator assigns an {\av} set variable (svar):
+The \TT{let} operator assigns a set variable (\GP{svar}):

 
 \begin{footnotesize} 
 \begin{center}
 %
 \irule{i \oft \GP{svar} \spc (\G_1, x_1) \daq (\g, S_1) \spc
 
 \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)}
+       ((\set{\G_s}{i}{S_1}, \G_e, \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}
 {}{(\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
+introducing a fresh variable, so ``$ x_1\ \TT{;;}\ x_2 $'' rewrites

 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
 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.
-
+in element variables.

 The \TT{ex} (exists) operator gives access to the groups of attributes
 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
+associated to the {\av}'s in the $ \G_e $ 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
 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
+pool of attribute groups, one for each {\av} in the $ \G_e $ part of the

 context. Formally we have the rules:
 
 \begin{footnotesize}
 \begin{center}
 %
 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}
+\irule{(\lall \D_g \in \All\ \G_e)\ ((\G_s, \G_e, \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}
 %
       {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\}}{}
+\irule {i \oft \GP{evar} \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}
        {(\G, i\TT{.}p) \daq \{(s_1, \ES), \cdots, (s_m, \ES)\}}
 %
 \end{center}


@@ -335,31 +328,29 @@ context. Formally we have the rules:
 
 where%
 \footnote{$\D_g$ has the type of $ \G_g $.}
 
 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} \} $,
+$ \All\ \G_e = \{\D_g \st \get{\D_g}{i} = G\ \RM{iff}\ G \in \Snd\ \get{\G_e}{i} \} $,

 and $ \G = \g $.
 
 Moreover $ \get{\get{\G_g}{i}}{\Name\ p} $ means $ \ES $
 if $ i $ or $ \Name\ p $ are not defined where appropriate.
 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}
 
 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:
+The third group of \GP{query} expressions allows the {\av} set manipulation:

 
 \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
 
 \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.
+according to the setting of the \TT{distr} flag.

 
 \begin{footnotesize} 
 \begin{center}
 %
 \irule
 
 \begin{footnotesize} 
 \begin{center}
 %
 \irule

-{h \in \TT{["distr"]?} \spc a \in \GP{xgroups} \spc 
+{h \in \TT{["distr"]?} \spc a \in \GP{xgroups} \icr 

  (\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)\}}
  (\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)\}}


@@ -368,54 +359,58 @@ according to the \TT{distr} flag.
 \begin{center}
 %
 \irule
 \begin{center}
 %
 \irule

-{h \in \TT{["distr"]?} \spc i \in \GP{avar} \spc  
+{h \in \TT{["distr"]?} \spc i \in \GP{evar} \spc  

  (\g, x) \daq \{(r_1, A_1), \cdots, (r_m, A_m)\}}{}
  (\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})\}}
+{(\g, \TT{add}\ i\ \TT{in}\ x) \daq \{(r_1, A_1 \jolly \Snd\ \get{\G_e}{i}), \cdots, (r_m, A_m \jolly \Snd\ \get{\G_e}{i})\}}

 %
 \end{center}
 \end{footnotesize}
 
 Where $ \jolly_{\tt""} = \sor $ and $ \jolly_{\tt"distr"} = \distr $.
 %
 \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.
+Moreover $ \Snd\ \get{\G_e}{i} = \ES $ if $i$ is not defined.

 
 \item
 
 \item

-The semantics of the \TT{for} operator is given in terms of the {\For} helper
+The semantics of the \TT{for} operator is given using the {\For} helper

 function:
 
 \begin{footnotesize}
 \begin{center}
 %
 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}}{}
+\irule{i \oft \GP{evar} \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}
+%
+\end{center} 
+\begin{center}
+%
+\irule{i \oft \GP{evar} \spc x_2 \oft \GP{query}}{}

       {\For\ h\ \G\ i\ x_2\ \ES\ \RM{rewrites to}\ (\G, \ES)}
 %
 \end{center} 
 \begin{center}
 %
       {\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)}
+\irule{i \oft \GP{evar} \spc ((\G_s, \set{\G_e}{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}
 
       {}{\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 $.
+Here we have $ R \oft T_3 $, $ \G = \g $, $ \jolly_{\tt"sup"} = \ssum $ and
+$ \jolly_{\tt"inf"} = \sprod $.

 
 

-$ \dprod $ and $ \prod $ are helper functions describing the two intersection
+$ \dprod $ and $ \sprod $ are helper functions describing the two intersection

 operations on {\av} sets: with and without attribute distribution respectively.
 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}.   
+They are dual to $ \dsum $ and $ \ssum $. $ \dprod $ does not appear in this
+version of {\MathQL} but was used in the earlier versions 
+\cite{Lor02,GS03,Gui03}.   

 
 \begin{footnotesize}
 \begin{center} \begin{tabular}{lrll}
 %
 1a &
 
 \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 $ \\ 
+$ (S_1 \sdor \{(r, A_1)\}) \sprod (S_2 \sdor \{(r, A_2)\}) $ & rewrites to &
+$ (S_1 \sprod S_2) \sor \{(r, A_1 \sor A_2)\} $ \\
+1b & $ S_1 \sprod 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)\} $ \\
 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)\} $ \\


@@ -424,7 +419,7 @@ $ (S_1 \dprod S_2) \sor \{(r, A_1 \distr A_2)\} $ \\
 \end{tabular} \end{center}
 \end{footnotesize}
 
 \end{tabular} \end{center}
 \end{footnotesize}
 

-As for $ \sum $ and $ \dsum $, rules 1a, 2a override rules 1b, 2b respectively.
+As for $ \ssum $ and $ \dsum $, rules 1a, 2a override rules 1b, 2b respectively.

 
 \item
 The semantics of the \TT{while} operator is given by the rules below:
 
 \item
 The semantics of the \TT{while} operator is given by the rules below:


@@ -440,20 +435,19 @@ The semantics of the \TT{while} operator is given by the rules below:
 %
 \irule
 {h \in \TT{["sup"|"inf"]} \spc (\G, x_1) \daq (\G_1, S_1) \spc
 %
 \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_1, x_2) \daq (\G_2, S_2) \icr 

  (\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}
 
  (\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.
+Again $ \jolly_{\tt"sup"} = \ssum $ and $ \jolly_{\tt"inf"} = \sprod $.
+Rule 1 takes precedence over rule 2.

 
 \end{itemize}
 
 
 \end{itemize}
 

-The forth group of \GP{query} constructions make {\MathQL} an extensible
-language.
+The forth group of \GP{query} constructions makes {\MathQL} extensible.

 
 \begin{itemize}
 
 
 \begin{itemize}
 


@@ -482,7 +476,7 @@ The core language does not include any external function and it is a mistake
 to invoke an undefined function.
 
 \item
 to invoke an undefined function.
 
 \item

-The \TT{gen} construction invokes an external function returning a \GP{query}
+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
 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


@@ -503,24 +497,21 @@ 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.
 \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.
+The construction ``\TT{gen} p \TT{in} x'' rewrites to ``\TT{gen} p \{x\}''.

 
 \end{itemize}
 
 \subsubsection*{Results}
 
 
 \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.
+An \GP{avs} expression (the explicit representation of an {\av} set denoting 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}{}
 
 \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}
+      {x_1 \TT{;} \cdots \TT{;} x_m \dar S_1 \ssum \cdots \ssum S_m}

 %
 \end{center} 
 \begin{center} 
 %
 \end{center} 
 \begin{center} 


@@ -528,7 +519,7 @@ following rules.
 \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}{}
 \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}
+      {q\ \TT{attr}\ g_1 \TT{,} \cdots \TT{,} g_m \dar S_1 \ssum \cdots \ssum S_m}

 %
 \end{center} 
 \begin{center} 
 %
 \end{center} 
 \begin{center} 


@@ -541,6 +532,13 @@ following rules.
 \end{center} 
 \begin{center} 
 %
 \end{center} 
 \begin{center} 
 %

+\irule{q, q_0 \in \GP{string} \spc p \in \GP{path}}{}
+      {q\ \TT{attr}\ \{ p = q_0 \} \dar 
+       \{(\Unquote\ q, \{ \{ (\Name\ p, \{ \Unquote\ q_0 \}) \} \})\}}
+%
+\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 \}) \} \})\}}
 \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 \}) \} \})\}}

diff --git a/helm/mathql/doc/mathql_overview.tex b/helm/mathql/doc/mathql_overview.tex
index 6d59b55fa92dcbeb5ef1abc20cb2d66704e69880..45fd2cb99f366fe50ea2a38ada18660058cd6219 100644 (file)
--- a/helm/mathql/doc/mathql_overview.tex
+++ b/helm/mathql/doc/mathql_overview.tex
@@ -16,7 +16,6 @@ database or on-line libraries reviewers, for proof assistants or
 proof-checking systems, and also for learning environments because these
 applications require features for classifying, searching and browsing
 mathematical information in a semantically meaningful way.
 proof-checking systems, and also for learning environments because these
 applications require features for classifying, searching and browsing
 mathematical information in a semantically meaningful way.

-

 Other languages to be defined in the context of the MathQL proposal may be
 suitable for queries about the semantic structure of mathematical data:
 this includes content-based pattern-matching and possibly other forms of
 Other languages to be defined in the context of the MathQL proposal may be
 suitable for queries about the semantic structure of mathematical data:
 this includes content-based pattern-matching and possibly other forms of


@@ -50,6 +49,8 @@ native support for post-processing the query results;
 We will briefly analyze these features in the remaining part of this
 section.
 
 We will briefly analyze these features in the remaining part of this
 section.
 

+\vspace{-1pc}
+

 \subsubsection*{The main requirements from the RDF community}
 
 As a query language for {\RDF} databases, {\MathQL} has a well-conceived
 \subsubsection*{The main requirements from the RDF community}
 
 As a query language for {\RDF} databases, {\MathQL} has a well-conceived


@@ -66,9 +67,8 @@ part of a solution should be preserved, and supports a machine-processable
 the best usability.
 The two syntaxes concern both queries and results, making {\MathQL} usable in
 a distributed environment where query engines are implemented as stand-alone
 the best usability.
 The two syntaxes concern both queries and results, making {\MathQL} usable in
 a distributed environment where query engines are implemented as stand-alone

-components. This is because in this setting both queries and query results
-must be exchanged by the system's components and thus need to be encoded in
-clearly defined format.
+components. In this setting in fact both the queries and their results must be
+exchanged by the system's components and thus need to be clearly encoded.

 
 {\MathQL} provides a graph-oriented access to the {\RDF} metadata, based on
 tree instantiation.
 
 {\MathQL} provides a graph-oriented access to the {\RDF} metadata, based on
 tree instantiation.


@@ -80,9 +80,11 @@ definitely desirable especially in a distributed context.
 {\MathQL} query results are meant to capture the structure of trees coming
 from an {\RDF} graph and for this purpose a standard $1$- or $2$-dimensional
 organization (as provided by most {\RDF}-oriented query languages) is not
 {\MathQL} query results are meant to capture the structure of trees coming
 from an {\RDF} graph and for this purpose a standard $1$- or $2$-dimensional
 organization (as provided by most {\RDF}-oriented query languages) is not

-satisfactory. Here {\MathQL} approach is to use a $4$-dimensional organization
+satisfactory. {\MathQL} approach is to use a $4$-dimensional organization

 for its query results.
 
 for its query results.
 

+\vspace{-1pc}
+

 \subsubsection*{Post-processing and code generation capabilities}
 
 The {\MathQL} query engine, that is written in {\CAML}%
 \subsubsection*{Post-processing and code generation capabilities}
 
 The {\MathQL} query engine, that is written in {\CAML}%


@@ -112,7 +114,6 @@ Moreover the language provides access to an extensible set of code-generating
 functions (also available at {\CAML} side) that the expert user can define
 writing suitable {\CAML} modules for the engine.
 Note that the generated code is always {\MathQL} code.
 functions (also available at {\CAML} side) that the expert user can define
 writing suitable {\CAML} modules for the engine.
 Note that the generated code is always {\MathQL} code.

-

 The code generation features allow to build complex queries incrementally and
 in an automatic manner, as required by the needs of the {\HELM} project.
 Using the native programming language, instead, queries can include the
 The code generation features allow to build complex queries incrementally and
 in an automatic manner, as required by the needs of the {\HELM} project.
 Using the native programming language, instead, queries can include the


@@ -123,6 +124,8 @@ In this sense the alternative of performing a complex query on a remote
 component issuing some {\MathQL} querying code followed by some {\CAML}
 post-processing code is really infeasible in a distributed context.  
 
 component issuing some {\MathQL} querying code followed by some {\CAML}
 post-processing code is really infeasible in a distributed context.  
 

+\vspace{-1pc}
+

 \subsubsection*{Physical organization of the RDF database}
 
 The implementation of the {\MathQL} query engine does not depend on any
 \subsubsection*{Physical organization of the RDF database}
 
 The implementation of the {\MathQL} query engine does not depend on any

diff --git a/helm/mathql/doc/mathql_tests.tex b/helm/mathql/doc/mathql_tests.tex
new file mode 100644 (file)
index 0000000..1e31b94
--- /dev/null
+++ b/helm/mathql/doc/mathql_tests.tex
@@ -0,0 +1,28 @@
+\section{A use case: retrieving the transitive principles} 
+
+In this section we briefly present one on the many queries that we are using
+to test {\MathQL}.4: the one that retrieves the transitive principles stored
+in the {\HELM} library. The details on the {\RDF} metadata used to index the
+contents of the library can be found in \cite{Sch02,Gui03,GSC03}.
+This query, executed in {\MySQL}-mode on an AMD Athlon 1.5 GHz, retrieved 
+$55$ {\HELM} objects (out of $41451$) in $4.00s$ (the interpreter worked
+for $0.31s$) after having issued $2205$ {\SQL} queries to the underlying
+database. This test was executed on April 2 2004 by the Author.
+
+\begin{footnotesize} \begin{verbatim}
+gen /"helm"/"aliases" in let $sets = property inverse /"refSort" istrue 
+/"h:sort" in $SET, /"h:position" in $MC, /"h:depth" in "0" of "" in let
+$prop = property inverse /"refSort" istrue /"h:sort" in $PROP, 
+/"h:position" in $MC, /"h:depth" in "2" of "" in let $rels0 = for @uri
+in $prop sup add {/"set" = property /"refObj" main /"h:occurrence" istrue
+/"h:position" in $MH of @uri} in @uri in let $rels = select @uri from
+$rels0 where ex ((count @uri./"set" eq "1") and (@uri./"set" sub $sets))
+in let $trans0 = for @uri in $rels sup add {/"rel" = @uri; /"set" = proj
+/"set" of @uri} in property inverse /"refObj" main /"h:occurrence" istrue
+/"h:position" in $MC, /"h:depth" in "5" of @uri in let $trans1 = for @uri
+in $trans0 sup add distr {/"premises" = property /"refObj" main /"h:occur
+rence" istrue /"h:position" in $MH of @uri; /"extra" = property /"refObj"
+main /"h:occurrence" istrue /"h:position" in {$IC, $IH} of @uri} in @uri
+in let $trans = select @uri from $trans1 where ex (not @uri./"extra" and
+(@uri./"premises" sub {@uri./"rel", @uri./"set"})) in keep $trans
+\end{verbatim} \end{footnotesize} %$