From: Luca Padovani Date: Thu, 3 Apr 2003 21:52:52 +0000 (+0000) Subject: * major update in regular context language definition and semantics X-Git-Tag: before_refactoring~54 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ced0086b4bb5b10e6c4a8268ea781624a41394dd;p=helm.git * major update in regular context language definition and semantics --- diff --git a/helm/DEVEL/mathml_editor/doc/spec.tex b/helm/DEVEL/mathml_editor/doc/spec.tex index 504825ae6..be9ba51bb 100644 --- a/helm/DEVEL/mathml_editor/doc/spec.tex +++ b/helm/DEVEL/mathml_editor/doc/spec.tex @@ -5,6 +5,7 @@ \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} @@ -180,7 +181,7 @@ The following tokens are defined: \end{tabular} %$ -%% \section{Description and Semantics of the Pattern Language} +\section{Description and Semantics of the Pattern Language} %% \begin{eqnarray*} %% \mathit{NodeTest} & ::= & \mathtt{*} \\ @@ -196,6 +197,28 @@ The following tokens are defined: %% & | & \mathit{AttributeName}\mathtt{='}\mathit{Text}\mathtt{'} %% \end{eqnarray*} +\begin{table} +\[ +\begin{array}{rcl@{\hspace{3em}}rcl@{\hspace{3em}}rcl} + C &::=& Q\verb+/+ & Q &::=& T & P &::=& P' \\ + &|& Q\verb+//+ & &|& Q\verb+[@+n\verb+=+v\verb+]+ & &|& \verb+^+P'\\ + &|& \verb+(+C\verb+)+ & &|& Q\verb+[!@+n\verb+=+v\verb+]+ & &|& P'\verb+$+\\%$ + &|& (\alpha\verb+=+C) & &|& Q\verb+[@+n\verb+]+ & &|& \verb+^+P'\verb+$+\\%$ + &|& C_1 \verb+&+ C_2 & &|& Q\verb+[+P\verb+]+ & & &\\ + &|& C_1 \verb+|+ C_2 & & & & P' &::=& P''\\ + &|& C\verb.+. & T &::=& N & &|& P''\verb+#+P''\\ + &|& C\verb+*+ & &|& C N & & &\\ + &|& C\verb+?+ & & & & P'' &::=& \\ + &|& C_1~C_2 & N &::=& \verb+<*>+ & &|& T\;P''\\ + &|& \verb+!+C & &|& \verb+<+n_1\verb+|+\cdots\verb+|+n_2\verb+>+ & & &\\ + & & & &|& \verb++ & & &\\ +\end{array} +\] +\caption{Syntax of the pattern language. $n$, $n_i$ denote names, $v$ +denotes a string enclosed in single or double quotes} +\end{table} + + \section{Insert Rules} \paragraph{Begin Group:} $\{$ @@ -819,4 +842,64 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node % 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}[2]{\mathcal{P}\llbracket#1\rrbracket#2} +\newcommand{\PPSEM}[2]{\mathcal{P'}\llbracket#1\rrbracket(#2)} +\newcommand{\PARENT}[1]{\mathit{parent}(#1)} +\newcommand{\CHILDREN}[1]{\mathit{children}(#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)} + +\[ +\begin{array}{rcl} + \CSEM{.}{x} &=& \{x\}\\ + \CSEM{..}{x} &=& \PARENT{x}\\ + \CSEM{/}{x} &=& \CHILDREN{x}\\ + \CSEM{q}{x} &=& \{x_1\mid x_1\in\{x\} \wedge \QSEM{q}{x_1}\}\\ + \CSEM{(c)}{x} &=& \CSEM{c}{x}\\ + \CSEM{\alpha(c)}{x} &=& \CSEM{c}{x}, \mbox{bind $\alpha$ to $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} &=& \CSEM{.\mid c}{x}\\ + \CSEM{c*}{x} &=& \CSEM{{c+}?}{x}\\ + \CSEM{c_1\;c_2}{x} &=& \CSEM{c_2}{\CSEM{c_1}{x}}\\[3ex] + \QSEM{\langle*\rangle}{x} &=& \ISELEMENT{x}\\ + \QSEM{\langle!*\rangle}{x} &=& \neg\QSEM{\langle*\rangle}{x}\\ + \QSEM{\langle n_1\mid\cdots\mid n_k\rangle}{x} &=& \exists i\in\{1,\dots,k\}:\NAME{x}=n_i\\ + \QSEM{\langle !n_1\mid\cdots\mid n_k\rangle}{x} &=& \neg\QSEM{\langle n_1\mid\cdots\mid n_k\rangle}{x}\\ + \QSEM{q[@n]}{x} &=& \QSEM{q}{x} \wedge \HASATTRIBUTE{x}{n}\\ + \QSEM{q[!@n]}{x} &=& \QSEM{q}{x} \wedge \HASNOATTRIBUTE{x}{n}\\ + \QSEM{q[@n=v]}{x} &=& \QSEM{q}{x} \wedge \ATTRIBUTE{x}{n}= v\\ + \QSEM{q[!@n=v]}{x} &=& \QSEM{q}{x} \wedge \ATTRIBUTE{x}{n}\ne v\\ + \QSEM{q[p]}{x} &=& \QSEM{q}{x} \wedge \PSEM{p}{x}\\ + \QSEM{q[!p]}{x} &=& \QSEM{q}{x} \wedge \neg\PSEM{p}{x}\\[3ex] + \PSEM{p_1\#p_2}{x} &=& \PPSEM{p_1}{*,x}\wedge\PPSEM{p_2}{x,*}\\ + \PSEM{\cent p_1\#p_2}{x} &=& \PPSEM{p_1}{\cent,x}\wedge\PPSEM{p_2}{x,*}\\ + \PSEM{p_1\#p_2\$}{x} &=& \PPSEM{p_1}{*,x}\wedge\PPSEM{p_2}{x,\$}\\ + \PSEM{\cent p_1\#p_2\$}{x} &=& \PPSEM{p_1}{\cent,x}\wedge\PPSEM{p_2}{x,\$}\\[3ex] + \PPSEM{}{*,x} &=& \mathit{true}\\ + \PPSEM{}{\cent,x} &=& \PREV{x}=\emptyset\\ + \PPSEM{}{x,*} &=& \mathit{true}\\ + \PPSEM{}{x,\$} &=& \NEXT{x}=\emptyset\\ + \PPSEM{p\;c}{\alpha,x} &=& \CSEM{c}{\PREV{x}}\ne\emptyset\wedge\PPSEM{p}{\alpha,\PREV{x}}\\ + \PPSEM{c\;p}{x,\alpha} &=& \CSEM{c}{\NEXT{x}}\ne\emptyset\wedge\PPSEM{p}{\NEXT{x},\alpha}\\ +\end{array} +\] + \end{document}