From: Luca Padovani <luca.padovani@unito.it>
Date: Sun, 6 Apr 2003 09:07:22 +0000 (+0000)
Subject: * new semantics with 2 continuations
X-Git-Tag: before_refactoring~46
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5f420bd186321bd74d0b7346fc8941e4d9abd4de;p=helm.git

* new semantics with 2 continuations
---

diff --git a/helm/DEVEL/mathml_editor/doc/spec.tex b/helm/DEVEL/mathml_editor/doc/spec.tex
index c99c65909..a55f950c0 100644
--- a/helm/DEVEL/mathml_editor/doc/spec.tex
+++ b/helm/DEVEL/mathml_editor/doc/spec.tex
@@ -873,6 +873,12 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
 \newcommand{\TRUE}{\mathit{true}}
 \newcommand{\FALSE}{\mathit{false}}
 \newcommand{\FUN}[2]{\lambda#1.#2}
+\newcommand{\LET}[3]{\mathbf{let}~#1=#2~\mathbf{in}~#3}
+\newcommand{\APPLY}[2]{(#1\;#2)}
+\newcommand{\AND}{\wedge}
+\newcommand{\OR}{\vee}
+\newcommand{\AAND}{\,\vec{\AND}\,}
+\newcommand{\AOR}{\,\vec{\OR}\,}
 
 \[
 \begin{array}{rcl}
@@ -926,23 +932,23 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
   \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_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)} &=& \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\&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}{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)}{l} &=& \FSEM{c}{l}\\
-  \FSEM{c_1\;c_2}{l} &=& \FSEM{c_1}{\FSEM{c_2}{l}}\\
-  \FSEM{c_1\&c_2}{l} &=& \FUN{x}{(\FSEM{c_1}{\FUN{y}{(l\;y)\wedge(\FSEM{c_2}{\FUN{z}{z=y}}\;x)}}\;x)}\\
-  \FSEM{c_1\mid c_2}{l} &=& \FUN{x}{(\FSEM{c_1}{l}\;x)\vee(\FSEM{c_2}{l}\;x)}\\
-  \FSEM{c+}{l} &=& \FSEM{c}{\FUN{y}{(l\;y)\vee(\FSEM{c+}{l}\;y)}}\\
-  \FSEM{c?}{l} &=& \FUN{x}{(l\;x)\vee(\FSEM{c}{l}\;x)}\\
-  \FSEM{c*}{l} &=& \FSEM{{c+}?}{l}\\
+  \FSEM{q}{t,f} &=& \FUN{x}{(\APPLY{\PSEM{q}}{x}\AAND\APPLY{t}{x})\AOR\APPLY{f}{x}}\\
+  \FSEM{..}{t,f} &=& \FUN{x}{\LET{\{y\}}{\PARENT{x}}{\APPLY{t}{y}\AOR\APPLY{f}{x}}}\\
+  \FSEM{/}{t,f} &=& \FUN{x}{(\vee_{y\in\CHILDREN{x}} \APPLY{t}{y})\AOR\APPLY{f}{x}}\\
+  \FSEM{(c)}{t,f} &=& \FSEM{c}{t,f}\\
+  \FSEM{c_1\;c_2}{t,f} &=& \FSEM{c_1}{\FSEM{c_2}{t,\FUN{\_}{\FALSE}},f}\\
+  \FSEM{c_1\&c_2}{t,f} &=& \FUN{x}{\APPLY{\FSEM{c_1}{\FUN{y}{\APPLY{t}{y}\AAND\APPLY{\FSEM{c_2}{\FUN{z}{z=y},\FUN{\_}{\FALSE}}}{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}\\
 \end{array}
 \]