# HG changeset patch # User Christian Urban # Date 1268988034 -3600 # Node ID a37c65fe10de5a216c6903fd5f629482956d95f9 # Parent 813ce40078d92c6a1b3a6ef2c4858bae0aaddf19 more tuning on the paper diff -r 813ce40078d9 -r a37c65fe10de Paper/Paper.thy --- a/Paper/Paper.thy Thu Mar 18 23:39:48 2010 +0100 +++ b/Paper/Paper.thy Fri Mar 19 09:40:34 2010 +0100 @@ -16,15 +16,15 @@ text {* So far, Nominal Isabelle provides a mechanism for constructing - automatically alpha-equated terms such as + alpha-equated terms such as \begin{center} $t ::= x \mid t\;t \mid \lambda x. t$ \end{center} \noindent - where bound variables have a name. - For such terms it derives automatically a reasoning + where free and bound variables have names. + For such terms Nominal Isabelle derives automatically a reasoning infrastructure, which has been used in formalisations of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency @@ -33,7 +33,7 @@ used by Pollack for formalisations in the locally-nameless approach to binding \cite{SatoPollack10}. - However, Nominal Isabelle fared less well in a formalisation of + However, Nominal Isabelle has fared less well in a formalisation of the algorithm W \cite{UrbanNipkow09}, where types and type-schemes are of the form @@ -44,17 +44,17 @@ \end{center} \noindent - and the quantification abstracts over a finite (possibly empty) set of type variables. + and the quantification binds a finite (possibly empty) set of type-variables. While it is possible to formalise such abstractions by iterating single bindings, - it leads to a very clumsy formalisation of W. This need of iterating single binders - for representing multiple binders is also the reason why Nominal Isabelle and other + this leads to a rather clumsy formalisation of W. This need of iterating single binders + in order to representing multiple binders is also one reason why Nominal Isabelle and other theorem provers have not fared extremely well with the more advanced tasks - in the POPLmark challenge \cite{challenge05}, because also there one would be able - to aviod clumsy reasoning if there were a mechanisms for abstracting several variables - at once. + in the POPLmark challenge \cite{challenge05}, because also there one would like + to bind multiple variables at once. - To see this, let us point out some interesting properties of binders abstracting multiple - variables. First, in the case of type-schemes, we do not like to make a distinction + Binding multiple variables in a single abstraction has interesting properties that are not + captured by iterating single binders. First, + in the case of type-schemes, we do not like to make a distinction about the order of the bound variables. Therefore we would like to regard the following two type-schemes as alpha-equivalent @@ -78,6 +78,7 @@ \end{center} \noindent + where $z$ does not occur freely in the type. In this paper we will give a general abstraction mechanism and associated notion of alpha-equivalence that can be used to faithfully represent type-schemes in Nominal Isabelle. The difficulty of finding the right notion @@ -89,13 +90,13 @@ However, the notion of alpha-equivalence that is preserved by vacuous binders is not alway wanted. For example in terms like - \begin{center} - $\LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END$ - \end{center} + \begin{equation}\label{one} + \LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END + \end{equation} \noindent we might not care in which order the assignments $x = 3$ and $y = 2$ are - given, but it would be unusual to regard the above term as alpha-equivalent + given, but it would be unusual to regard \eqref{one} as alpha-equivalent with \begin{center} @@ -105,29 +106,28 @@ \noindent Therefore we will also provide a separate abstraction mechanism for cases in which the order of binders does not matter, but the ``cardinality'' of the - binders has to be the same. + binders has to agree. However, we found that this is still not sufficient for covering language constructs frequently occuring in programming language research. For example in $\mathtt{let}$s involving patterns - \begin{center} - $\LET (x, y) = (3, 2) \IN x\,\backslash\,y \END$ - \end{center} + \begin{equation}\label{two} + \LET (x, y) = (3, 2) \IN x\,\backslash\,y \END + \end{equation} \noindent - we want to bind all variables from the pattern (there might be an arbitrary - number of them) inside the body of the $\mathtt{let}$, but we also care about - the order of these variables, since we do not want to identify the above term - with + we want to bind all variables from the pattern inside the body of the + $\mathtt{let}$, but we also care about the order of these variables, since + we do not want to identify \eqref{two} with \begin{center} $\LET (y, x) = (3, 2) \IN x\,\backslash y\,\END$ \end{center} \noindent - As a result, we provide three general abstraction mechanisms for multiple binders - and allow the user to chose which one is intended when formalising a + As a result, we provide three general abstraction mechanisms for binding multiple + variables and allow the user to chose which one is intended when formalising a programming language calculus. By providing these general abstraction mechanisms, however, we have to work around @@ -149,9 +149,9 @@ \end{center} \noindent - where the $[\_\!\_].\_\!\_$ indicates that a list of variables becomes - bound in $s$. In this representation we need additional predicates to ensure - that the two lists are of equal length. This can result into very + where the notation $[\_\!\_].\_\!\_$ indicates that a set of variables becomes + bound in $s$. In this representation we need additional predicates about terms + to ensure that the two lists are of equal length. This can result into very unintelligible reasoning (see for example~\cite{BengtsonParow09}). To avoid this, we will allow for example specifications of $\mathtt{let}$s as follows @@ -168,21 +168,22 @@ \noindent where $assn$ is an auxiliary type representing a list of assignments and $bn$ an auxilary function identifying the variables to be bound by - the $\mathtt{let}$, given by + the $\mathtt{let}$. This function can be defined as \begin{center} $bn\,(\mathtt{anil}) = \varnothing \qquad bn\,(\mathtt{acons}\;x\;t\;as) = \{x\} \cup bn\,(as)$ \end{center} \noindent - This style of specifications for term-calculi with multiple binders is heavily - inspired by the Ott-tool \cite{ott-jfp}. + This style of specifying terms and bindings is heavily + inspired by the syntax of the Ott-tool \cite{ott-jfp}. - We will not be able to deal with all specifications that are allowed by + However, we will not be able to deal with all specifications that are allowed by Ott. One reason is that we establish the reasoning infrastructure for alpha-\emph{equated} terms. In contrast, Ott produces for a subset of its - specifiactions a reasoning infrastructure involving concrete, - \emph{non}-alpha-equated terms. To see the difference, note that working + specifiactions a reasoning infrastructure for terms that have names for + bound variables, but these terms are concrete, \emph{non}-alpha-equated terms. To see + the difference, note that working with alpha-equated terms means that the two type-schemes with $x$, $y$ and $z$ being distinct @@ -191,25 +192,23 @@ \end{center} \noindent - are not just alpha-equal, but actually equal---we are working with - alpha-equivalence classes, but still have that bound variables - carry a name. - Our insistence on reasoning with alpha-equated terms comes from the - wealth of experience we gained with the older version of Nominal - Isabelle: for non-trivial properties, - reasoning about alpha-equated terms is much easier than reasoning - with concrete terms. The fundamental reason is that the HOL-logic - underlying Nominal Isabelle allows us to replace ``equals-by-equals''. - Replacing ``alpha-equals-by-alpha-equals'' requires a lot of work. + are not just alpha-equal, but actually equal. Our insistence on reasoning + with alpha-equated terms comes from the wealth of experience we gained with + the older version of Nominal Isabelle: for non-trivial properties, reasoning + about alpha-equated terms is much easier than reasoning with concrete + terms. The fundamental reason for this is that the HOL-logic underlying + Nominal Isabelle allows us to replace ``equals-by-equals''. In contrast, + replacing ``alpha-equals-by-alpha-equals'' requires a lot of extra work. + - Although a reasoning infrastructure for alpha-equated terms with names - is in informal reasoning nearly always taken for granted, establishing + Although in informal settings a reasoning infrastructure for alpha-equated + terms that have names is nearly always taken for granted, establishing it automatically in a theorem prover is a rather non-trivial task. - For every specification we will construct a type that contains - exactly the corresponding alpha-equated terms. For this we use the - standard HOL-technique of defining a new type that has been - identified as a non-empty subset of an existing type. In our - context we take as the starting point the type of sets of concrete + For every specification we will need to construct a type containing as + elements exactly those sets containing alpha-equal 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. In our + we take as the starting point the type of sets of concrete terms (the latter being defined as datatypes). Then quotient these sets according to our alpha-equivalence relation and then identifying the new type as these alpha-equivalence classes. The construction we @@ -271,8 +270,8 @@ logic work are sorted atoms and permutations of atoms. The sorted atoms represent different kinds of variables, such as term- and type-variables in Core-Haskell, and it is assumed that there is an infinite supply of atoms - for each sort. However, in order to simplify the description of our work, we - shall assume in this paper that there is only a single sort of atoms. + for each sort. However, in order to simplify the description, we + shall assume in what follows that there is only a single sort of atoms. Permutations are bijective functions from atoms to atoms that are the identity everywhere except on a finite number of atoms. There is a diff -r 813ce40078d9 -r a37c65fe10de Paper/document/root.bib --- a/Paper/document/root.bib Thu Mar 18 23:39:48 2010 +0100 +++ b/Paper/document/root.bib Fri Mar 19 09:40:34 2010 +0100 @@ -1,3 +1,13 @@ +@incollection{UrbanNipkow09, + author = {C.~Urban and T.~Nipkow}, + title = {{N}ominal {V}erification of {A}lgorithm {W}}, + booktitle={From Semantics to Computer Science. Essays in Honour of Gilles Kahn}, + editor={G.~Huet and J.-J.~L{\'e}vy and G.~Plotkin}, + publisher={Cambridge University Press}, + pages={363--382}, + year=2009 +} + @InProceedings{Homeier05, author = {P.~Homeier}, title = {{A} {D}esign {S}tructure for {H}igher {O}rder {Q}uotients}, diff -r 813ce40078d9 -r a37c65fe10de Paper/document/root.tex --- a/Paper/document/root.tex Thu Mar 18 23:39:48 2010 +0100 +++ b/Paper/document/root.tex Fri Mar 19 09:40:34 2010 +0100 @@ -51,7 +51,7 @@ opposed to de-Bruijn indices). In this paper we present an extension of Nominal Isabelle in order to deal with general binding structures. Such binding structures are ubiquitous in programming language research and only -very poorly supported with single binders, as for example found in the +very poorly supported with single binders, such as the lambdas in the lambda-calculus. For our extension we introduce novel definitions of alpha-equivalence and establish automatically the reasoning infrastructure for alpha-equated terms. This includes strong induction principles that have the