X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2Fdoc%2Fmain.tex;h=9885e542079ccc5a4401c05b0211eb63f0cead90;hb=e4e8adaec753165a73a3acfa20c5d97a405e5dfa;hp=f27cebdd6ce0e5274407471dda8784ee152f9285;hpb=0c3432b87b1bd4636dda94e8db0c2d1e23e0246a;p=helm.git

diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex
index f27cebdd6..9885e5420 100644
--- a/helm/ocaml/cic_notation/doc/main.tex
+++ b/helm/ocaml/cic_notation/doc/main.tex
@@ -1,10 +1,10 @@
-\documentclass[a4paper]{article}
+\documentclass[a4paper,draft]{article}
 
 \usepackage{manfnt}
 \usepackage{a4wide}
 \usepackage{pifont}
 \usepackage{semantic}
-\usepackage{stmaryrd}
+\usepackage{stmaryrd,latexsym}
 
 \newcommand{\BLOB}{\raisebox{0ex}{\small\manstar}}
 
@@ -21,11 +21,15 @@
 \newcommand{\NVAR}[1]{#1:\mathtt{number}}
 \newcommand{\IVAR}[1]{#1:\mathtt{name}}
 \newcommand{\FENCED}[1]{\texttt{\char'050}#1\texttt{\char'051}}
-\newcommand{\IOT}[2]{|[#1|]_{\mathcal#2}^1}
+\newcommand{\ITO}[2]{|[#1|]_{\mathcal#2}^1}
+\newcommand{\IOT}[2]{|[#1|]_{\mathcal#2}^2}
 \newcommand{\ADDPARENS}[2]{\llparenthesis#1\rrparenthesis^{#2}}
 \newcommand{\NAMES}{\mathit{names}}
 \newcommand{\DOMAIN}{\mathit{domain}}
 
+\mathlig{~>}{\leadsto}
+\mathlig{|->}{\mapsto}
+
 \begin{document}
   \maketitle
 
@@ -127,7 +131,7 @@ used in different contexts.
 \end{table}
 
 \[
-\IOT{\cdot}{{}} : P -> \mathit{Env} -> T
+\ITO{\cdot}{{}} : P -> \mathit{Env} -> T
 \]
 
 \begin{table}
@@ -135,23 +139,23 @@ used in different contexts.
 \hrule
 \[
 \begin{array}{rcll}
-  \IOT{L_\kappa[P_1,\dots,P_n]}{E} & = & L_\kappa[\IOT{(P_1)}{E},\dots,\IOT{(P_n)}{E} ] \\
-  \IOT{B_\kappa^{ab}[P_1\cdots P_n]}{E} & = & B_\kappa^{ab}[\IOT{P_1}{E}\cdots\IOT{P_n}{E}] \\
-  \IOT{\BREAK}{E} & = & \BREAK \\
-  \IOT{(P)}{E} & = & \IOT{P}{E} \\
-  \IOT{(P_1\cdots P_n)}{E} & = & B_H^{00}[\IOT{P_1}{E}\cdots\IOT{P_n}{E}] \\
-  \IOT{\TVAR{x}}{E} & = & t & \mathcal{E}(x) = \verb+Term+~t \\
-  \IOT{\NVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+Number+~l \\
-  \IOT{\IVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+String+~l \\
-  \IOT{\mathtt{opt}~P}{E} & = & \varepsilon & \mathcal{E}(\NAMES(P)) = \{\mathtt{None}\} \\
-  \IOT{\mathtt{opt}~P}{E} & = & \IOT{P}{E'} & \mathcal{E}(\NAMES(P)) = \{\mathtt{Some}~v_1,\dots,\mathtt{Some}~v_n\} \\
+  \ITO{L_\kappa[P_1,\dots,P_n]}{E} & = & L_\kappa[\ITO{(P_1)}{E},\dots,\ITO{(P_n)}{E} ] \\
+  \ITO{B_\kappa^{ab}[P_1\cdots P_n]}{E} & = & B_\kappa^{ab}[\ITO{P_1}{E}\cdots\ITO{P_n}{E}] \\
+  \ITO{\BREAK}{E} & = & \BREAK \\
+  \ITO{(P)}{E} & = & \ITO{P}{E} \\
+  \ITO{(P_1\cdots P_n)}{E} & = & B_H^{00}[\ITO{P_1}{E}\cdots\ITO{P_n}{E}] \\
+  \ITO{\TVAR{x}}{E} & = & t & \mathcal{E}(x) = \verb+Term+~t \\
+  \ITO{\NVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+Number+~l \\
+  \ITO{\IVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+String+~l \\
+  \ITO{\mathtt{opt}~P}{E} & = & \varepsilon & \mathcal{E}(\NAMES(P)) = \{\mathtt{None}\} \\
+  \ITO{\mathtt{opt}~P}{E} & = & \ITO{P}{E'} & \mathcal{E}(\NAMES(P)) = \{\mathtt{Some}~v_1,\dots,\mathtt{Some}~v_n\} \\
   & & & \mathcal{E}'(x)=\left\{
   \begin{array}{@{}ll}
     v, & \mathcal{E}(x) = \mathtt{Some}~v \\
     \mathcal{E}(x), & \mbox{otherwise}
   \end{array}
   \right. \\
-  \IOT{\mathtt{list}k~P~l?}{E} & = & \IOT{P}{{E}_1}~{l?}\cdots {l?}~\IOT{P}{{E}_n} &
+  \ITO{\mathtt{list}k~P~l?}{E} & = & \ITO{P}{{E}_1}~{l?}\cdots {l?}~\ITO{P}{{E}_n} &
     \mathcal{E}(\NAMES(P)) = \{[v_{11},\dots,v_{1n}],\dots,[v_{m1},\dots,v_{mn}]\} \\
     & & & n\ge k \\
   & & & \mathcal{E}_i(x) = \left\{
@@ -160,7 +164,7 @@ used in different contexts.
     \mathcal{E}(x), & \mbox{otherwise}
   \end{array}
   \right. \\
-  \IOT{l}{E} & = & l \\
+  \ITO{l}{E} & = & l \\
 
 %%     &  |  & (P) & \mbox{(fenced)} \\
 %%     &  |  & M & \mbox{(magic)} \\
@@ -237,7 +241,7 @@ used in different contexts.
 \newcommand{\ANNPOS}[2]{\mathit{pos}(#1)_{#2}}
 
 \begin{table}
-\caption{\label{tab:addparens} Where are parentheses added? Look here.\strut}
+\caption{\label{tab:addparens} Can't read the AST and need parentheses? Here you go!.\strut}
 \hrule
 \[
 \begin{array}{rcll}
@@ -293,45 +297,47 @@ used in different contexts.
 \newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
 
 \begin{table}
+\caption{\label{tab:synl2} Concrete syntax of level 2 patterns.\strut}
+\hrule
 \[
 \begin{array}{@{}rcll@{}}
-  \NT{term} & ::= & & \mbox{(\bf terms)} \\
-    &     & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
-    &  |  & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
-    &  |  & \NT{binder}~\{\NT{ptnames}\}^{+}~\verb+.+~\NT{term} \\
-    &  |  & \NT{term}~\NT{term} & \mbox{(application)} \\
-    &  |  & x & \mbox{(identifier)} \\
-    &  |  & \mathrm{URI} & \mbox{(URI)} \\
+  \NT{term} & ::= & & \mbox{\bf terms} \\
+    &     & x & \mbox{(identifier)} \\
     &  |  & n & \mbox{(number)} \\
+    &  |  & \mathrm{URI} & \mbox{(URI)} \\
     &  |  & \verb+?+ & \mbox{(implicit)} \\
     &  |  & \verb+%+ & \mbox{(placeholder)} \\
     &  |  & \verb+?+n~[\verb+[+~\{\NT{subst}\}~\verb+]+] & \mbox{(meta)} \\
+    &  |  & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
+    &  |  & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
+    &  |  & \NT{binder}~\{\NT{ptnames}\}^{+}~\verb+.+~\NT{term} \\
+    &  |  & \NT{term}~\NT{term} & \mbox{(application)} \\
     &  |  & \verb+Prop+ \mid \verb+Set+ \mid \verb+Type+ \mid \verb+CProp+ & \mbox{(sort)} \\
     &  |  & [\verb+[+~\NT{term}~\verb+]+]~\verb+match+~\NT{term}~\verb+with [+~[\NT{rule}~\{\verb+|+~\NT{rule}\}]~\verb+]+ & \mbox{(pattern match)} \\
     &  |  & \verb+(+~\NT{term}~\verb+:+~\NT{term}~\verb+)+ & \mbox{(cast)} \\
     &  |  & \verb+(+~\NT{term}~\verb+)+ \\
-    &  |  & \BLOB & \mbox{(blob)} \\
-  \NT{defs}  & ::= & & \mbox{(\bf mutual definitions)} \\
+    &  |  & \BLOB(\NT{meta},\dots,\NT{meta}) & \mbox{(meta blob)} \\
+  \NT{defs}  & ::= & & \mbox{\bf mutual definitions} \\
     &     & \NT{fun}~\{\verb+and+~\NT{fun}\} \\
-  \NT{fun} & ::= & & \mbox{(\bf function)} \\
+  \NT{fun} & ::= & & \mbox{\bf functions} \\
     &     & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\
-  \NT{binder} & ::= & & \mbox{(\bf binders)} \\
+  \NT{binder} & ::= & & \mbox{\bf binders} \\
     &     & \verb+\Pi+ \mid \verb+\exists+ \mid \verb+\forall+ \mid \verb+\lambda+ \\
-  \NT{arg} & ::= & & \mbox{(\bf single argument)} \\
-    &     & \verb+_+ \mid x \mid \BLOB \\
-  \NT{ptname} & ::= & & \mbox{(\bf possibly typed name)} \\
+  \NT{arg} & ::= & & \mbox{\bf single argument} \\
+    &     & \verb+_+ \mid x \mid \BLOB(\NT{meta},\dots,\NT{meta}) \\
+  \NT{ptname} & ::= & & \mbox{\bf possibly typed name} \\
     &     & \NT{arg} \\
     &  |  & \verb+(+~\NT{arg}~\verb+:+~\NT{term}~\verb+)+ \\
-  \NT{ptnames} & ::= & & \mbox{(\bf bound variables)} \\
+  \NT{ptnames} & ::= & & \mbox{\bf bound variables} \\
     &     & \NT{arg} \\
     &  |  & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\
-  \NT{kind} & ::= & & \mbox{(\bf induction kind)} \\
+  \NT{kind} & ::= & & \mbox{\bf induction kind} \\
     &     & \verb+rec+ \mid \verb+corec+ \\
-  \NT{rule} & ::= & & \mbox{(\bf rules)} \\
+  \NT{rule} & ::= & & \mbox{\bf rules} \\
     &     & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term} \\[10ex]
 
-  \NT{meta} & ::= & & \mbox{(\bf meta)} \\
-    &     & \BLOB \\
+  \NT{meta} & ::= & & \mbox{\bf meta} \\
+    &     & \BLOB(\NT{term},\dots,\NT{term}) & \mbox{(term blob)} \\
     &  |  & [\verb+term+]~x \\
     &  |  & \verb+number+~x \\
     &  |  & \verb+ident+~x \\
@@ -343,6 +349,303 @@ used in different contexts.
     &  |  & \verb+fail+ 
 \end{array}
 \]
+\hrule
+\end{table}
+
+\begin{table}
+\caption{\label{tab:wfl2} Well-formedness rules for level 2 patterns.\strut}
+\hrule
+\[
+\renewcommand{\arraystretch}{3.5}
+\begin{array}{@{}c@{}}
+  \inference[\sc Constr]
+    {P_i :: D_i}
+    {\BLOB[P_1,\dots,P_n] :: D_i \oplus \cdots \oplus D_j} \\
+  \inference[\sc TermVar]
+    {}
+    {\mathtt{term}~x :: x : \mathtt{Term}}
+  \quad
+  \inference[\sc NumVar]
+    {}
+    {\mathtt{number}~x :: x : \mathtt{Number}}
+  \\
+  \inference[\sc IdentVar]
+    {}
+    {\mathtt{ident}~x :: x : \mathtt{String}}
+  \quad
+  \inference[\sc FreshVar]
+    {}
+    {\mathtt{fresh}~x :: x : \mathtt{String}}
+  \\
+  \inference[\sc Success]
+    {}
+    {\mathtt{anonymous} :: \emptyset}
+  \\
+  \inference[\sc Fold]
+    {P_1 :: D_1 & P_2 :: D_2 \oplus (x : \mathtt{Term}) & \DOMAIN(D_2)\ne\emptyset & \DOMAIN(D_1)\cap\DOMAIN(D_2)=\emptyset}
+    {\mathtt{fold}~P_1~\mathtt{rec}~x~P_2 :: D_1 \oplus D_2~\mathtt{List}}
+  \\
+  \inference[\sc Default]
+    {P_1 :: D \oplus D_1 & P_2 :: D & \DOMAIN(D_1) \ne \emptyset & \DOMAIN(D) \cap \DOMAIN(D_1) = \emptyset}
+    {\mathtt{default}~P_1~P_2 :: D \oplus D_1~\mathtt{Option}}
+  \\
+  \inference[\sc If]
+    {P_1 :: \emptyset & P_2 :: D & P_3 :: D }
+    {\mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 :: D}
+  \qquad
+  \inference[\sc Fail]
+    {}
+    {\mathtt{fail} :: \emptyset}
+%%     &  |  & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\
+%%     &  |  & \verb+fail+ 
+\end{array}
+\]
+\hrule
+\end{table}
+
+\begin{table}
+\caption{...}
+\hrule
+\[
+\begin{array}{rcll}
+\IOT{C[t_1,\dots,t_n]}{E} & = & C[\IOT{t_1}{E},\dots,\IOT{t_n}{E}] \\
+\IOT{\mathtt{term}~x}{E} & = & t & \mathcal{E}(x) = \mathtt{Term}~t \\
+\IOT{\mathtt{number}~x}{E} & = & n & \mathcal{E}(x) = \mathtt{Number}~n \\
+\IOT{\mathtt{ident}~x}{E} & = & y & \mathcal{E}(x) = \mathtt{String}~y \\
+\IOT{\mathtt{fresh}~x}{E} & = & y & \mathcal{E}(x) = \mathtt{String}~y \\
+\IOT{\mathtt{default}~P_1~P_2}{E} & = & \IOT{P_2}{E'} & \mathcal{E}(\NAMES(P_1)\setminus\NAMES(P_2)))=\{\mathtt{None}\} \\
+& & & \mathcal{E}'(x) =
+ \left\{
+ \begin{array}{@{}ll}
+ \bot & x \in \NAMES(P_1)\setminus\NAMES(P_2) \\
+ \mathcal{E}(x) & \mbox{otherwise} \\
+ \end{array}
+ \right. \\
+\IOT{\mathtt{default}~P_1~P_2}{E} & = & \IOT{P_2}{E'} & \mathcal{E}(\NAMES(P_1)\setminus\NAMES(P_2)))=\{\mathtt{Some}~v_1,\dots,\mathtt{Some}~v_n\} \\
+& & & \mathcal{E}'(x) =
+ \left\{
+ \begin{array}{@{}ll}
+ v & x \in \NAMES(P_1)\setminus\NAMES(P_2) \wedge \mathcal{E}(x) = \mathtt{Some}~v\\
+ \mathcal{E}(x) & \mbox{otherwise}
+ \end{array}
+ \right. \\
+\IOT{\mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2}{E}
+& =
+& \IOT{P_2}{E'}
+& \mathcal{E}(\NAMES(P_2)\setminus\{x\}) = \{[]\} \\
+& & & \mathcal{E}'(y) =
+ \left\{
+ \begin{array}{@{}ll}
+ \bot & y \in \NAMES(P_2)\setminus\{x\} \\
+ \mathcal{E}(y) & \mbox{otherwise} \\
+ \end{array}
+ \right. \\
+\IOT{\mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2}{E}
+& =
+& \IOT{P_2}{E'}
+& \mathcal{E}(\NAMES(P_2)\setminus\{x\}) = \{[v_{11},\dots,v_{1n}],\dots,[v_{m1},\dots,v_{mn}]\} \\
+& & & \mathcal{E}'(y) =
+ \left\{
+ \begin{array}{@{}ll}
+ \IOT{\mathtt{fold}~d~P_1~\mathtt{rec}~x~P_e}{E''} & y = x \\
+ v_1 & y\in\NAMES(P_2)\setminus\{x\} \wedge \mathcal{E}(y)=[v_1;\dots;v_n] \\
+ \mathcal{E}(y) & \mbox{otherwise} \\
+ \end{array}
+ \right. \\
+& & & \mathcal{E}''(y) =
+ \left\{
+ \begin{array}{@{}ll}
+ [v_2;\dots;v_n] & y\in\NAMES(P_2)\setminus\{x\} \wedge \mathcal{E}(y)=[v_1;\dots;v_n] \\
+ \mathcal{E}(y) & \mbox{otherwise} \\
+ \end{array}
+ \right. \\
+\end{array} \\
+\]
+\end{table}
+
+\begin{table}
+\caption{\label{tab:l2match} Pattern matching of level 2 terms.\strut}
+\hrule
+\[
+\renewcommand{\arraystretch}{3.5}
+\begin{array}{@{}c@{}}
+  \inference[\sc Constr]
+    {t_i \in P_i ~> \mathcal E_i & i\ne j => \DOMAIN(\mathcal E_i)\cap\DOMAIN(\mathcal E_j)=\emptyset}
+    {C[t_1,\dots,t_n] \in C[P_1,\dots,P_n] ~> \mathcal E_1 \oplus \cdots \oplus \mathcal E_n}
+  \\
+  \inference[\sc TermVar]
+    {}
+    {t \in [\mathtt{term}]~x ~> [x |-> \mathtt{Term}~t]}
+  \quad
+  \inference[\sc NumVar]
+    {}
+    {n \in \mathtt{number}~x ~> [x |-> \mathtt{Number}~n]}
+  \\
+  \inference[\sc IdentVar]
+    {}
+    {x \in \mathtt{ident}~x ~> [x |-> \mathtt{String}~x]}
+  \quad
+  \inference[\sc FreshVar]
+    {}
+    {x \in \mathtt{fresh}~x ~> [x |-> \mathtt{String}~x]}
+  \\
+  \inference[\sc Success]
+    {}
+    {t \in \mathtt{anonymous} ~> \emptyset}
+  \\
+  \inference[\sc DefaultT]
+    {t \in P_1 ~> \mathcal E}
+    {t \in \mathtt{default}~P_1~P_2 ~> \mathcal E'}
+    \quad
+    \mathcal E'(x) = \left\{
+    \renewcommand{\arraystretch}{1}
+    \begin{array}{ll}
+      \mathtt{Some}~\mathcal{E}(x) & x \in \NAMES(P_1) \setminus \NAMES(P_2) \\
+      \mathcal{E}(x) & \mbox{otherwise}
+    \end{array}
+    \right.
+  \\
+  \inference[\sc DefaultF]
+    {t \not\in P_1 & t \in P_2 ~> \mathcal E}
+    {t \in \mathtt{default}~P_1~P_2 ~> \mathcal E'}
+    \quad
+    \mathcal E'(x) = \left\{
+    \renewcommand{\arraystretch}{1}
+    \begin{array}{ll}
+      \mathtt{None} & x \in \NAMES(P_1) \setminus \NAMES(P_2) \\
+      \mathcal{E}(x) & \mbox{otherwise}
+    \end{array}
+    \right.
+  \\
+  \inference[\sc IfT]
+    {t \in P_1 ~> \mathcal E' & t \in P_2 ~> \mathcal E}
+    {t \in \mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 ~> \mathcal E}
+  \quad
+  \inference[\sc IfF]
+    {t \not\in P_1 & t \in P_3 ~> \mathcal E}
+    {t \in \mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 ~> \mathcal E}
+  \\
+  \inference[\sc FoldRec]
+    {t \in P_2 ~> \mathcal E & \mathcal{E}(x) \in \mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'}
+    {t \in \mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E''}
+  \\
+  \mbox{where}~\mathcal{E}''(y) = \left\{
+    \renewcommand{\arraystretch}{1}
+    \begin{array}{ll}
+      \mathcal{E}(y)::\mathcal{E}'(y) & y \in \NAMES(P_2) \setminus \{x\} \wedge d = \mathtt{right} \\
+      \mathcal{E}'(y)@[\mathcal{E}(y)] & y \in \NAMES(P_2) \setminus \{x\} \wedge d = \mathtt{left} \\
+      \mathcal{E}'(y) & \mbox{otherwise}
+    \end{array}  
+  \right.
+  \\
+  \inference[\sc FoldBase]
+    {t \not\in P_2 & t \in P_1 ~> \mathcal E}
+    {t \in \mathtt{fold}~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'}
+  \quad
+  \mathcal E'(y) = \left\{
+    \renewcommand{\arraystretch}{1}
+    \begin{array}{ll}
+      [] & y \in \NAMES(P_2) \setminus \{x\} \\
+      \mathcal{E}(y) & \mbox{otherwise}
+    \end{array}  
+  \right.
+\end{array}
+\]
+\hrule
 \end{table}
 
-\end{document}
\ No newline at end of file
+\section{Type checking}
+
+\newcommand{\GUARDED}{\mathit{guarded}}
+\newcommand{\TRUE}{\mathit{true}}
+\newcommand{\FALSE}{\mathit{false}}
+
+\newcommand{\TN}{\mathit{tn}}
+
+\begin{table}
+\caption{\label{tab:guarded} Guarded condition of level 2
+pattern. Note that the recursive case of the \texttt{fold} magic is
+not explicitly required to be guarded. The point is that it must
+contain at least two distinct names, and this guarantees that whatever
+is matched by the recursive pattern, the terms matched by those two
+names will be smaller than the whole matched term.\strut} \hrule
+\[
+\begin{array}{rcll}
+  \GUARDED(C(M(P))) & = & \GUARDED(P) \\
+  \GUARDED(C(t_1,\dots,t_n)) & = & \TRUE \\
+  \GUARDED(\mathtt{term}~x) & = & \FALSE \\
+  \GUARDED(\mathtt{number}~x) & = & \FALSE \\
+  \GUARDED(\mathtt{ident}~x) & = & \FALSE \\
+  \GUARDED(\mathtt{fresh}~x) & = & \FALSE \\
+  \GUARDED(\mathtt{anonymous}) & = & \TRUE \\
+  \GUARDED(\mathtt{default}~P_1~P_2) & = & \GUARDED(P_1) \wedge \GUARDED(P_2) \\
+  \GUARDED(\mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3) & = & \GUARDED(P_2) \wedge \GUARDED(P_3) \\
+  \GUARDED(\mathtt{fail}) & = & \TRUE \\
+  \GUARDED(\mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2) & = & \GUARDED(P_2)
+\end{array}
+\]
+\hrule
+\end{table}
+
+%% Assume that we have two corresponding patterns $P_1$ (level 1) and
+%% $P_2$ (level 2) and that we have to check whether they are
+%% ``correct''. First we define the notion of \emph{top-level names} of
+%% $P_1$ and $P_2$, as follows:
+%% \[
+%% \begin{array}{rcl}
+%%   \TN(C_1[P'_1,\dots,P'_2]) & = & \TN(P'_1) \cup \cdots \cup \TN(P'_2) \\
+%%   \TN(\TVAR{x}) & = & \{x\} \\
+%%   \TN(\NVAR{x}) & = & \{x\} \\
+%%   \TN(\IVAR{x}) & = & \{x\} \\
+%%   \TN(\mathtt{list0}~P'~l?) & = & \emptyset \\
+%%   \TN(\mathtt{list1}~P'~l?) & = & \emptyset \\
+%%   \TN(\mathtt{opt}~P') & = & \emptyset \\[3ex]
+%%   \TN(\BLOB(P''_1,\dots,P''_2)) & = & \TN(P''_1) \cup \cdots \cup \TN(P''_2) \\
+%%   \TN(\mathtt{term}~x) & = & \{x\} \\
+%%   \TN(\mathtt{number}~x) & = & \{x\} \\
+%%   \TN(\mathtt{ident}~x) & = & \{x\} \\
+%%   \TN(\mathtt{fresh}~x) & = & \{x\} \\
+%%   \TN(\mathtt{anonymous}) & = & \emptyset \\
+%%   \TN(\mathtt{fold}~P''_1~\mathtt{rec}~x~P''_2) & = & \TN(P''_1) \\
+%%   \TN(\mathtt{default}~P''_1~P''_2) & = & \TN(P''_1) \cap \TN(P''_2) \\
+%%   \TN(\mathtt{if}~P''_1~\mathtt{then}~P''_2~\mathtt{else}~P''_3) & = & \TN(P''_2) \\
+%%   \TN(\mathtt{fail}) & = & \emptyset
+%% \end{array}
+%% \]
+
+We say that a \emph{bidirectional transformation}
+\[
+  P_1 <=> P_2
+\]
+is well-formed if:
+\begin{itemize}
+  \item the pattern $P_2$ is guarded, that is $\GUARDED(P_2)=\TRUE$;
+  \item the two patterns are well-formed in the same context $D$, that
+    is $P_1 :: D$ and $P_2 :: D$;
+  \item for any direct sub-pattern $\mathtt{opt}~P'_1$ of $P_1$ such
+    that $\mathtt{opt}~P'_1 :: X$ there is a sub-pattern
+    $\mathtt{default}~P'_2~P''_2$ of $P_2$ such that
+    $\mathtt{default}~P'_2~P''_2 :: X \oplus Y$ for some context $Y$;
+  \item for any direct sub-pattern $\mathtt{list}~P'_1~l?$ of $P_1$
+    such that $\mathtt{list}~P'_1~l? :: X$ there is a sub-pattern
+    $\mathtt{fold}~P'_2~\mathtt{rec}~x~P''_2$ of $P_2$ such that
+    $\mathtt{fold}~P'_2~\mathtt{rec}~x~P''_2 :: X \oplus Y$ for some
+    context $Y$.
+\end{itemize}
+
+A \emph{left-to-right transformation}
+\[
+  P_1 => P_2
+\]
+is well-formed if $P_2$ does not contain \texttt{if}, \texttt{fail},
+or \texttt{anonymous} meta patterns.
+
+Note that the transformations are in a sense asymmetric. Moving from
+the concrete syntax (level 1) to the abstract syntax (level 2) we
+forget about syntactic details. Moving from the abstract syntax to the
+concrete syntax we may want to forget about redundant structure
+(types).
+
+Relationship with grammatical frameworks?
+
+\end{document}