]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/DEVEL/mathml_editor/doc/spec.tex
This commit was manufactured by cvs2svn to create branch 'moogle'.
[helm.git] / helm / DEVEL / mathml_editor / doc / spec.tex
diff --git a/helm/DEVEL/mathml_editor/doc/spec.tex b/helm/DEVEL/mathml_editor/doc/spec.tex
deleted file mode 100644 (file)
index a9ccdc2..0000000
+++ /dev/null
@@ -1,973 +0,0 @@
-\documentclass[10pt]{article}
-
-\usepackage{a4wide}
-\usepackage{palatino}
-\usepackage{euler}
-\usepackage{amssymb}
-\usepackage{stmaryrd}
-\usepackage{wasysym}
-
-\title{\EdiTeX: a MathML Editor Based on \TeX{} Syntax\\\small Description and Formal Specification}
-\author{Paolo Marinelli\\Luca Padovani\\\small\{{\tt pmarinel},{\tt lpadovan}\}{\tt @cs.unibo.it}\\\small Department of Computer Science\\\small University of Bologna}
-\date{}
-
-\newcommand{\EdiTeX}{Edi\TeX}
-
-\newcommand{\tmap}[1]{\llbracket#1\rrbracket}
-\newcommand{\tadvance}{\vartriangle}
-\newcommand{\tnext}{\rhd}
-\newcommand{\G}{\texttt{g}}
-\newcommand{\PNODE}{\texttt{p}}
-\newcommand{\SNODE}{\texttt{s}}
-\newcommand{\INODE}{\texttt{i}}
-\newcommand{\NNODE}{\texttt{n}}
-\newcommand{\ONODE}{\texttt{o}}
-\newcommand{\CNODE}{\texttt{c}}
-\newcommand{\TABLE}{\texttt{table}}
-\newcommand{\SP}{\texttt{sp}}
-\newcommand{\SB}{\texttt{sb}}
-\newcommand{\CELL}{\texttt{cell}}
-\newcommand{\ROW}{\texttt{row}}
-\newcommand{\SLDROP}{\blacktriangleleft}
-\newcommand{\NLDROP}{\vartriangleleft}
-\newcommand{\RDROP}{\vartriangleright}
-
-\begin{document}
-
-\maketitle
-
-\section{Introduction}
-
-MathML~\cite{MathML1,MathML2,MathML2E} is an XML application for the
-representation of mathematical expressions. As most XML applications,
-MathML is unsuitable to be hand-written, except for the simplest
-cases, because of its verbosity. In fact, the MathML specification
-explicitly states that
-\begin{quote}
-``While MathML is human-readable, it is anticipated that, in all but
-the simplest cases, authors will use equation editors, conversion
-programs, and other specialized software tools to generate MathML''
-\end{quote}
-
-The statement about human readability of MathML is already too strong,
-as the large number of mathematical symbols, operators, and
-diacritical marks that are used in mathematical notation cause MathML
-documents to make extensive use of Unicode characters that typically
-are not in the ``visible'' range of common text editors. Such
-characters may appear as entity references, whose name indicates
-somehow the kind of symbol used, or character references or they are
-directly encoded in the document encoding scheme (for instance,
-UTF-8).
-
-It is thus obvious that authoring MathML documents assumes the
-assistance of dedicated tools. As of today, such tools can be
-classified into two main categories:
-\begin{enumerate}
-  \item WYSIWYG (What You See Is What You Get) editors that allow the
-    author to see the formatted document on the screen as it is
-    composed;
-  \item conversion tools that generate MathML markup from different
-    sources, typically other markup languages for scientific
-    documents, such as \TeX.
-\end{enumerate}
-
-While the former tools are certainly more appealing, especially to the
-unexperienced user, as they give a direct visual feedback, the
-existance of tools in the second category takes into account the large
-availability of existing documents in \TeX{} format, and also the fact
-that experienced or ``lazy'' users may continue to prefer the use of a
-markup language other than MathML for editing, and generate MathML
-only as a final step of the authoring process. The ``laziness'' is not
-really intended as a way of being reluctant towards a new technology,
-but rather as a justified convincement that WYSIWYG editors are ``nice
-to look at'' but after all they may slow down the authoring process.
-WYSIWYG editors often involve the use of menus, palettes of symbols,
-and, in general, an extensive use of the pointing device (the mouse)
-for completing most operations. The use of shortcuts is of little
-help, as it implies very soon a challenging exercise for the fingers
-and the mind. Moreover, authors \emph{cannot improve} their authoring
-speed with time.  On the other side, the gap between the syntax of any
-markup language for mathematics and mathematical notation may be
-relevant, especially for large, non-trivial formulas and authoring is
-a re-iterated process in which the author repeadtedly types the markup
-in the editor, compiles, and looks at the result inside a pre-viewer.
-
-\EdiTeX{} tries to synthesize the ``best of both worlds'' in a single
-tool. The basic idea is that of creating a WYSIWYG editor in which
-editing is achieved by typing \TeX{} markup as the author would do in
-a text editor. The \TeX{} markup is tokenized and parsed on-the-fly
-and a corresponding MathML representation is created and
-displayed. This way, the author can see the rendered document as it
-changes. The advantages of this approach can be summarized as follows:
-\begin{itemize}
-  \item the document is rendered concurrently with the editing, the
-    user has an immediate feedback hence it is easier to spot errors;
-  \item the author types in a concrete (and likely familiar) syntax
-    improving the editing speed;
-  \item the usual WYSIWYG mechanisms are still available. In
-    particular, it is possible to select \emph{visually} a fragment of
-    the document that needs re-editing, or that was left behind for
-    subsequent editing.
-\end{itemize}
-
-\paragraph{The Name of the Game:} there is no reference to MathML in
-the name ``\EdiTeX.'' In fact, the architecture of the editor is not
-tied to MathML markup. Although we focus on MathML editing, by
-changing a completely modularized component of the editor it is
-virtually possible to generate any other markup language.
-
-\paragraph{Acknowledgments.} Stephen M. Watt and Igor Rodionov for
-their work on the \TeX{} to MathML conversion tool; Stan Devitt for an
-illuminating discussion about the architecture of \TeX{} to XML
-conversion tools; Claudio Sacerdoti Coen for the valuable feedback and
-uncountable bug reports.
-
-\section{Architecture}
-
-\section{Customization}
-
-\subsection{Short and Long Identifiers}
-
-\subsection{The Dictionary}
-
-\subsection{Stylesheets and Trasformations}
-
-\subsection{Rendering}
-
-\section{XML Representation of \TeX{} Markup}
-
-\section{Tokens}
-
-The following tokens are defined:
-
-\begin{tabular}{lllp{0.5\textwidth}}
-  \textbf{\TeX{}} & \textbf{Notation} & \textbf{Node} & \textbf{Description} \\
-\hline
-  \verb+{+ & $\mathrm{begin}$ & \texttt{g} & Beginning of a group \\
-  \verb+}+ & $\mathrm{end}$ & & End of a group \\
-  \verb+$+ & $\$$ & \texttt{math} & Math shift \\ %$ \\
-  & &  & End-of-line \\
-  \verb+#+$i$ & $p(i)$ & \texttt{p} & Parameter \\
-  \verb+^+ & $\uparrow$ & \texttt{sp} & Superscript \\
-  \verb+_+ & $\downarrow$ & \texttt{sb} & Subscript \\
-  & $\square$ & & Space-like character that can be ignored \\
-  & $s$ & \texttt{s} & Space-like character that may be significant \\
-  letter & $i(v)$ & \texttt{i} & Identifier $v$ \\
-  digit & $n(v)$ & \texttt{n} & Number $v$ \\
-  other & $o(v)$ & \texttt{o} & Other character or operator $v$ \\
-  \verb+~+ & $\sim$ & & Active character \\
-  \verb+%+ & $\%$ & & Comment \\
-  control & $c(v)\langle\alpha_1,\dots,\alpha_n\rangle$ & \texttt{c} & 
-    Control sequence $v$ that expects the $\alpha_1,\dots,\alpha_n$ sequence of tokens. \\
-  backspace & $\vartriangleleft$ & & \\
-  backspace & $\blacktriangleleft$ & & \\
-\end{tabular}
-
-%% Some tokens are mapped directly into nodes of the TML tree. The following functions shows
-%% the mapping:
-
-\begin{tabular}{r@{\quad$=$\quad}l}
-  $\tmap{\{}$ & \verb+g+ \\
-  $\tmap{p(i)}$ & \verb+p[@index=+$i$\verb+]+ \\
-  $\tmap{p_l(i)}$ & \verb+p[@index=+$i$\verb+][@left-open='1']+ \\
-  $\tmap{p_r(i)}$ & \verb+p[@index=+$i$\verb+][@right-open='1']+ \\
-  $\tmap{s}$ & \verb+s+ \\
-  $\tmap{\uparrow}$ & \verb+sp+ \\
-  $\tmap{\downarrow}$ & \verb+sb+ \\
-  $\tmap{i(v)}$ & \verb+i[@value=+$v$\verb+]+ \\
-  $\tmap{n(v)}$ & \verb+n[@value=+$v$\verb+]+ \\
-  $\tmap{o(v)}$ & \verb+o[@value=+$v$\verb+]+ \\
-  $\tmap{c(v)\langle\alpha_1,\dots,\alpha_n\rangle}$ & \verb+c[@name=+$v$\verb+][^+$\tmap{\alpha_1}\cdots\tmap{\alpha_n}$\verb+$]+\\
-\end{tabular}
-%$
-
-\section{Description and Semantics of the Pattern Language}
-
-%% \begin{eqnarray*}
-%%   \mathit{NodeTest} & ::= & \mathtt{*} \\
-%%   & | & \mathit{ElementType} \\
-%%   & | & \mathtt{<}~\mathit{ElementTypePattern}~\mathtt{>} \\[1ex]
-%%   \mathit{ElementTypePattern} & ::= & \mathtt{*} \\
-%%   & | & \mathit{ElementType}~(\mathtt{|}~\mathit{ElementType})^* \\
-%%   & | & \mathtt{!}\mathit{ElementType}~(\mathtt{|}~\mathit{ElementType})^*\\[1ex]
-%%   \mathit{NodePattern} & ::= & \mathit{NodeTest}~\mathit{AttributeQualifier}^*\\[1ex]
-%%   \mathit{AttributeQualifier} & ::= & \mathtt{[@}\mathit{AttributeTest}\mathtt{]}\\
-%%   & | & \mathtt{[!@}\mathit{AttributeTest}\mathtt{]}\\[1ex]
-%%   \mathit{AttributeTest} & ::= & \mathit{AttributeName} \\
-%%   & | & \mathit{AttributeName}\mathtt{='}\mathit{Text}\mathtt{'}
-%% \end{eqnarray*}
-
-\begin{table}
-\[
-\begin{array}{rcl@{\hspace{3em}}rcl@{\hspace{3em}}rcl}
-  C &::=& .               & Q &::=& \langle*\rangle                  & P &::=& P'\#P' \\
-  &|& ..                  & &|& \langle!*\rangle                     & &|& \cent P'\#P'\\
-  &|& /                   & &|& \langle n_1\mid\cdots\mid n_k\rangle & &|& P'\#P'\$\\%$
-  &|& Q                   & &|& \langle!n_1\mid\cdots\mid n_k\rangle & &|& \cent P'\#P'\$\\%$
-  &|& (C)                 & &|& Q[@n]                                & & &\\
-  &|& \{C:\Gamma\}        & &|& Q[!@n]                               & P' &::=& \\
-  &|& C\&C                & &|& Q[@n=v]                              & &|& C\;P'\\
-  &|& C\mid C             & &|& Q[!@n=v]                             & & &\\
-  &|& C+                  & &|& Q[P]                                 & & &\\
-  &|& C?                  & &|& Q[!P]                                & & &\\
-  &|& C*                  & & &                                      & & &\\ 
-  &|& C\;C                & & &                                      & & &\\
-  &|& !C                  & & &                                      & & &\\
-\end{array}
-\]
-\caption{Syntax of the regular context language. $n$, $n_i$ denote
-names, $v$ denotes a string enclosed in single or double quotes}
-\end{table}
-
-
-\section{Insert Rules}
-
-\paragraph{Begin Group:} $\{$
-
-\begin{description}
-  \item{\verb+table/cursor+}\\
-   create a \texttt{row} node, create a \texttt{cell} node, create a \texttt{g} node,
-    append the cursor to the \texttt{g} node, append the \texttt{g} node to the \texttt{cell} node,
-    append the \texttt{cell} node to the \texttt{row} node, append the \texttt{row} node to the
-    \texttt{c} node 
-  \item{\verb+cursor+} \\ create a \texttt{g} node, replace the cursor with the new \texttt{g} node,
-    append the cursor to the new \texttt{g} node
-\end{description}
-
-% CASE: c/g[!@id]/cursor
-
-% CASE: c/cursor
-
-% ELSE:
-
-% do_begin:
-% CASE: c[@table='1']/cursor
-% ELSE:
-%   create a g node with id, replace the cursor with the fresh g and append
-%   the cursor as only child of it
-
-\paragraph{End Group:} $\}$
-
-\begin{description}
-  \item{\verb+g[@id]/cursor+}\\
-  remove the cursor, put $\tadvance$ after the \texttt{g} node
-  \item{\verb+row/cell/g/cursor+}\\
-  remove the cursor, put $\tadvance$ after the \texttt{row} node
-  \item{\verb+math/g[!@id]/cursor+}\\
-  ?
-  \item{\verb+cursor+}\\
-  error ?
-\end{description}
-
-\paragraph{Math Shift:} $\$$
-
-\begin{description}
-  \item{\verb+tex/cursor+}\\
-  create a \texttt{math} node, create a \texttt{g} node, append the \texttt{g} node
-    as child of the \texttt{math} node, append the cursor as child of the \texttt{g} node
-  \item{\verb+math[@display='1']/g[!@id][*#]/cursor+}\\
-  append the cursor as last child of the \texttt{math} node
-  \item{\verb+math/g[!@id][*#]/cursor+}\\
-  remove the cursor
-  \item{\verb+math[!display='1']/g[!@id]/cursor+}\\
-  set \verb+display='1'+ in the \texttt{math} node
-  \item{\verb+math/g[!@id]+}\\
-  append the cursor after the \texttt{math} node
-  \item{\verb+math/cursor+}\\
-  remove the cursor
-  \item{\verb+cursor+} \\
-  error ?
-\end{description}
-
-% do_shift:
-% CASE: tex/cursor
-%   create a math node. create a g node. append g as child of math.
-%   append the cursor as child of g
-% CASE: math[@display='1']/g[!@id][*#]/cursor
-%   append the cursor as last child of math
-% CASE: math/g[!@id][*#]/cursor
-%   remove the cursor. Editing is done
-% CASE: math[!display='1']/g[!@id]/cursor
-%   set the display attribute to '1'
-% CASE: math/g[!@id]
-%   append the cursor after math (?)
-% CASE: math/cursor
-%   remove the cursor. Editing is done
-% ELSE:
-%   error
-
-\paragraph{Align:} $\&$
-
-\begin{description}
-  \item{\verb+g[@id]/cursor+}\\
-  create a \texttt{row} node, create a \texttt{cell} node, create a \texttt{g} node,
-    append the cursor to the new \texttt{g} node, append the \texttt{cell} node to the
-    the \texttt{row} node ?
-  \item{\verb+row/cell/g/cursor+}\\
-  create the \texttt{g} node, create the \texttt{cell} node, append the cursor
-    as child of the new \texttt{g} node, append the new \texttt{g} node to the new
-    \texttt{cell} node after the old \texttt{cell} node
-  \item{\verb+cursor+}\\
-  error
-\end{description}
-
-% do_align:
-% CASE: g[@id]/cursor
-%   create a row node. create a cell node. create a g node. append the
-%   cursor to g, append the g to cell, append the cell to row, ???
-% CASE: row/cell/g/cursor
-%   create a g node. create a cell node. appent the cursor to g,
-%   append the g to cell, insert the new cell after the existing cell
-% ELSE:
-%   error
-
-\paragraph{End-of-line:}
-
-% do_eol:
-%   ignored
-
-\paragraph{Parameter:} $p(i)$
-% do_parameter:
-%   ignored
-
-\paragraph{Superscript:} $\uparrow$
-
-\begin{description}
-  \item{\verb+<g|p>[^#]/cursor+}\\
-  create a \SP{} node, create a \G{} node, replace the cursor with the \SP{} node,
-    append the \G{} node as first child of the \SP{} node, append the cursor as last
-    child of the \SP{} node
-  \item{\verb+<g|p>[*#]/cursor+}\\
-  create a \SP{} node, replace \texttt{*} with the \SP{} node, append \texttt{*} to
-    the \SP{} node, append cursor to the \SP{} node
-  \item{\verb+sp[^*#$][!@over='1']/cursor+}\\ %$
-  set \verb+over='1'+ in the \SP{} node
-  \item{\verb+sp[^*#$][@over='1']/cursor+}\\ %$
-  error
-  \item{\verb+cursor+}\\
-  error ?
-\end{description}
-% do_superscript:
-% CASE: g[^#]/cursor
-%   create sp node. create g node, replace cursor with sp, append g to sp, append cursor to sp
-% CASE: g[*#]/cursor
-%   create sp node, replace * with sp, append * to sp, append cursor to sp
-% CASE: sp[^*#$][!@over='1']/cursor
-%   set over='1' in sp node
-% CASE: sp[^*#$][@over='1']/cursor
-%   error
-% ELSE:
-%   error ?
-
-\paragraph{Subscript:} $\downarrow$
-
-\begin{description}
-  \item{\verb+<g|p>[^#]/cursor+}\\
-  create a \SB{} node, create a \G{} node, replace the cursor with the \SB{} node,
-    append the \G{} node as first child of the \SB{} node, append the cursor as last
-    child of the \SB{} node
-  \item{\verb+<g|p>[*#]/cursor+}\\
-  create a \SB{} node, replace \texttt{*} with the \SB{} node, append \texttt{*} to
-    the \SB{} node, append cursor to the \SB{} node
-  \item{\verb+sb[^*#$][!@under='1']/cursor+}\\ %$
-  set \verb+under='1'+ in the \SB{} node
-  \item{\verb+sb[^*#$][@under='1']/cursor+}\\ %$
-  error
-  \item{\verb+cursor+}\\
-  error ?
-\end{description}
-% do_subscript:
-% CASE: g[^#]/cursor
-%   create sb node. create g node, replace cursor with sb, append g to sb, append cursor to sb
-% CASE: g[*#]/cursor
-%   create sb node, replace * with sb, append * to sb, append cursor to sb
-% CASE: sb[^*#$][!@under='1']/cursor
-%   set over='1' in sb node
-% CASE: sb[^*#$][@under='1']/cursor
-%   error
-% ELSE:
-%   error ?
-
-\paragraph{Ignorable space:} $\square$
-
-% do_ignorable_space:
-%   do nothing?
-
-\paragraph{Space:} $s$
-
-\begin{description}
-  \item{\verb+cursor+}\\
-  create \SNODE{} node, replace cursor with the \SNODE{} node, append
-  $\tadvance$ after \SNODE{} node
-\end{description}
-
-% do_space
-%   create s node, replace cursor with s, append \advance after s
-
-\paragraph{Identifier:} $i(v)$
-
-\begin{description}
-  \item{\verb+cursor+}\\
-  create an \INODE{}, set \verb+value=+$v$ in the \INODE{}, replace
-  cursor with \INODE{}, append $\tadvance$ after the \INODE{} node
-\end{description}
-
-% do_identifier
-%   create i node, replace cursor with i, append \advance after i
-
-\paragraph{Number:} $n(v)$
-
-\begin{description}
-  \item{\verb+cursor+}\\
-  create an \NNODE{}, set \verb+value=+$v$ in the \NNODE{}, replace
-  cursor with \NNODE{}, append $\tadvance$ after the \NNODE{} node
-\end{description}
-
-% do_number
-%   create n node, replace cursor with n, append \advance after n
-
-\paragraph{Apostrophe:} $o({}')$
-
-\begin{description}
-  \item{\verb+<g/p>[(sp[*#$]/g[o[@name='prime']$])#]/cursor+}\\
-  create a \ONODE{} node, set \verb+name='prime'+ in the \ONODE{},
-    append the \ONODE{} to the innermost \G{} node
-  \item{\verb+<g|p>[(sb[^sp[^*#$]/g[o[@name='prime']]$])#]/cursor+}\\
-  create a \ONODE{} node, set \verb+name='prime'+ in the \ONODE{},
-    append the \ONODE{} to the innermost \G{} node
-  \item{\verb+<g|p>[*#]/cursor+}\\
-  create a \ONODE{} node, set \verb+name='prime'+ in the \ONODE{},
-    create a \SP{} node, create a \G{} node, replace \texttt{*} with \SP{} node,
-    append the new \G{} node to the \SP{} node, append the \ONODE{}
-    node to the new \G{} node
-  \item{\verb+<g|p>[^#]/cursor+}\\
-  error?
-  \item{\verb+cursor+}\\
-  cursor is not in a group, error?
-\end{description}
-
-% do_apostrophe
-% CASE: g[(sp[^*#$]/g[o[@name='prime']$])#]/cursor
-%   append a new o[@name='prime'] node to the inner g node
-% CASE: g[(sb[^sp[^*#$]/g[o[@name='prime']]$])#]/cursor
-%   append a new o[@name='prime'] node to the inner g node
-% CASE: g[*#]/cursor
-%   create sp node, create g node, replace * with sp, append * to sp, append g to sp,
-%   append a new o[@name='prime'[ node to the new g node
-% CASE: g[^#]/cursor
-%   error?
-% ELSE:
-%   cursor is not in a group, error?
-
-\paragraph{Other:} $o(v)$
-
-create an \ONODE{}, set \verb+value=+$v$ in the \ONODE{}, replace
-cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
-
-% do_other
-%   create o node, replace cursor with o, append \advance after o
-
-\paragraph{Active:} $\sim$
-
-% do_active:
-%   ignored ???
-
-\paragraph{Comment:} $\%$
-
-% do_comment:
-%   ignored ???
-
-\paragraph{Begin Environment:} $c(\mathtt{begin})\langle\alpha_1,\dots,\alpha_n\rangle$
-
-\paragraph{End Environment:} $c(\mathtt{end})\langle\rangle$
-
-\paragraph{Left Delimiter:} $c(\mathtt{left})\langle\alpha\rangle$
-
-\paragraph{Right Delimiter:} $c(\mathtt{right})\langle\alpha\rangle$
-
-\paragraph{Carriage-Return:} $c(\mathtt{cr})\langle\rangle$
-
-\begin{description}
-  \item{\verb+row/cell/g/cursor+}\\
-  create a \ROW{} node, create a \CELL{} node, create a \G{}
-    node, append the cursor to the new \G{} node, append the new \G{}
-    node to the new \CELL{} node, append the new \CELL{} node to the
-    new \ROW{} node, insert the new \ROW{} node after the old \ROW{} node
-  \item{\verb+cursor+}\\
-  ignored?
-\end{description}
-
-% do_cr:
-% CASE: row/cell/g/cursor
-%   create row node, create cell node, create g node,
-%   append cursor to g, append g to cell, append cell to row,
-%   insert new row after old row
-% ELSE:
-%   ignored ???
-
-\paragraph{Macro:} $c(v)\langle\alpha_1,\dots,\alpha_n\rangle$
-
-\begin{description}
-  \item{\verb+<p|g>/cursor+}\\
-  create a \CNODE{} node with the children corresponding to the pattern
-  $\tmap{\alpha_1}$,\dots,$\tmap{\alpha_n}$, replace the cursor with
-  the new \CNODE{} node. put $\tnext$ as the first child of the new
-  \CNODE{} node
-
-  \item{\verb+*/cursor+}\\
-  create a \CNODE{} node with the children corresponding to the pattern
-  $\tmap{\alpha_1}$,\dots,$\tmap{\alpha_n}$, replace the cursor with
-  the new \CNODE{} node, put $\tnext$ as the first child of the new
-  \CNODE{} node. If $n\ne0$ emit a warning (the macro has arguments but
-  but the context wouldn't normally allow them to be entered)
-\end{description}
-
-% do_macro:
-% CASE: g/cursor
-%   create a c node with children corresponding to the pattern of the macro
-%   append \nextparam as first child of the macro
-
-\section{Left Drop Rules}
-
-\paragraph{Normal Left Drop:} $\NLDROP$
-
-\begin{description}
-
-  \item{\verb+cursor+}\\
-  replace the cursor with the $\NLDROP$.
-
-\end{description}
-
-\paragraph{Special Left Drop:} $\SLDROP$
-
-\begin{description}
-
-  \item{\verb+cursor+}\\
-  replace the cursor with the $\SLDROP$.
-
-\end{description}
-
-\section{Right Drop Rules}
-
-\begin{description}
-
-  \item{\verb+cursor+}\\
-  replace the cursor with the $\RDROP$.
-
-\end{description}
-
-\section{$\varepsilon$-rules}
-
-\paragraph{Nromal Left Drop}
-
-\begin{description}
-
-  \item{\verb+math/g[^#]/+$\NLDROP$}\\
-  repalce the $\NLDROP$ with the cursor.
-
-  %**************************************************************************************
-  %****************************** epsilon-rules with \NLDROP ****************************
-  %**************************************************************************************
-
-  %**************  \NLDROP has neither preceding nor following nodes ********************
-
-  \item{\verb+math[^#$]/+$\NLDROP$}\\
-  replace the $\NLDROP$ with the cursor.
-
-  \item{\verb+g[^#$]/+$\NLDROP$}\\
-  replace the \G{} node with the $\NLDROP$.
-
-  % this rule is overridden by the two ones below
-  \item{\verb+c/p[^#$]/+$\NLDROP$}\\
-  remove the $\NLDROP$ and insert it before the \PNODE{} node.
-
-  \item{\verb+c[p[@left-open='1'][*]#$]/p[@right-open='1'][^#$]/+$\NLDROP$}\\
-  replace the \CNODE{} node with the content of the first \PNODE{} node and insert the $\NLDROP$ after this content
-
-  \item{\verb+c[p[@left-open='1'][!*]#$]/p[@right-open='1'][^#$]/+$\NLDROP$}\\
-  replace the \CNODE{} node with the $\NLDROP$.
-
-  \item{\verb+c[^#][!p(*)]/+$\NLDROP$}\\
-  replace the \CNODE{} node with the $\NLDROP$.
-
-  \item{\verb+cell[^#$]/+$\NLDROP$}\\
-  replace the cell with the $\NLDROP_n$.
-
-  \item{\verb+table[^#$]/+$\NLDROP$}\\
-  replace the \TABLE{} node with the $\NLDROP$.
-
-  %************************* \NLDROP has at least one preceding node *********************
-
-  % general rules
-
-  % this rule should also handles the case where the \NLDROP is the third (and last) child of a script.
-  \item{\verb+*[*#]/+$\NLDROP$}\\
-  remove the $\NLDROP$ and append it as the last child of its ex preceding brother.
-
-  % this rule overrides the one above
-  \item{\verb+*[(i|n|o|s|c[!*])#]/+$\NLDROP$}\\
-  remove the $\NLDROP$ and replace the token with the $\NLDROP_n$.
-
-  % special rules
-
-  \item{\verb+<sp|sb>[^*#$]+/$\NLDROP$}\\
-  replace the script node with its first child and insert the $\NLDROP$ after it.
-
-  % this rule overrides the one above.
-  \item{\verb+<sp|sb>[^g[!@id][!*]#$]/+$\NLDROP$}\\
-  replace the script with the cursor.
-
-  % this rule overrides the one above
-  \item{\verb+*[sp[!@id][^*g[!@id][^o[@name='prime']++\verb+o[@name='prime']$]]#]/+$\NLDROP$}\\
-  remove the last \ONODE{} node and replace the $\NLDROP$ with the cursor.%$\NLDROP_n$.
-
-  \item{\verb+*[sp[!@id][^*g[!@id][^o[@name='prime']$]]#]/+$\NLDROP$}\\
-  replace the script with its first child and replace the $\NLDROP$ with the cursor.%$\NLDROP_n$.
-
-  \item{\verb+c[(i|n|o|s|c[!*])#]/+$\NLDROP$}\\
-  move the $\NLDROP$ before the delimiter.
-
-  % this rule is true for both right-open and parameterized macros.
-  \item{\verb+c[p#]/+$\NLDROP$}\\
-  move the $\NLDROP$ into the \PNODE{} node.
-
-  %**************** \NLDROP has no preceding nodes, but has following nodes **************
-
-  % general rule
-  \item{\verb+*[^#*]/+$\NLDROP$}\\
-  remove the $\NLDROP$ and insert it before its parent.
-
-  % special rules
-
-  % this rule is applicable to all macros.
-  \item{\verb+c[^#][p[*]]/+$\NLDROP$}\\
-  remove the $\NLDROP$ and insert it before the \CNODE{} node.
-
-\end{description}
-
-\paragraph{Special Left Drop}
-
-\begin{description}
-
-  %********************************************************************************************************
-  %************************************ epsilon-rules with \SLDROP ****************************************
-  %********************************************************************************************************
-
-  \item{\verb+math/+$\SLDROP$}\\
-  replace the $\SLDROP$ with the cursor.
-
-  \item{\verb+math/g[^#]/+$\NLDROP$}\\
-  replace the $\NLDROP$ with the cursor.
-
-  %************************ \SLDROP has neither preceding nor following nodes *****************************
-
-  \item{\verb+g[^#$]/+$\SLDROP$}\\
-  replace the \G{} node with the cursor.
-
-  \item{\verb+c[p[@left-open='1'][*]#$]/p[@right-open='1'][^#$]/+$\SLDROP$}\\
-  replace the \CNODE{} node with the content of the first \PNODE{} node and insert the cursor after this content
-
-  \item{\verb+c[p[@left-open='1'][!*]#$]/p[@right-open='1'][^#$]/+$\SLDROP$}\\
-  replace the \CNODE{} node with the cursor.
-
-  \item{\verb+c/p[^#$]/+$\SLDROP$}\\
-  remove the $\SLDROP$ and insert it before the \PNODE{} node.
-
-  \item{\verb+c[^#][!p(*)]/+$\SLDROP$}\\
-  replace the \CNODE{} node with the cursor.
-
-  \item{\verb+cell[^#$]/+$\SLDROP$}\\
-  replace the cell with the $\NLDROP_n$.
-
-  \item{\verb+table[^#$]/+$\SLDROP$}\\
-  replace the \TABLE{} node with the cursor.
-
-  %*********************** \SLDROP has at least one preceding node ***********************************
-
-  \item{\verb+*[sp[!@id][^*g[!@id][^o[@name='prime']++\verb+o[@name='prime']$]]#]/+$\SLDROP$}\\
-  remove the last \ONODE{} node and replace the $\SLDROP$ with the cursor.
-
-  \item{\verb+*[sp[!@id][^*g[!@id][^o[@name='prime']$]]#]/+$\SLDROP$}\\
-  replace the script with its first child and replace the $\SLDROP$ with the cursor.%$\NLDROP_n$.
-
-  \item{\verb+<sp|sb>[^g[!@id][!*]#$]/+$\SLDROP$}\\
-  replace the script with the cursor.
-
-  % this rule is overridden by the three rules above.
-  \item{\verb+<sp|sb>[^*#$]+/$\SLDROP$}\\
-  replace the script node with its first child and insert the cursor after it.
-
-  \item{\verb+c[(i|n|o|s|c[!*])#]/+$\SLDROP$}\\
-  remove the $\SLDROP$ and insert the cursor before the delimiter.
-
-  \item{\verb+c[p#(i|n|o|s|c[!*])]/+$\SLDROP$}\\
-  remove the $\SLDROP$ and insert the cursor into the \PNODE{} node.
-
-  \item{\verb+c[p[@right-open='1']#]+}\\
-  remove the $\SLDROP$ and append the curor as last child of the \PNODE{} node.
-
-  % this rule is overridden by the two ones above.
-  \item{\verb+c[p#]/+$\SLDROP$}\\
-  move the $\SLDROP$ into the \PNODE{} node.
-
-  \item{\verb+*[(i|n|o|s|c[!*])#]/+$\SLDROP$}\\
-  remove the $\SLDROP$ and replace the token with the cursor.
-
-  \item{\verb+*[table#]/+$\SLDROP$}\\
-  remove the $\SLDROP$ and append the $\NLDROP_n$ as the last child of the \TABLE{} node.
-
-  \item{\verb+*[c#]/+$\SLDROP$}\\
-  move the $\SLDROP$ into the \CNODE{} node.
-
-  \item{\verb+*[g#]/+$\SLDROP$}\\
-  remove the $\SLDROP$ and append the cursor as the last child of the \G{} node.
-
-  %********** \SLDROP has no preceding node, but has following ones **************
-
-  \item{\verb+c[^#p][p(*)]/+$\SLDROP$}\\
-  remove the $\SLDROP$ and insert the cursor before the \CNODE{} node.
-
-  % general rule
-  \item{\verb+*[^#*]/+$\SLDROP$}\\
-  remove the $\SLDROP$ and insert the cursor before its parent.
-
-\end{description}
-
-\paragraph{Normalize Left Drop}
-
-\begin{description}
-
-  %****************************************************************************************
-  %***************************** epsilon-rules with \NLDROP_n *****************************
-  %****************************************************************************************
-
-  \item{\verb+*[*#]/+$\NLDROP_n$}\\
-  replace the $\NLDROP_n$ with the cursor.
-
-  \item{\verb+row[cell#]/+$\NLDROP_n$}\\
-  remove the $\NLDROP_n$ and append the cursor as the last child of the \CELL{} node.
-
-  \item{\verb+row[^#$]/+$\NLDROP_n$}\\
-  replace the \ROW{} node with the $\NLDROP_n$
-
-  \item{\verb+table[row#]/+$\NLDROP_n$}\\
-  remove the $\NLDROP_n$ and append it as last child of the \ROW{} node.
-
-  \item{\verb+table[^#$]/+$\NLDROP_n$}\\
-  replace the \TABLE{} with the cursor.%$\NLDROP_n$.
-
-  \item{\verb+g[@id][^#$]/+$\NLDROP_n$}\\
-  replace the \G{} node with the $\NLDROP_n$.
-
-  \item{$\NLDROP_n$}\\
-  replace the $\NLDROP_n$ with the cursor.
-
-\end{description}
-
-\paragraph{Right Drop}
-
-\begin{description}
-
-  %************************* \RDROP has at least a following node ****************************************
-
-  \item{\verb+c[#(i|n|o|s|c[!*])]/+$\RDROP$}\\
-  remove the $\RDROP$ and append it after the delimiter
-
-  \item{\verb+*[#(i|n|o|s|c[!*])]/+$\RDROP$}\\
-  remove the token and replace the $\RDROP$ with the cursor $\RDROP_n$.
-
-  % this rule is overridden by those ones above.
-  \item{\verb+*[#*]/+$\RDROP$}\\
-  remove the $\RDROP$ and append it as the first child of the following node.
-
-  %************************** \RDROP has neither following nor preceding nodes ******************************
-
-  \item{\verb+c[#$][!p[*]]/+$\RDROP$}\\
-  replace the \CNODE{} with the $\RDROP$.
-
-  \item{\verb+p[^#$]/+$\RDROP$}\\
-  move the $\RDROP$ after the \PNODE{} node.
-
-  \item{\verb+g[^#$]/+$\RDROP$}\\
-  replace the \G{} node with the $\RDROP$.
-
-\end{description}
-
-\paragraph{Normalize Right Drop}
-
-\begin{description}
-
-  % at the moment it's the only rule, defined for this symbol.
-  \item{\verb+g[@id][^#$]/+$\RDROP_n$}\\
-  replace the \G{} node with the $\RDROP_n$.
-
-  \item{$\RDROP_n$}\\
-  replace the $\RDROP$ with the cursor.
-
-\end{description}
-
-\paragraph{Advance}
-
-\begin{description}
-  \item{\verb+g/+$\tadvance$}\\
-  replace $\tadvance$ with the cursor
-
-  \item{\verb+p[#$]/+$\tadvance$}\\ %$
-  put $\tadvance$ after the \PNODE{} node
-
-  \item{\verb+c[#p]/+$\tadvance$} \\
-  remove $\tadvance$, put the cursor as first child of the \PNODE{} node
-
-  \item{\verb+c[#*]/+$\tadvance$} \\ %$
-  replace $\tadvance$ with the cursor 
-
-  \item{\verb+c[#$]/+$\tadvance$} \\ %$
-  move $\tadvance$ after the \CNODE{} node
-\end{description}
-
-\paragraph{Next Parameter}
-
-\paragraph{Next Token}
-
-%% \begin{description}
-%%   \item{\verb+c[#p]/+$\tnext$} \\
-%% \end{description}
-
-% g[@id]/(c[#$][@right-open]/g[!@id][#$]/)+cursor  }   let p = cursor.parent() in remove; advance(p)
-
-% c/g[!@id]/cursor
-% c/cursor 
-% */cursor  {   let g = new group in replace
-
-% g[@id][^#$]/cursor  <=   cursor.parent().replace(cursor)
-% g[@id][^#$]/cursor  <-   cursor
-% (!g[@id][^#$])[A#B]/(g[@id][^#$]/)+cursor  <-  (!g[@id][^#$])[A#B]/cursor  
-
-\clearpage
-\appendix
-\section{Semantics of the Regular Context Language}
-
-\newcommand{\CSEM}[2]{\mathcal{C}\llbracket#1\rrbracket#2}
-\newcommand{\QSEM}[2]{\mathcal{Q}\llbracket#1\rrbracket#2}
-\newcommand{\TSEMUP}[2]{\mathcal{T}^\uparrow\llbracket#1\rrbracket#2}
-\newcommand{\TSEMDOWN}[2]{\mathcal{T}_\downarrow\llbracket#1\rrbracket#2}
-\newcommand{\NSEM}[2]{\mathcal{N}\llbracket#1\rrbracket#2}
-\newcommand{\PSEM}[1]{\mathcal{P}\llbracket#1\rrbracket}
-\newcommand{\LSEM}[2]{\mathcal{L}\llbracket#1\rrbracket#2}
-\newcommand{\RSEM}[2]{\mathcal{R}\llbracket#1\rrbracket#2}
-\newcommand{\FSEM}[2]{\mathcal{F}\llbracket#1\rrbracket(#2)}
-\newcommand{\PARENT}[1]{\mathit{parent}(#1)}
-\newcommand{\CHILDREN}[1]{\mathit{children}(#1)}
-\newcommand{\CHILD}[1]{\mathit{child}(#1)}
-\newcommand{\ANCESTORS}[1]{\mathit{ancestors}(#1)}
-\newcommand{\DESCENDANTS}[1]{\mathit{descendants}(#1)}
-\newcommand{\HASATTRIBUTE}[2]{\mathit{hasAttribute}(#1,#2)}
-\newcommand{\HASNOATTRIBUTE}[2]{\mathit{hasNoAttribute}(#1,#2)}
-\newcommand{\ATTRIBUTE}[2]{\mathit{attribute}(#1,#2)}
-\newcommand{\ISELEMENT}[1]{\mathit{isElement}(#1)}
-\newcommand{\NAME}[1]{\mathit{name}(#1)}
-\newcommand{\PREV}[1]{\mathit{prev}(#1)}
-\newcommand{\NEXT}[1]{\mathit{next}(#1)}
-\newcommand{\PREDICATE}[1]{\mathit{predicate}(#1)}
-\newcommand{\IFV}[3]{\begin{array}[t]{@{}l}\mathbf{if}~#1~\mathbf{then}\\\quad#2\\\mathbf{else}\\\quad#3\end{array}}
-\newcommand{\IFH}[3]{\mathbf{if}~#1~\mathbf{then}~#2~\mathbf{else}~#3}
-\newcommand{\TRUE}{\mathbf{true}}
-\newcommand{\FALSE}{\mathbf{false}}
-\newcommand{\FUN}[2]{\lambda#1.#2}
-\newcommand{\LET}[3]{\mathbf{let}~#1=#2~\mathbf{in}~#3}
-\newcommand{\REC}[2]{\mathbf{rec}~#1=#2}
-\newcommand{\APPLY}[2]{(#1\;#2)}
-\newcommand{\APPLYX}[3]{(#1\;#2\;#3)}
-\newcommand{\AND}{\wedge}
-\newcommand{\OR}{\vee}
-\newcommand{\AAND}{\,\vec{\AND}\,}
-\newcommand{\AOR}{\,\vec{\OR}\,}
-\newcommand{\MATCH}[4]{\begin{array}[t]{@{}c@{~\to~}l@{}l@{}}\multicolumn{2}{@{}l@{}}{\mathbf{match}~#1~\mathbf{with}}\\\phantom{|}\quad\{#2\}&#3\\|\quad\emptyset&#4\end{array}}
-
-\[
-\begin{array}{rcl}
-  \CSEM{q}{x} &=& \{x_1\mid x_1\in\{x\} \wedge \QSEM{q}{x_1}\}\\
-  \CSEM{..}{x} &=& \PARENT{x}\\
-  \CSEM{/}{x} &=& \CHILDREN{x}\\
-  \CSEM{c_1\;c_2}{x} &=& \CSEM{c_2}{\CSEM{c_1}{x}}\\
-  \CSEM{(c)}{x} &=& \CSEM{c}{x}\\
-  \CSEM{\{c:\alpha\}}{x} &=& \alpha(x,\CSEM{c}{x})\\
-  \CSEM{c_1\&c_2}{x} &=& \CSEM{c_1}{x} \cap \CSEM{c_2}{x}\\
-  \CSEM{c_1\mid c_2}{x} &=& \CSEM{c_1}{x} \cup \CSEM{c_2}{x}\\
-  \CSEM{c+}{x} &=& \CSEM{c}{x} \cup \CSEM{c+}{\CSEM{c}{x}}\\
-  \CSEM{c?}{x} &=& \{x\}\cup\CSEM{c}{x}\\
-  \CSEM{c*}{x} &=& \CSEM{{c+}?}{x}\\[3ex]
-  \QSEM{c}{x} &=& \CSEM{c}{x}\ne\emptyset\\
-  \QSEM{!c}{x} &=& \CSEM{c}{x}=\emptyset\\
-  \QSEM{\langle*\rangle}{x} &=& \TRUE\\
-  \QSEM{\langle n\rangle}{x} &=& \NAME{x}=n\\
-  \QSEM{@n}{x} &=& \HASATTRIBUTE{x}{n}\\
-  \QSEM{@n=v}{x} &=& \ATTRIBUTE{x}{n}=v\\
-  \QSEM{[p_1\#p_2]}{x} &=& \LSEM{p_1}{\PREV{x}}\wedge\RSEM{p_2}{\NEXT{x}}\\[3ex]
-  \LSEM{}{\alpha} &=& \TRUE\\
-  \LSEM{\cent}{\alpha} &=& \alpha=\emptyset\\
-  \LSEM{p\;q}{\emptyset} &=& \FALSE\\
-  \LSEM{p\;q}{\{x\}} &=& \QSEM{q}{x}\wedge\LSEM{p}{\PREV{x}}\\[3ex]
-  \RSEM{}{\alpha} &=& \TRUE\\
-  \RSEM{\$}{\alpha} &=& \alpha=\emptyset\\
-  \RSEM{q\;p}{\emptyset} &=& \FALSE\\
-  \RSEM{q\;p}{\{x\}} &=& \QSEM{q}{x}\wedge\RSEM{p}{\NEXT{x}}\\[3ex]
-  \PREDICATE{q} &=& \TRUE\\
-  \PREDICATE{..} &=& \FALSE\\
-  \PREDICATE{/} &=& \FALSE\\
-  \PREDICATE{c_1\;c_2} &=& \PREDICATE{c_1}\wedge\PREDICATE{c_2}\\
-  \PREDICATE{(c)} &=& \PREDICATE{c}\\
-  \PREDICATE{c_1\&c_2} &=& \PREDICATE{c_1}\wedge\PREDICATE{c_2}\\
-  \PREDICATE{c_1\mid c_2} &=& \PREDICATE{c_1}\wedge\PREDICATE{c_2}\\
-  \PREDICATE{c+} &=& \PREDICATE{c}\\
-  \PREDICATE{c?} &=& \PREDICATE{c}\\
-  \PREDICATE{c*} &=& \PREDICATE{c}
-\end{array}
-\]
-
-\[
-\begin{array}{rcl}
-  \PSEM{q} &=& \FUN{x}{\APPLY{\QSEM{q}{}}{x}} \\
-  \PSEM{..} &=& \FUN{x}{\neg\APPLY{\mathit{null}}{\PARENT{x}}}\\
-  \PSEM{/} &=& \FUN{x}{\neg\APPLY{\mathit{null}}{\CHILD{x}}}\\
-  \PSEM{(c)} &=& \PSEM{c}\\
-  \PSEM{\{c:\alpha\}} &=& \FUN{x}{\APPLY{\PSEM{c}}{x}\AAND\APPLY{\alpha}{x}}\\
-  \PSEM{c_1\;c_2} &=& \IFV{\PREDICATE{c_1}}{\FUN{x}{(\PSEM{c_1}\;x)\wedge(\PSEM{c_2}\;x)}}{\FSEM{c_1}{\PSEM{c_2},\FUN{\_}{\FALSE}}}\\
-  \PSEM{c_1\&c_2} &=& \IFV{\PREDICATE{c_1}\wedge\PREDICATE{c_2}}{\FUN{x}{(\PSEM{c_1}\;x)\wedge(\PSEM{c_2}\;x)}}{\FSEM{c_1\&c_2}{\FUN{\_}{\TRUE},\FUN{\_}{\FALSE}}}\\
-  \PSEM{c_1\mid c_2} &=& \FUN{x}{(\PSEM{c_1}\;x)\vee(\PSEM{c_2}\;x)}\\
-  \PSEM{c+} &=& \PSEM{c}\\
-  \PSEM{c?} &=& \FUN{\_}{\TRUE}\\
-  \PSEM{c*} &=& \FUN{\_}{\TRUE}\\[3ex]
-  \FSEM{q}{t,f} &=& \FUN{x}{(\APPLY{\PSEM{q}}{x}\AAND\APPLY{t}{x})\AOR\APPLY{f}{x}}\\
-  \FSEM{..}{t,f} &=& \FUN{x}{\MATCH{\PARENT{x}}{y}{\APPLY{t}{y}}{\APPLY{f}{x}}}\\
-%  \FSEM{/}{t,f} &=& \FUN{x}{(\vee_{y\in\CHILDREN{x}} \APPLY{t}{y})\AOR\APPLY{f}{x}}\\
-  \FSEM{/}{t,f} &=& \FUN{x}{\APPLYX{\mathit{exists}}{t}{\CHILD{x}}\AOR\APPLY{f}{x}}\\
-  \FSEM{(c)}{t,f} &=& \FSEM{c}{t,f}\\
-  \FSEM{\{c:\alpha\}}{t,f} &=& \FSEM{c}{\FUN{x}{\PSEM{c}\AAND\APPLY{\alpha}{x}\AAND\APPLY{t}{x},f}}\\
-  \FSEM{c_1\;c_2}{t,f} &=& \FUN{x}{\APPLY{\FSEM{c_1}{\FSEM{c_2}{t,\FUN{\_}{\APPLY{f}{x}}},f}}{x}}\\
-  \FSEM{c_1\&c_2}{t,f} &=& \FUN{x}{\APPLY{\FSEM{c_1}{\FUN{y}{\APPLY{\FSEM{c_2}{\FUN{z}{(y=z)\AAND\APPLY{t}{z}},\FUN{\_}{\APPLY{f}{x}}}}{x}},f}}{x}}\\
-  \FSEM{c_1\mid c_2}{t,f} &=& \FSEM{c_1}{t,\FSEM{c_2}{t,f}}\\
-  \FSEM{c+}{t,f} &=& \FSEM{c}{\FSEM{c+}{t,t},f}\\
-  \FSEM{c?}{t,f} &=& \FSEM{c}{t,t}\\
-  \FSEM{c*}{t,f} &=& \FSEM{{c+}?}{t,f}\\[3ex]
-  \QSEM{c}{} &=& \PSEM{c}\\
-  \QSEM{!c}{} &=& \FUN{x}{\neg\APPLY{\PSEM{c}}{x}}\\
-  \QSEM{\langle*\rangle}{} &=& \FUN{\_}{\TRUE}\\
-  \QSEM{\langle n\rangle}{} &=& \FUN{x}{\NAME{x}=n}\\
-  \QSEM{@n}{} &=& \FUN{x}{\HASATTRIBUTE{x}{n}}\\
-  \QSEM{@n=v}{} &=& \FUN{x}{\ATTRIBUTE{x}{n}=v}\\
-  \QSEM{[p_1\#p_2]}{} &=& \FUN{x}{\APPLY{\LSEM{p_1}{}}{\PREV{x}}\wedge\APPLY{\RSEM{p_2}{}}{\NEXT{x}}}\\[3ex]
-  \LSEM{}{} &=& \FUN{\_}{\TRUE}\\
-  \LSEM{\cent}{} &=& \mathit{null}\\
-  \LSEM{p\;q}{} &=& \FUN{x}{\MATCH{x}{y}{\QSEM{q}{y}\AAND\APPLY{\LSEM{p}}{\PREV{y}}}{\FALSE}}\\
-  \RSEM{}{} &=& \FUN{\_}{\TRUE}\\
-  \RSEM{\$}{} &=& \mathit{null}\\
-  \RSEM{p\;q}{} &=& \FUN{x}{\MATCH{x}{y}{\QSEM{q}{y}\AAND\APPLY{\RSEM{p}}{\NEXT{y}}}{\FALSE}}\\
-  \mathit{null} &=& \FUN{x}{\MATCH{x}{\_}{\FALSE}{\TRUE}}\\
-  \mathit{exists} &=& \FUN{t}{\REC{a}{\FUN{x}{\MATCH{x}{y}{\APPLY{t}{y}\AOR\APPLY{a}{\NEXT{x}}}{\FALSE}}}}
-\end{array}
-\]
-
-
-
-\end{document}