# HG changeset patch # User Christian Urban # Date 1286541714 -3600 # Node ID c86b98642013d351317ef7c55bff47600a2c38d9 # Parent 06a8f782b2c14026409fee699eddac0bd6c308f0 down to 20 pages diff -r 06a8f782b2c1 -r c86b98642013 Paper/Paper.thy --- a/Paper/Paper.thy Thu Oct 07 14:23:32 2010 +0900 +++ b/Paper/Paper.thy Fri Oct 08 13:41:54 2010 +0100 @@ -87,13 +87,14 @@ and the @{text "\"}-quantification binds a finite (possibly empty) set of type-variables. While it is possible to implement this kind of more general binders by iterating single binders, this leads to a rather clumsy - formalisation of W. The need of iterating single binders is also one reason - why Nominal Isabelle + formalisation of W. + %The need of iterating single binders is also one reason + %why Nominal Isabelle % and similar theorem provers that only provide %mechanisms for binding single variables - has not fared extremely well with the - more advanced tasks in the POPLmark challenge \cite{challenge05}, because - also there one would like to bind multiple variables at once. + %has not fared extremely well with the + %more advanced tasks in the POPLmark challenge \cite{challenge05}, because + %also there one would like to bind multiple variables at once. Binding multiple variables has interesting properties that cannot be captured easily by iterating single binders. For example in the case of type-schemes we do not @@ -274,7 +275,7 @@ Although in informal settings a reasoning infrastructure for $\alpha$-equated terms is nearly always taken for granted, establishing it automatically in the Isabelle/HOL is a rather non-trivial task. For every - specification we will need to construct a type containing as elements the + specification we will need to construct type(s) containing as elements the $\alpha$-equated terms. To do so, we use the standard HOL-technique of defining a new type by identifying a non-empty subset of an existing type. The construction we perform in Isabelle/HOL can be illustrated by the following picture: @@ -309,8 +310,8 @@ the type of sets of raw terms according to our $\alpha$-equivalence relation, and finally define the new type as these $\alpha$-equivalence classes (non-emptiness is satisfied whenever the raw terms are definable as datatype - in Isabelle/HOL and the property that our relation for $\alpha$-equivalence is - indeed an equivalence relation). + in Isabelle/HOL and our relation for $\alpha$-equivalence is + an equivalence relation). %The fact that we obtain an isomorphism between the new type and the %non-empty subset shows that the new type is a faithful representation of @@ -379,9 +380,9 @@ from the Ott-tool, but we introduce crucial restrictions, and also extensions, so that our specifications make sense for reasoning about $\alpha$-equated terms. The main improvement over Ott is that we introduce three binding modes - (only one is present in Ott), provide definitions for $\alpha$-equivalence and + (only one is present in Ott), provide formalised definitions for $\alpha$-equivalence and for free variables of our terms, and also derive a reasoning infrastructure - for our specifications inside Isabelle/HOL. + for our specifications inside Isabelle/HOL from ``first principles''. %\begin{figure} @@ -459,20 +460,37 @@ for example permutations acting on products, lists, sets, functions and booleans is given by: % - \begin{equation}\label{permute} - \mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}} + %\begin{equation}\label{permute} + %\mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}} + %\begin{tabular}{@ {}l@ {}} + %@{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm] + %@{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\ + %@{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\ + %\end{tabular} & + %\begin{tabular}{@ {}l@ {}} + %@{thm permute_set_eq[no_vars, THEN eq_reflection]}\\ + %@{text "p \ f \ \x. p \ (f (- p \ x))"}\\ + %@{thm permute_bool_def[no_vars, THEN eq_reflection]} + %\end{tabular} + %\end{tabular}} + %\end{equation} + % + \begin{center} + \mbox{\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {\hspace{4mm}}c@ {}} \begin{tabular}{@ {}l@ {}} - @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm] + @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\ + @{thm permute_bool_def[no_vars, THEN eq_reflection]} + \end{tabular} & + \begin{tabular}{@ {}l@ {}} @{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\ @{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\ \end{tabular} & \begin{tabular}{@ {}l@ {}} @{thm permute_set_eq[no_vars, THEN eq_reflection]}\\ @{text "p \ f \ \x. p \ (f (- p \ x))"}\\ - @{thm permute_bool_def[no_vars, THEN eq_reflection]} \end{tabular} \end{tabular}} - \end{equation} + \end{center} \noindent Concrete permutations in Nominal Isabelle are built up from swappings, @@ -504,11 +522,12 @@ A striking consequence of these definitions is that we can prove without knowing anything about the structure of @{term x} that swapping two fresh atoms, say @{text a} and @{text b}, leaves - @{text x} unchanged: + @{text x} unchanged, namely if @{text "a \ x"} and @{text "b \ x"} + then @{term "(a \ b) \ x"}. - \begin{myproperty}\label{swapfreshfresh} - @{thm[mode=IfThen] swap_fresh_fresh[no_vars]} - \end{myproperty} + %\begin{myproperty}\label{swapfreshfresh} + %@{thm[mode=IfThen] swap_fresh_fresh[no_vars]} + %\end{myproperty} %While often the support of an object can be relatively easily %described, for example for atoms, products, lists, function applications, @@ -629,8 +648,9 @@ In order to keep our work with deriving the reasoning infrastructure manageable, we will wherever possible state definitions and perform proofs - on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code that - generates them anew for each specification. To that end, we will consider + on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code. % that + %generates them anew for each specification. + To that end, we will consider first pairs @{text "(as, x)"} of type @{text "(atom set) \ \"}. These pairs are intended to represent the abstraction, or binding, of the set of atoms @{text "as"} in the body @{text "x"}. @@ -657,7 +677,7 @@ \mbox{\it (iv)} & @{term "(p \ as) = bs"} \\ \end{array} \end{equation} - + % \noindent Note that this relation depends on the permutation @{text "p"}; $\alpha$-equivalence between two pairs is then the relation where we @@ -682,7 +702,7 @@ \mbox{\it (iv)} & @{term "(p \ as) = bs"}\\ \end{array} \end{equation} - + % \noindent where @{term set} is the function that coerces a list of atoms into a set of atoms. Now the last clause ensures that the order of the binders matters (since @{text as} @@ -701,12 +721,12 @@ \end{array} \end{equation} - It might be useful to consider first some examples about how these definitions + It might be useful to consider first some examples how these definitions of $\alpha$-equivalence pan out in practice. For this consider the case of abstracting a set of atoms over types (as in type-schemes). We set @{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we define - + % \begin{center} @{text "fa(x) = {x}"} \hspace{5mm} @{text "fa(T\<^isub>1 \ T\<^isub>2) = fa(T\<^isub>1) \ fa(T\<^isub>2)"} \end{center} @@ -1049,7 +1069,7 @@ \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\smallskip\\ \end{tabular}} \end{equation} - + % \noindent In this specification the function @{text "bn"} determines which atoms of the pattern @{text p} are bound in the argument @{text "t"}. Note that in the @@ -1059,14 +1079,14 @@ As said above, for deep binders we allow binding clauses such as % - \begin{center} - \begin{tabular}{ll} - @{text "Bar p::pat t::trm"} & - \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"}\\ - \end{tabular} - \end{center} - - \noindent + %\begin{center} + %\begin{tabular}{ll} + @{text "Bar p::pat t::trm"} %%%& + \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"} %%\\ + %\end{tabular} + %\end{center} + % + %\noindent where the argument of the deep binder also occurs in the body. We call such binders \emph{recursive}. To see the purpose of such recursive binders, compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following @@ -1088,7 +1108,7 @@ \hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\ \end{tabular}} \end{equation} - + % \noindent The difference is that with @{text Let} we only want to bind the atoms @{text "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms @@ -1098,7 +1118,7 @@ To make sure that atoms bound by deep binders cannot be free at the same time, we cannot have more than one binding function for a deep binder. Consequently we exclude specifications such as - + % \begin{center} \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}} @{text "Baz\<^isub>1 p::pat t::trm"} & @@ -1244,20 +1264,20 @@ @{text "D"} stands for the set of free atoms of the bodies, @{text B} for the set of binding atoms in the binders and @{text "B'"} for the set of free atoms in non-recursive deep binders, - then the free atoms of the binding clause @{text bc\<^isub>i} are + then the free atoms of the binding clause @{text bc\<^isub>i} are\\[-2mm] % \begin{equation}\label{fadef} \mbox{@{text "fa(bc\<^isub>i) \ (D - B) \ B'"}}. \end{equation} - + % \noindent The set @{text D} is formally defined as % - \begin{center} + %\begin{center} @{text "D \ fa_ty\<^isub>1 d\<^isub>1 \ ... \ fa_ty\<^isub>q d\<^isub>q"} - \end{center} - - \noindent + %\end{center} + % + %\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; @@ -1265,7 +1285,7 @@ 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 + for atom types to which shallow binders may refer\\[-4mm] % %\begin{center} %\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} @@ -1276,21 +1296,21 @@ %\end{center} % \begin{center} - @{text "bn_atom a \ {atom a}"}\hspace{17mm} - @{text "bn_atom_set as \ atoms as"}\\ - @{text "bn_atom_list as \ atoms (set as)"} + @{text "bn\<^bsub>atom\<^esub> a \ {atom a}"}\hfill + @{text "bn\<^bsub>atom_set\<^esub> as \ atoms as"}\hfill + @{text "bn\<^bsub>atom_list\<^esub> as \ atoms (set as)"} \end{center} - + % \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}"}. - The set @{text B} is then formally defined as + The set @{text B} is then formally defined as\\[-4mm] % \begin{center} @{text "B \ bn_ty\<^isub>1 b\<^isub>1 \ ... \ bn_ty\<^isub>p b\<^isub>p"} \end{center} - + % \noindent where we use the auxiliary binding functions for shallow binders. The set @{text "B'"} collects all free atoms in non-recursive deep @@ -1303,12 +1323,12 @@ %\noindent with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ and none of the @{text "l"}$_{1..r}$ being among the bodies @{text - "d"}$_{1..q}$. The set @{text "B'"} is defined as + "d"}$_{1..q}$. The set @{text "B'"} is defined as\\[-5mm] % \begin{center} - @{text "B' \ fa_bn\<^isub>1 l\<^isub>1 \ ... \ fa_bn\<^isub>r l\<^isub>r"} - \end{center} - + @{text "B' \ fa_bn\<^isub>1 l\<^isub>1 \ ... \ fa_bn\<^isub>r l\<^isub>r"}\\[-9mm] + \end{center} + % \noindent This completes the definition of the free-atom functions @{text "fa_ty"}$_{1..n}$. @@ -1365,7 +1385,7 @@ Recall that @{text ANil} and @{text "ACons"} have no binding clause in the specification. The corresponding free-atom function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all free atoms - occurring in an assignment (in case of @{text "ACons"}, they are given in + of an assignment (in case of @{text "ACons"}, they are given in terms of @{text supp}, @{text "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}). The binding only takes place in @{text Let} and @{text "Let_rec"}. In case of @{text "Let"}, the binding clause specifies @@ -1988,20 +2008,26 @@ clause @{text "bn (C x\<^isub>1 \ x\<^isub>r) = rhs"}, we define % \begin{center} - @{text "p \\<^bsub>bn\<^esub> (C x\<^isub>1 \ x\<^isub>r) \ C y\<^isub>1 \ y\<^isub>r"} + @{text "p \\<^bsub>bn\<^esub> (C x\<^isub>1 \ x\<^isub>r) \ C y\<^isub>1 \ y\<^isub>r"} \;\; with + $\begin{cases} + \text{@{text "y\<^isub>i \ x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}}\\ + \text{@{text "y\<^isub>i \ p \\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}}\\ + \text{@{text "y\<^isub>i \ p \ x\<^isub>i"} otherwise} + \end{cases}$ \end{center} % + %\noindent + %with @{text "y\<^isub>i"} determined as follows: + % + %\begin{center} + %\begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}} + %$\bullet$ & @{text "y\<^isub>i \ x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\ + %$\bullet$ & @{text "y\<^isub>i \ p \\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\ + %$\bullet$ & @{text "y\<^isub>i \ p \ x\<^isub>i"} otherwise + %\end{tabular} + %\end{center} + % \noindent - with @{text "y\<^isub>i"} determined as follows: - % - \begin{center} - \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}} - $\bullet$ & @{text "y\<^isub>i \ x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\ - $\bullet$ & @{text "y\<^isub>i \ p \\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\ - $\bullet$ & @{text "y\<^isub>i \ p \ x\<^isub>i"} otherwise - \end{tabular} - \end{center} - % Now Properties \ref{supppermeq} and \ref{avoiding} give us a permutation @{text q} such that @{text "(set (bn (q \\<^bsub>bn\<^esub> p)) \\<^sup>* c"} holds and such that @{text "[q \\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \ t)"} is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \\<^bsub>bn\<^esub> p) \\<^bsub>bn\<^esub> p"}. But @@ -2186,17 +2212,19 @@ %unwanted terms. Our guess is that such predicates result in rather %intricate formal reasoning. - Another representation technique for binding is higher-order abstract syntax - (HOAS), which for example is implemented in the Twelf system. This representation + Another technique for representing binding is higher-order abstract syntax + (HOAS). %, which for example is implemented in the Twelf system. + This %%representation technique supports very elegantly many aspects of \emph{single} binding, and impressive work has been done that uses HOAS for mechanising the metatheory of SML~\cite{LeeCraryHarper07}. We are, however, not aware how multiple binders of SML are represented in this work. Judging from the submitted Twelf-solution for the POPLmark challenge, HOAS cannot easily deal with - binding constructs where the number of bound variables is not fixed. For - example in the second part of this challenge, @{text "Let"}s involve + binding constructs where the number of bound variables is not fixed. %For + example + In the second part of this challenge, @{text "Let"}s involve patterns that bind multiple variables at once. In such situations, HOAS - representations have to resort to the iterated-single-binders-approach with + seems to 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 @@ -2224,7 +2252,7 @@ notion of $\alpha$-equivalence. A definition for the notion of free variables is work in progress in Ott. - Although we were heavily inspired by the syntax in Ott, + Although we were heavily inspired by the syntax of Ott, its definition of $\alpha$-equivalence is unsuitable for our extension of Nominal Isabelle. First, it is far too complicated to be a basis for automated proofs implemented on the ML-level of Isabelle/HOL. Second, it @@ -2294,7 +2322,7 @@ has a more operational flavour and calculates a partial (renaming) map. In this way, the definition can deal with vacuous binders. However, to our best knowledge, no concrete mathematical result concerning this - definition of $\alpha$-equivalence has been proved. + definition of $\alpha$-equivalence has been proved.\\[-7mm] *} section {* Conclusion *} @@ -2321,7 +2349,7 @@ Isabelle \cite{UrbanBerghofer06} this turned out to be a thorny issue. We hope to do better this time by using the function package that has recently been implemented in Isabelle/HOL and also by restricting function - definitions to equivariant functions (for such functions it is possible to + definitions to equivariant functions (for such functions we can provide more automation). %There are some restrictions we imposed in this paper that we would like to lift in @@ -2349,8 +2377,8 @@ %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 + % + \smallskip \noindent {\bf Acknowledgements:} %We are very grateful to Andrew Pitts for %many discussions about Nominal Isabelle. @@ -2358,7 +2386,7 @@ making the informal notes \cite{SewellBestiary} available to us and also for patiently explaining some of the finer points of the work on the Ott-tool. %Stephanie Weirich suggested to separate the subgrammars - %of kinds and types in our Core-Haskell example. + %of kinds and types in our Core-Haskell example. \\[-6mm] *} diff -r 06a8f782b2c1 -r c86b98642013 Paper/document/root.tex --- a/Paper/document/root.tex Thu Oct 07 14:23:32 2010 +0900 +++ b/Paper/document/root.tex Fri Oct 08 13:41:54 2010 +0100 @@ -23,7 +23,7 @@ \DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}} \DeclareRobustCommand{\frqq}{\mbox{\guillemotright}} \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} -\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}} +\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\hspace{-0.5mm}\cdot\hspace{-0.5mm}}$}}} \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} \renewcommand{\isasymequiv}{$\dn$} %%\renewcommand{\isasymiota}{} @@ -61,7 +61,7 @@ \newenvironment{proof-of}[1]{{\em Proof of #1:}}{} \addtolength{\textwidth}{2mm} -\addtolength{\parskip}{-0.3mm} +\addtolength{\parskip}{-0.33mm} \begin{document} \title{General Bindings and Alpha-Equivalence\\ in Nominal Isabelle}