-\documentclass[a4paper]{article}
+\documentclass[a4paper,draft]{article}
\usepackage{manfnt}
\usepackage{a4wide}
\newcommand{\BREAK}{\mathtt{break}}
\newcommand{\TVAR}[1]{#1:\mathtt{term}}
+\newcommand{\IMPVAR}{\TVAR{\_}}
\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|]_{#2}^2}
+\newcommand{\IAP}[2]{|[#1|]_{#2}^a}
+\newcommand{\IAPP}[3]{|[#1|]_{#2,#3}^a}
\newcommand{\ADDPARENS}[2]{\llparenthesis#1\rrparenthesis^{#2}}
\newcommand{\NAMES}{\mathit{names}}
\newcommand{\DOMAIN}{\mathit{domain}}
+\newcommand{\UPDATE}[2]{#1[#2]}
\mathlig{~>}{\leadsto}
\mathlig{|->}{\mapsto}
\end{table}
\[
-\IOT{\cdot}{{}} : P -> \mathit{Env} -> T
+\ITO{\cdot}{{}} : P -> \mathit{Env} -> T
\]
\begin{table}
-\caption{\label{tab:il1} Instantiation of level 1 patterns.\strut}
+\caption{\label{tab:il1f2} Instantiation of level 1 patterns from level 2.\strut}
\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\{
\mathcal{E}(x), & \mbox{otherwise}
\end{array}
\right. \\
- \IOT{l}{E} & = & l \\
+ \ITO{l}{E} & = & l \\
%% & | & (P) & \mbox{(fenced)} \\
%% & | & M & \mbox{(magic)} \\
\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}
\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} \\
& & x & \mbox{(identifier)} \\
& | & n & \mbox{(number)} \\
+ & | & s & \mbox{(symbol)} \\
& | & \mathrm{URI} & \mbox{(URI)} \\
& | & \verb+?+ & \mbox{(implicit)} \\
& | & \verb+%+ & \mbox{(placeholder)} \\
& & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term} \\[10ex]
\NT{meta} & ::= & & \mbox{\bf meta} \\
- & & \BLOB(\NT{term},\dots,\NT{term}) & (term blob) \\
+ & & \BLOB(\NT{term},\dots,\NT{term}) & \mbox{(term blob)} \\
& | & [\verb+term+]~x \\
& | & \verb+number+~x \\
& | & \verb+ident+~x \\
& | & \verb+fail+
\end{array}
\]
+\hrule
\end{table}
\begin{table}
\renewcommand{\arraystretch}{3.5}
\begin{array}{@{}c@{}}
\inference[\sc Constr]
- {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
+ {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}}
+ {\mathtt{term}~x :: x : \mathtt{Term}}
\quad
\inference[\sc NumVar]
{}
\qquad
\inference[\sc Fail]
{}
- {\mathtt{fail} : \emptyset}
+ {\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{\label{tab:il2f1} Instantiation of level 2 patterns from level 1.
+ \strut}
+\hrule
+\[
+\begin{array}{rcll}
+
+\IOT{C[t_1,\dots,t_n]}{\mathcal{E}} & =
+& C[\IOT{t_1}{\mathcal{E}},\dots,\IOT{t_n}{\mathcal{E}}] \\
+
+\IOT{\mathtt{term}~x}{\mathcal{E}} & = & t & \mathcal{E}(x) = \mathtt{Term}~t \\
+
+\IOT{\mathtt{number}~x}{\mathcal{E}} & =
+& n & \mathcal{E}(x) = \mathtt{Number}~n \\
+
+\IOT{\mathtt{ident}~x}{\mathcal{E}} & =
+& y & \mathcal{E}(x) = \mathtt{String}~y \\
+
+\IOT{\mathtt{fresh}~x}{\mathcal{E}} & = & y & \mathcal{E}(x) = \mathtt{String}~y \\
+
+\IOT{\mathtt{default}~P_1~P_2}{\mathcal{E}} & =
+& \IOT{P_1}{\UPDATE{\mathcal{E}}{x_i|->v_i}}
+& \mathcal{E}(x_i)=\mathtt{Some}~v_i \\
+& & & \NAMES(P_1)\setminus\NAMES(P_2)=\{x_1,\dots,x_n\} \\
+
+\IOT{\mathtt{default}~P_1~P_2}{\mathcal{E}} & =
+& \IOT{P_2}{\UPDATE{\mathcal{E}}{x_i|->\bot}}
+& \mathcal{E}(x_i)=\mathtt{None} \\
+& & & \NAMES(P_1)\setminus\NAMES(P_2)=\{x_1,\dots,x_n\} \\
+
+\IOT{\mathtt{fold}~\mathtt{right}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}}
+& =
+& \IOT{P_1}{\mathcal{E}'}
+& \mathcal{E}(\NAMES(P_2)\setminus\{x\}) = \{[],\dots,[]\} \\
+& & \multicolumn{2}{l}{\mathcal{E}'=\UPDATE{\mathcal{E}}{\NAMES(P_2)\setminus\{x\}|->\bot}}
+\\
+
+\IOT{\mathtt{fold}~\mathtt{right}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}}
+& =
+& \IOT{P_2}{\mathcal{E}'}
+& \mathcal{E}(y_i) = [v_{i1},\dots,v_{in}] \\
+& & & \NAMES(P_2)\setminus\{x\}=\{y_1,\dots,y_m\} \\
+& & \multicolumn{2}{l}{\mathcal{E}'(y) =
+ \left\{
+ \begin{array}{@{}ll}
+ \IOT{\mathtt{fold}~\mathtt{right}~P_1~\mathtt{rec}~x~P_e}{\mathcal{E}''}
+ & y=x \\
+ v_{i1} & y=y_i \\
+ \mathcal{E}(y) & \mbox{otherwise} \\
+ \end{array}
+ \right.} \\
+& & \multicolumn{2}{l}{\mathcal{E}''(y) =
+ \left\{
+ \begin{array}{@{}ll}
+ [v_{i2};\dots;v_{in}] & y=y_i \\
+ \mathcal{E}(y) & \mbox{otherwise} \\
+ \end{array}
+ \right.} \\
+
+\IOT{\mathtt{fold}~\mathtt{left}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}}
+& =
+& \mathit{eval\_fold}(x,P_2,\mathcal{E}')
+& \\
+& & \multicolumn{2}{l}{\mathcal{E}' = \UPDATE{\mathcal{E}}{x|->
+\IOT{P_1}{\UPDATE{\mathcal{E}}{\NAMES(P_2)|->\bot}}}} \\
+
+\mathit{eval\_fold}(x,P,\mathcal{E})
+& =
+& \mathcal{E}(x)
+& \mathcal{E}(\NAMES(P)\setminus\{x\})=\{[],\dots,[]\} \\
+
+\mathit{eval\_fold}(x,P,\mathcal{E})
+& =
+& \mathit{eval\_fold}(x,P,\mathcal{E}')
+& \mathcal{E}(y_i) = [v_{i1},\dots,v_{in}] \\
+& & & \NAMES(P)\setminus{x}=\{y_1,\dots,y_m\} \\
+&
+& \multicolumn{2}{l}{\mathcal{E}' = \UPDATE{\mathcal{E}}{x|->\IOT{P}{\mathcal{E}''}; ~ y_i |-> [v_{i2};\dots;v_{in_i}]}}
+\\
+&
+& \multicolumn{2}{l}{\mathcal{E}''(y) =
+\left\{
+\begin{array}{ll}
+ v_1 & y\in \NAMES(P)\setminus\{x\} \\
+ \mathcal{E}(x) & y=x \\
+ \bot & \mathit{otherwise} \\
+\end{array}
+\right.
+}
+\\
+
+\end{array} \\
+\]
+\end{table}
+
\begin{table}
\caption{\label{tab:l2match} Pattern matching of level 2 terms.\strut}
\hrule
{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 FoldR]
- {t \in P_2 ~> \mathcal E & \mathcal{E}(x) \in \mathtt{fold}~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'}
- {t \in \mathtt{fold}~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E''}
- \quad
- \mathcal E''(y) = \left\{
+ \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\} \\
+ \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 FoldB]
+ \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
\hrule
\end{table}
-\end{document}
\ No newline at end of file
+\begin{table}
+ \caption{\label{tab:synl3} Abstract syntax of level 3 terms and patterns.}
+ \hrule
+ \[
+ \begin{array}{@{}ll@{}}
+ \begin{array}[t]{rcll}
+ T & : := & & \mbox{(\bf terms)} \\
+ & & u & \mbox{(uri)} \\
+ & | & \lambda x.T & \mbox{($\lambda$-abstraction)} \\
+ & | & (T_1 \dots T_n) & \mbox{(application)} \\
+ & | & \dots \\[2ex]
+ \end{array} &
+ \begin{array}[t]{rcll}
+ P & : := & & \mbox{(\bf patterns)} \\
+ & & u & \mbox{(uri)} \\
+ & | & V & \mbox{(variable)} \\
+ & | & (P_1 \dots P_n) & \mbox{(application)} \\[2ex]
+ V & : := & & \mbox{(\bf variables)} \\
+ & & \TVAR{x} & \mbox{(term variable)} \\
+ & | & \IMPVAR & \mbox{(implicit variable)} \\
+ \end{array} \\
+ \end{array}
+ \]
+ \hrule
+\end{table}
+
+\begin{table}
+\caption{\label{tab:wfl3} Well-formedness rules for level 3 patterns.\strut}
+\hrule
+\[
+\renewcommand{\arraystretch}{3.5}
+\begin{array}{@{}c@{}}
+ \inference[\sc Uri] {} {u :: \emptyset} \quad
+ \inference[\sc ImpVar] {} {\TVAR{x} :: \emptyset} \quad
+ \inference[\sc TermVar] {} {\TVAR{x} :: x:\mathtt{Term}} \\
+ \inference[\sc Appl]
+ {P_i :: D_i
+ \quad \forall i,j,i\neq j=>\DOMAIN(D_i)\cap\DOMAIN(D_j)=\emptyset}
+ {P_1\cdots P_n :: D_1\oplus\cdots\oplus D_n} \\
+\end{array}
+\]
+\hrule
+\end{table}
+
+\begin{table}
+ \caption{\label{tab:synargp} Abstract syntax of applicative symbol patterns.}
+ \hrule
+ \[
+ \begin{array}{rcll}
+ P & : := & & \mbox{(\bf patterns)} \\
+ & & s ~ \{ \mathit{arg} \} & \mbox{(symbol pattern)} \\[2ex]
+ \mathit{arg} & : := & & \mbox{(\bf argument)} \\
+ & & \TVAR{x} & \mbox{(term variable)} \\
+ & | & \eta.\mathit{arg} & \mbox{($\eta$-abstraction)} \\
+ \end{array}
+ \]
+ \hrule
+\end{table}
+
+\begin{table}
+\caption{\label{tab:wfargp} Well-formedness rules for applicative symbol
+patterns.\strut}
+\hrule
+\[
+\renewcommand{\arraystretch}{3.5}
+\begin{array}{@{}c@{}}
+ \inference[\sc Pattern]
+ {\mathit{arg}_i :: D_i
+ \quad \forall i,j,i\neq j=>\DOMAIN(D_i)\cap\DOMAIN(D_j)=\emptyset}
+ {s~\mathit{arg}_1\cdots\mathit{arg}_n :: D_1\oplus\cdots\oplus D_n} \\
+ \inference[\sc TermVar]
+ {}
+ {\TVAR{x} :: x : \mathtt{Term}}
+ \quad
+ \inference[\sc EtaAbs]
+ {\mathit{arg} :: D}
+ {\eta.\mathit{arg} :: D}
+ \\
+\end{array}
+\]
+\hrule
+\end{table}
+
+\begin{table}
+\caption{\label{tab:l3match} Pattern matching of level 3 terms.\strut}
+\hrule
+\[
+\renewcommand{\arraystretch}{3.5}
+\begin{array}{@{}c@{}}
+ \inference[\sc Uri] {} {u\in u ~> []} \quad
+ \inference[\sc Appl] {t_i\in P_i ~> \mathcal{E}_i}
+ {(t_1\dots t_n)\in(P_1\dots P_n) ~>
+ \mathcal{E}_1\oplus\cdots\oplus\mathcal{E}_n} \\
+ \inference[\sc TermVar] {} {t\in \TVAR{x} ~> [x |-> \mathtt{Term}~t]} \quad
+ \inference[\sc ImpVar] {} {t\in \IMPVAR ~> []} \\
+\end{array}
+\]
+\hrule
+\end{table}
+
+\begin{table}
+\caption{\label{tab:iapf3} Instantiation of applicative symbol patterns (from
+level 3).\strut}
+\hrule
+\[
+\begin{array}{rcll}
+ \IAP{s~a_1\cdots a_n}{\mathcal{E}} & = &
+ (s~\IAPP{a_1}{\mathcal{E}}{0}\cdots\IAPP{a_n}{\mathcal{E}}{0}) & \\
+ \IAPP{\TVAR{x}}{\mathcal{E}}{0} & = & t & \mathcal{E}(x)=\mathtt{Term}~t \\
+ \IAPP{\TVAR{x}}{\mathcal{E}}{i+1} & = & \lambda y.\IAPP{t}{\mathcal{E}}{i}
+ & \mathcal{E}(x)=\mathtt{Term}~\lambda y.t \\
+ \IAPP{\TVAR{x}}{\mathcal{E}}{i+1} & =
+ & \lambda y_1.\cdots.\lambda y_{i+1}.t~y_1\cdots y_{i+1}
+ & \mathcal{E}(x)=\mathtt{Term}~t\wedge\forall y,t\neq\lambda y.t \\
+ \IAPP{\eta.a}{\mathcal{E}}{i} & = & \IAPP{a}{\mathcal{E}}{i+1} \\
+\end{array}
+\]
+\hrule
+\end{table}
+
+\section{Type checking}
+
+\subsection{Level 1 $<->$ Level 2}
+
+\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_1)
+\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 $P_1$ is a well-formed \emph{level 1 pattern} in some context $D$ and
+ $P_2$ is a well-formed \emph{level 2 pattern} in the very same context $D$,
+ that is $P_1 :: D$ and $P_2 :: D$;
+ \item the pattern $P_2$ is guarded, that is $\GUARDED(P_2)=\TRUE$;
+ \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?
+
+\subsection{Level 2 $<->$ Level 3}
+
+We say that an \emph{interpretation}
+\[
+ P_2 <=> P_3
+\]
+is well-formed if:
+\begin{itemize}
+ \item $P_2$ is a well-formed \emph{applicative symbol pattern} in some context
+ $D$ and $P_3$ is a well-formed \emph{level 3 pattern} in the very same
+ context $D$, that is $P_2 :: D$ and $P_3 :: D$.
+\end{itemize}
+
+\end{document}
+
projects / helm.git / blobdiff