From: Luca Padovani <luca.padovani@unito.it>
Date: Sat, 5 Apr 2003 19:21:15 +0000 (+0000)
Subject: * set-based + functional semantics
X-Git-Tag: before_refactoring~48
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3e4cd0c8f1cd759faa56060770e1686009e9a552;p=helm.git

* set-based + functional semantics
---

diff --git a/helm/DEVEL/mathml_editor/doc/spec.tex b/helm/DEVEL/mathml_editor/doc/spec.tex
index 7849651d9..87e2cd603 100644
--- a/helm/DEVEL/mathml_editor/doc/spec.tex
+++ b/helm/DEVEL/mathml_editor/doc/spec.tex
@@ -852,8 +852,10 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
 \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{\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{\ANCESTORS}[1]{\mathit{ancestors}(#1)}
@@ -865,44 +867,82 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
 \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}{\mathit{true}}
+\newcommand{\FALSE}{\mathit{false}}
+\newcommand{\FUN}[2]{\lambda#1.#2}
 
 \[
 \begin{array}{rcl}
-  \CSEM{.}{x} &=& \{x\}\\
+  \CSEM{q}{x} &=& \{x_1\mid x_1\in\{x\} \wedge \QSEM{q}{x_1}\}\\
   \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_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} &=& \CSEM{.\mid c}{x}\\
-  \CSEM{c*}{x} &=& \CSEM{{c+}?}{x}\\
-  \CSEM{c_1\;c_2}{x} &=& \CSEM{c_2}{\CSEM{c_1}{x}}\\
-  \CSEM{!c}{x} &=& \{x_1\mid x_1\in\{x\} \wedge \CSEM{c}{x}=\emptyset\}\\[3ex]
+  \CSEM{c*}{x} &=& \CSEM{{c+}?}{x}\\[3ex]
+  \QSEM{c}{x} &=& \CSEM{c}{x}\ne\emptyset\\
+  \QSEM{!c}{x} &=& \CSEM{c}{x}=\emptyset\\
+  \QSEM{.}{x} &=& \TRUE\\
   \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}{*,\PREV{x}}\wedge\PPSEM{p_2}{\NEXT{x},*}\\
-  \PSEM{\cent p_1\#p_2}{x} &=& \PPSEM{p_1}{\cent,\PREV{x}}\wedge\PPSEM{p_2}{\NEXT{x},*}\\
-  \PSEM{p_1\#p_2\$}{x} &=& \PPSEM{p_1}{*,\PREV{x}}\wedge\PPSEM{p_2}{\NEXT{x},\$}\\
-  \PSEM{\cent p_1\#p_2\$}{x} &=& \PPSEM{p_1}{\cent,\PREV{x}}\wedge\PPSEM{p_2}{\NEXT{x},\$}\\[3ex]
-  \PPSEM{}{*,\alpha} &=& \mathit{true}\\
-  \PPSEM{}{\cent,\alpha} &=& \alpha=\emptyset\\
-  \PPSEM{p\;c}{\alpha,\emptyset} &=& \mathit{false}\\
-  \PPSEM{p\;c}{\alpha,\{x\}} &=& \CSEM{c}{x}\ne\emptyset\wedge\PPSEM{p}{\alpha,\PREV{x}}\\
-  \PPSEM{}{\alpha,*} &=& \mathit{true}\\
-  \PPSEM{}{\alpha,\$} &=& \alpha=\emptyset\\
-  \PPSEM{c\;p}{\emptyset,\alpha} &=& \mathit{false}\\
-  \PPSEM{c\;p}{\{x\},\alpha} &=& \CSEM{c}{x}\ne\emptyset\wedge\PPSEM{p}{\NEXT{x},\alpha}\\
+  \QSEM{\langle n\rangle}{x} &=& \ISELEMENT{x}\wedge\NAME{x}=n\\
+  \QSEM{@n}{x} &=& \ISELEMENT{x}\wedge\HASATTRIBUTE{x}{n}\\
+  \QSEM{@n=v}{x} &=& \ISELEMENT{x}\wedge\ATTRIBUTE{x}{n}=v\\
+  \QSEM{[p_1\#p_2]}{x} &=& \ISELEMENT{x}\wedge\LSEM{p_1}{\PREV{x}}\wedge\RSEM{p_2}{\NEXT{x}}\\[3ex]
+  \LSEM{}{\alpha} &=& \TRUE\\
+  \LSEM{\cent}{\alpha} &=& \alpha=\emptyset\\
+  \LSEM{p\;q}{\emptyset} &=& \mathit{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} &=& \mathit{false}\\
+  \RSEM{q\;p}{\{x\}} &=& \QSEM{q}{x}\wedge\RSEM{p}{\NEXT{x}}\\
+\end{array}
+\]
+
+\[
+\begin{array}{rcl}
+  \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}{\QSEM{q}{x}} \\
+  \PSEM{..} &=& \FUN{x}{\PARENT{x}\ne\emptyset}\\
+  \PSEM{/} &=& \FUN{x}{\CHILDREN{x}\ne\emptyset}\\
+  \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}}}\\
+  \PSEM{(c)} &=& \PSEM{c}\\
+  \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}}}\\
+  \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}\\
+  \PSEM{!c} &=& \FUN{x}{\neg(\PSEM{c}\;x)}\\[3ex]
+  \FSEM{q}{l} &=& \FUN{x}{\IFH{(\PSEM{q}\;x)}{(l\;x)}{\FALSE}}\\
+  \FSEM{..}{l} &=& \FUN{x}{\IFH{\PARENT{x}=\{y\}}{(l\;y)}{\FALSE}}\\
+  \FSEM{/}{l} &=& \FUN{x}{\vee_{p\in\CHILDREN{x}} (l\;p)}\\
+  \FSEM{c_1\;c_2}{l} &=& \FUN{x}{(\FSEM{c_1}{\FSEM{c_2}{l}}\;x)}\\
+  \FSEM{c_1\&c_2}{l} &=& \FUN{x}{(\FSEM{c_1}{\FUN{y}{\IFH{(l\;y)}{(\FSEM{c_2}{\FUN{z}{z=y}}\;x)}{\FALSE}}}\;x)}\\
+  \FSEM{c_1\mid c_2}{l} &=& \FUN{x}{(\FSEM{c_1}{l}\;x)\vee(\FSEM{c_2}{l}\;x)}\\
+  \FSEM{c+}{l} &=& \FUN{x}{(\FSEM{c}{\FUN{y}{(l\;y)\vee(\FSEM{c+}{l}\;y)}}\;x)}\\
+  \FSEM{c?}{l} &=& \FUN{x}{(l\;x)\vee(\FSEM{c}{l}\;x)}\\
+  \FSEM{c*}{l} &=& \FSEM{{c+}?}{l}\\
 \end{array}
 \]