diff -r 2ccf3086142b -r b5cb3183409e Paper/Paper.thy --- a/Paper/Paper.thy Tue Oct 05 21:48:31 2010 +0100 +++ b/Paper/Paper.thy Wed Oct 06 08:09:40 2010 +0100 @@ -448,12 +448,12 @@ the identity everywhere except on a finite number of atoms. There is a two-place permutation operation written @{text "_ \ _ :: perm \ \ \ \"} - in which the generic type @{text "\"} stands for the type of the object + where the generic type @{text "\"} stands for the type of the object over which the permutation acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"}, the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, and the inverse permutation of @{term p} as @{text "- p"}. The permutation - operation is defined by induction over the type-hierarchy \cite{HuffmanUrban10}; + operation is defined over the type-hierarchy \cite{HuffmanUrban10}; for example permutations acting on products, lists, sets, functions and booleans is given by: % @@ -611,7 +611,7 @@ @{text as} in @{text x}, because @{term "p \ x = x"}. Most properties given in this section are described in detail in \cite{HuffmanUrban10} - and of course all are formalised in Isabelle/HOL. In the next sections we will make + and all are formalised in Isabelle/HOL. In the next sections we will make extensive use of these properties in order to define $\alpha$-equivalence in the presence of multiple binders. *} @@ -737,13 +737,13 @@ \noindent (similarly for $\approx_{\,\textit{abs\_res}}$ and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence - relations and equivariant. + relations. %% and equivariant. \begin{lemma}\label{alphaeq} The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$ - and $\approx_{\,\textit{abs\_res}}$ are equivalence relations, and if @{term - "abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \ as, p \ x) (p \ - bs, p \ y)"} (similarly for the other two relations). + and $\approx_{\,\textit{abs\_res}}$ are equivalence relations. %, and if + %@{term "abs_set (as, x) (bs, y)"} then also + %@{term "abs_set (p \ as, p \ x) (p \ bs, p \ y)"} (similarly for the other two relations). \end{lemma} \begin{proof} @@ -929,15 +929,15 @@ annotated on the types are optional. Their purpose is to be used in the (possibly empty) list of \emph{binding clauses}, which indicate the binders and their scope in a term-constructor. They come in three \emph{modes}: - + % \begin{center} - \begin{tabular}{l} - \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\ - \isacommand{bind (set)}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\ - \isacommand{bind (res)}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\ + \begin{tabular}{@ {}l@ {}} + \isacommand{bind} {\it binders} \isacommand{in} {\it bodies}\;\;\;\; + \isacommand{bind (set)} {\it binders} \isacommand{in} {\it bodies}\;\;\;\; + \isacommand{bind (res)} {\it binders} \isacommand{in} {\it bodies} \end{tabular} \end{center} - + % \noindent The first mode is for binding lists of atoms (the order of binders matters); the second is for sets of binders (the order does not matter, but the @@ -1027,17 +1027,17 @@ \begin{equation}\label{letpat} \mbox{\small% \begin{tabular}{l} - \isacommand{nominal\_datatype} @{text trm} =\\ + \isacommand{nominal\_datatype} @{text trm} $=$\\ \hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\ \hspace{5mm}$\mid$~@{term "App trm trm"}\\ \hspace{5mm}$\mid$~@{text "Lam x::name t::trm"} \;\;\isacommand{bind} @{text x} \isacommand{in} @{text t}\\ \hspace{5mm}$\mid$~@{text "Let p::pat trm t::trm"} \;\;\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\ - \isacommand{and} @{text pat} =\\ - \hspace{5mm}\phantom{$\mid$}~@{text PNil}\\ - \hspace{5mm}$\mid$~@{text "PVar name"}\\ - \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\ + \isacommand{and} @{text pat} $=$ + @{text PNil} + $\mid$~@{text "PVar name"} + $\mid$~@{text "PTup pat pat"}\\ \isacommand{binder}~@{text "bn::pat \ atom list"}\\ \isacommand{where}~@{text "bn(PNil) = []"}\\ \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\ @@ -1070,14 +1070,14 @@ \begin{equation}\label{letrecs} \mbox{\small% \begin{tabular}{@ {}l@ {}} - \isacommand{nominal\_datatype}~@{text "trm ="}\ldots\\ + \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\ \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\ \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"} \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\ - \isacommand{and} @{text "ass"} =\\ - \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\ - \hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\ + \isacommand{and} @{text "assn"} $=$ + @{text "ANil"} + $\mid$~@{text "ACons name trm assn"}\\ \isacommand{binder} @{text "bn::assn \ atom list"}\\ \isacommand{where}~@{text "bn(ANil) = []"}\\ \hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\ @@ -1197,21 +1197,21 @@ free-atom functions from the specification. For the \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions % - \begin{equation}\label{fvars} - @{text "fa_ty\<^isub>1, \, fa_ty\<^isub>n"} - \end{equation} - - \noindent + %\begin{equation}\label{fvars} + @{text "fa_ty\<^isub>"}$_{1..n}$ + %\end{equation} + % + %\noindent by recursion. We define these functions together with auxiliary free-atom functions for the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$ we define % - \begin{center} - @{text "fa_bn\<^isub>1, \, fa_bn\<^isub>m"} - \end{center} - - \noindent + %\begin{center} + @{text "fa_bn\<^isub>"}$_{1..m}$. + %\end{center} + % + %\noindent The reason for this setup is that in a deep binder not all atoms have to be bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function that calculates those free atoms in a deep binder. @@ -1254,8 +1254,9 @@ \noindent where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function - we are defining by recursion - (see \eqref{fvars}); otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}. + we are defining by recursion; + %(see \eqref{fvars}); + otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}. In order to formally define the set @{text B} we use the following auxiliary @{text "bn"}-functions for atom types to which shallow binders may refer @@ -1276,8 +1277,8 @@ \noindent Like the function @{text atom}, the function @{text "atoms"} coerces - a set of atoms to a set of the generic atom type. It is defined as - @{text "atoms as \ {atom a | a \ as}"}. + a set of atoms to a set of the generic atom type. + %It is defined as @{text "atoms as \ {atom a | a \ as}"}. The set @{text B} is then formally defined as % \begin{center} @@ -1341,7 +1342,7 @@ "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text "fa\<^bsub>bn\<^esub>"} as follows: % - \begin{center} + \begin{center}\small \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} @{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \ fa\<^bsub>bn\<^esub> as"}\\ @{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \ fa\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm] @@ -1388,7 +1389,7 @@ "ty"}$_{1..n}$ from the specification. We write them as % %\begin{center} - @{text "\ty\<^isub>1, \, \ty\<^isub>n"}. + @{text "\ty"}$_{1..n}$. %\end{center} % %\noindent @@ -1396,7 +1397,7 @@ define auxiliary $\alpha$-equivalence relations % %\begin{center} - @{text "\bn\<^isub>1, \, \bn\<^isub>m"} + @{text "\bn\<^isub>"}$_{1..m}$ %\end{center} % %\noindent @@ -1406,9 +1407,9 @@ % \begin{center} \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} - @{text "(x\<^isub>1,.., x\<^isub>n) (R\<^isub>1,.., R\<^isub>n) (x\\<^isub>1,.., x\\<^isub>n)"} & @{text "\"} & - @{text "x\<^isub>1 R\<^isub>1 x\\<^isub>1 \ .. \ x\<^isub>n R\<^isub>n x\\<^isub>n"}\\ - @{text "(fa\<^isub>1,.., fa\<^isub>n) (x\<^isub>1,.., x\<^isub>n)"} & @{text "\"} & @{text "fa\<^isub>1 x\<^isub>1 \ .. \ fa\<^isub>n x\<^isub>n"}\\ + @{text "(x\<^isub>1,\, x\<^isub>n) (R\<^isub>1,\, R\<^isub>n) (x\\<^isub>1,\, x\\<^isub>n)"} & @{text "\"} & + @{text "x\<^isub>1 R\<^isub>1 x\\<^isub>1 \ \ \ x\<^isub>n R\<^isub>n x\\<^isub>n"}\\ + @{text "(fa\<^isub>1,\, fa\<^isub>n) (x\<^isub>1,\, x\<^isub>n)"} & @{text "\"} & @{text "fa\<^isub>1 x\<^isub>1 \ \ \ fa\<^isub>n x\<^isub>n"}\\ \end{tabular} \end{center} @@ -1563,7 +1564,7 @@ we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and $\approx_{\textit{bn}}$ with the following clauses: - \begin{center} + \begin{center}\small \begin{tabular}{@ {}c @ {}} \infer{@{text "Let as t \\<^bsub>trm\<^esub> Let as' t'"}} {@{term "\p. (bn as, t) \lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \\<^bsub>bn\<^esub> as'"}}\smallskip\\ @@ -1572,7 +1573,7 @@ \end{tabular} \end{center} - \begin{center} + \begin{center}\small \begin{tabular}{@ {}c @ {}} \infer{@{text "ANil \\<^bsub>assn\<^esub> ANil"}}{}\hspace{9mm} \infer{@{text "ACons a t as \\<^bsub>assn\<^esub> ACons a' t' as"}} @@ -1580,7 +1581,7 @@ \end{tabular} \end{center} - \begin{center} + \begin{center}\small \begin{tabular}{@ {}c @ {}} \infer{@{text "ANil \\<^bsub>bn\<^esub> ANil"}}{}\hspace{9mm} \infer{@{text "ACons a t as \\<^bsub>bn\<^esub> ACons a' t' as"}} @@ -1615,7 +1616,7 @@ \begin{lemma}\label{equiv} Given the raw types @{text "ty"}$_{1..n}$ and binding functions @{text "bn"}$_{1..m}$, the relations @{text "\ty"}$_{1..n}$ and - @{text "\bn"}$_{1..m}$ are equivalence relations and equivariant. + @{text "\bn"}$_{1..m}$ are equivalence relations.%% and equivariant. \end{lemma} \begin{proof} @@ -1721,8 +1722,10 @@ operations defined in \eqref{ceqvt}. In order to make this lifting to go through, we have to show that the permutation operations are respectful. This amounts to showing that the - $\alpha$-equivalence relations are equivariant, which we already established - in Lemma~\ref{equiv}. As a result we can add the equations + $\alpha$-equivalence relations are equivariant \cite{HuffmanUrban10}. + %, which we already established + %in Lemma~\ref{equiv}. + As a result we can add the equations % \begin{equation}\label{calphaeqvt} @{text "p \ (C\<^sup>\ x\<^isub>1 \ x\<^isub>r) = C\<^sup>\ (p \ x\<^isub>1) \ (p \ x\<^isub>r)"} @@ -1736,9 +1739,10 @@ The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$ by the datatype package of Isabelle/HOL. - Finally we can add to our infrastructure a structural induction principle - for the types @{text "ty\"}$_{i..n}$ whose - conclusion of the form + Finally we can add to our infrastructure a cases lemma (explained in the next section) + and a structural induction principle + for the types @{text "ty\"}$_{i..n}$. The conclusion of the induction principle is + of the form % \begin{equation}\label{weakinduct} \mbox{@{text "P\<^isub>1 x\<^isub>1 \ \ \ P\<^isub>n x\<^isub>n "}} @@ -1805,8 +1809,10 @@ for the types @{text "ty\"}$_{1..n}$ by first lifting definitions from the raw level to the quotient level and then by establishing facts about these lifted definitions. All necessary proofs - are generated automatically by custom ML-code. This code can deal with - specifications such as the one shown in Figure~\ref{nominalcorehas} for Core-Haskell. + are generated automatically by custom ML-code. + + %This code can deal with + %specifications such as the one shown in Figure~\ref{nominalcorehas} for Core-Haskell. %\begin{figure}[t!] %\begin{boxedminipage}{\linewidth} @@ -2084,17 +2090,17 @@ representations have to resort to the iterated-single-binders-approach with all the unwanted consequences when reasoning about the resulting terms. - Two formalisations involving general binders have been - performed in older - versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W - \cite{BengtsonParow09,UrbanNipkow09}). Both - use the approach based on iterated single binders. Our experience with - the latter formalisation has been disappointing. The major pain arose from - the need to ``unbind'' variables. This can be done in one step with our - general binders described in this paper, but needs a cumbersome - iteration with single binders. The resulting formal reasoning turned out to - be rather unpleasant. The hope is that the extension presented in this paper - is a substantial improvement. + %Two formalisations involving general binders have been + %performed in older + %versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W + %\cite{BengtsonParow09,UrbanNipkow09}). Both + %use the approach based on iterated single binders. Our experience with + %the latter formalisation has been disappointing. The major pain arose from + %the need to ``unbind'' variables. This can be done in one step with our + %general binders described in this paper, but needs a cumbersome + %iteration with single binders. The resulting formal reasoning turned out to + %be rather unpleasant. The hope is that the extension presented in this paper + %is a substantial improvement. The most closely related work to the one presented here is the Ott-tool \cite{ott-jfp} and the C$\alpha$ml language \cite{Pottier06}. Ott is a nifty @@ -2119,36 +2125,38 @@ binding clauses. In Ott you specify binding clauses with a single body; we allow more than one. We have to do this, because this makes a difference for our notion of $\alpha$-equivalence in case of \isacommand{bind (set)} and - \isacommand{bind (res)}. Consider the examples + \isacommand{bind (res)}. - \begin{center} - \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}} - @{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} & - \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\ - @{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} & - \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t"}, - \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "s"}\\ - \end{tabular} - \end{center} + %Consider the examples + % + %\begin{center} + %\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}} + %@{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} & + % \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\ + %@{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} & + % \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t"}, + % \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "s"}\\ + %\end{tabular} + %\end{center} + % + %\noindent + %In the first term-constructor we have a single + %body that happens to be ``spread'' over two arguments; in the second term-constructor we have + %two independent bodies in which the same variables are bound. As a result we + %have + % + %\begin{center} + %\begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l} + %@{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ & + %@{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}\\ + %@{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ & + %@{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\ + %\end{tabular} + %\end{center} \noindent - In the first term-constructor we have a single - body that happens to be ``spread'' over two arguments; in the second term-constructor we have - two independent bodies in which the same variables are bound. As a result we - have - - \begin{center} - \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l} - @{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ & - @{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}\\ - @{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ & - @{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\ - \end{tabular} - \end{center} - - \noindent - and therefore need the extra generality to be able to distinguish between - both specifications. + %and therefore need the extra generality to be able to distinguish between + %both specifications. Because of how we set up our definitions, we also had to impose some restrictions (like a single binding function for a deep binder) that are not present in Ott. Our expectation is that we can still cover many interesting term-calculi from @@ -2187,10 +2195,11 @@ $\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL. To specify general binders we used the specifications from Ott, but extended them in some places and restricted - them in others so that they make sense in the context of $\alpha$-equated terms. We also introduced two binding modes (set and res) that do not + them in others so that they make sense in the context of $\alpha$-equated terms. + We also introduced two binding modes (set and res) that do not exist in Ott. We have tried out the extension with terms from Core-Haskell, type-schemes - and the lambda-calculus, and our code + and a dozen of other calculi from programming language research. The code will eventually become part of the next Isabelle distribution.\footnote{For the moment it can be downloaded from the Mercurial repository linked at \href{http://isabelle.in.tum.de/nominal/download} @@ -2204,31 +2213,31 @@ definitions to equivariant functions (for such functions it is possible to provide more automation). - There are some restrictions we imposed in this paper that we would like to lift in - future work. One is the exclusion of nested datatype definitions. Nested - datatype definitions allow one to specify, for instance, the function kinds - in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded - version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To - achieve this, we need a slightly more clever implementation than we have at the moment. + %There are some restrictions we imposed in this paper that we would like to lift in + %future work. One is the exclusion of nested datatype definitions. Nested + %datatype definitions allow one to specify, for instance, the function kinds + %in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded + %version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To + %achieve this, we need a slightly more clever implementation than we have at the moment. - A more interesting line of investigation is whether we can go beyond the - simple-minded form of binding functions that we adopted from Ott. At the moment, binding - functions can only return the empty set, a singleton atom set or unions - of atom sets (similarly for lists). It remains to be seen whether - properties like + %A more interesting line of investigation is whether we can go beyond the + %simple-minded form of binding functions that we adopted from Ott. At the moment, binding + %functions can only return the empty set, a singleton atom set or unions + %of atom sets (similarly for lists). It remains to be seen whether + %properties like + %% + %\begin{center} + %@{text "fa_ty x = bn x \ fa_bn x"}. + %\end{center} % - \begin{center} - @{text "fa_ty x = bn x \ fa_bn x"}. - \end{center} - - \noindent - allow us to support more interesting binding functions. - - We have also not yet played with other binding modes. For example we can - imagine that there is need for a binding mode - where instead of lists, we abstract lists of distinct elements. - Once we feel confident about such binding modes, our implementation - can be easily extended to accommodate them. + %\noindent + %allow us to support more interesting binding functions. + % + %We have also not yet played with other binding modes. For example we can + %imagine that there is need for a binding mode + %where instead of lists, we abstract lists of distinct elements. + %Once we feel confident about such binding modes, our implementation + %can be easily extended to accommodate them. \medskip \noindent