# HG changeset patch # User Christian Urban # Date 1269009823 -3600 # Node ID 66d388a84e3cc008cef567c3317bef7afec5bd74 # Parent dbdce626c9254551d26ed29e836c48e7f0e9bce7 polished diff -r dbdce626c925 -r 66d388a84e3c Paper/Paper.thy --- a/Paper/Paper.thy Fri Mar 19 12:31:55 2010 +0100 +++ b/Paper/Paper.thy Fri Mar 19 15:43:43 2010 +0100 @@ -23,10 +23,10 @@ \end{center} \noindent - where free and bound variables have names. - For such terms Nominal Isabelle derives automatically a reasoning - infrastructure, which has been used successfully in formalisations of an equivalence - checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed + where free and bound variables have names. For such terms Nominal Isabelle + derives automatically a reasoning infrastructure, which has been used + successfully in formalisations of an equivalence checking algorithm for LF + \cite{UrbanCheneyBerghofer08}, Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been @@ -44,19 +44,19 @@ \end{center} \noindent - and the quantification binds at once 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 and similar - theorem provers have 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. + and the quantification binds at once 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 and similar theorem provers that only provide + mechanisms for binding single variables have 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 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 + Binding multiple variables 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 \begin{center} $\forall \{x, y\}. x \rightarrow y \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x$ @@ -89,7 +89,7 @@ alway wanted. For example in terms like \begin{equation}\label{one} - \LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END + \LET x = 3 \AND y = 2 \IN x\,-\,y \END \end{equation} \noindent @@ -98,20 +98,20 @@ with \begin{center} - $\LET x = 3 \AND y = 2 \AND z = loop \IN x\,\backslash\,y \END$ + $\LET x = 3 \AND y = 2 \AND z = loop \IN x\,-\,y \END$ \end{center} \noindent - Therefore we will also provide a separate binding mechanism for cases - in which the order of binders does not matter, but the ``cardinality'' of the + Therefore we will also provide a separate binding mechanism for cases in + which the order of binders does not matter, but the ``cardinality'' of the binders has to agree. - However, we found that this is still not sufficient for dealing with language - constructs frequently occurring in programming language research. For example - in $\mathtt{let}$s involving patterns + However, we found that this is still not sufficient for dealing with + language constructs frequently occurring in programming language + research. For example in $\mathtt{let}$s containing patterns \begin{equation}\label{two} - \LET (x, y) = (3, 2) \IN x\,\backslash\,y \END + \LET (x, y) = (3, 2) \IN x\,-\,y \END \end{equation} \noindent @@ -120,7 +120,7 @@ we do not want to identify \eqref{two} with \begin{center} - $\LET (y, x) = (3, 2) \IN x\,\backslash y\,\END$ + $\LET (y, x) = (3, 2) \IN x\,- y\,\END$ \end{center} \noindent @@ -140,7 +140,7 @@ which bind all the $x_i$ in $s$, we might not care about the order in which the $x_i = t_i$ are given, but we do care about the information that there are as many $x_i$ as there are $t_i$. We lose this information if we represent the - $\mathtt{let}$-constructor as something like + $\mathtt{let}$-constructor by something like \begin{center} $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$ @@ -148,10 +148,11 @@ \noindent where the notation $[\_\!\_].\_\!\_$ indicates that the $x_i$ become - bound in $s$. In this representation we need additional predicates about terms + bound in $s$. In this representation the term \mbox{$\LET [x].s\;\;[t_1,t_2]$} + would be perfectly legal instance, and so one needs 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 to specify $\mathtt{let}$s + messy reasoning (see for example~\cite{BengtsonParow09}). + To avoid this, we will allow for example to specify $\mathtt{let}$s as follows \begin{center} @@ -173,17 +174,18 @@ \end{center} \noindent - The scope of the binding is indicated by labels given to the types, for example - $s\!::\!trm$, and a binding clause $\mathtt{bind}\;bn\,(a) \IN s$. - This style of specifying terms and bindings is heavily + The scope of the binding is indicated by labels given to the types, for + example \mbox{$s\!::\!trm$}, and a binding clause, in this case + $\mathtt{bind}\;bn\,(a) \IN s$, that states bind all the names the function + $bn$ returns in $s$. This style of specifying terms and bindings is heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. 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 specifications a reasoning infrastructure in Isabelle for + its specifications a reasoning infrastructure in Isabelle/HOL for \emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms - and the concrete terms produced by Ott use names for the bound variables, + and the raw terms produced by Ott use names for the bound variables, there is a key difference: working with alpha-equated terms means that the two type-schemes with $x$, $y$ and $z$ being distinct @@ -192,26 +194,29 @@ \end{center} \noindent - are not just alpha-equal, but actually equal (note the ``=''-sign). 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''. In contrast replacing - ``alpha-equals-by-alpha-equals'' in a term calculus requires a lot of extra reasoning work. + are not just alpha-equal, but actually equal. As a + result, we can only support specifications that make sense on the level of + alpha-equated terms (offending specifications, which for example bind a variable + according to a variable bound somewhere else, are not excluded by Ott). 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 raw terms. The fundamental reason is that the + HOL-logic underlying Nominal Isabelle allows us to replace + ``equals-by-equals''. In contrast replacing ``alpha-equals-by-alpha-equals'' + in a representation based on raw terms requires a lot of extra reasoning work. - Although in informal settings a reasoning infrastructure for alpha-equated terms (that have names for bound variables) is nearly always taken for granted, establishing - it automatically in a theorem prover is a rather non-trivial task. + it automatically in the Isabelle/HOL theorem prover is a rather non-trivial task. For every specification we will need to construct a type 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. In our - case we take as the starting point the type of sets of concrete - terms (the latter being defined as a datatype). Then identify the + case we take as the starting point the type of sets of raw + terms (the latter being defined as a datatype); identify the alpha-equivalence classes according to our alpha-equivalence relation and - then identify the new type as these alpha-equivalence classes. The construction we + then define the new type as these alpha-equivalence classes. The construction we can perform in HOL is illustrated by the following picture: \begin{center} @@ -240,7 +245,7 @@ \noindent To ``lift'' the reasoning from the underlying type to the new type is usually a tricky task. To ease this task we reimplemented in Isabelle/HOL - the quotient package described by Homeier in \cite{Homeier05}. This + the quotient package described by Homeier \cite{Homeier05}. This re-implementation will automate the proofs we require for our reasoning infrastructure over alpha-equated terms.\medskip diff -r dbdce626c925 -r 66d388a84e3c Paper/document/root.tex --- a/Paper/document/root.tex Fri Mar 19 12:31:55 2010 +0100 +++ b/Paper/document/root.tex Fri Mar 19 15:43:43 2010 +0100 @@ -55,8 +55,8 @@ very poorly supported with single binders, such as the lambdas in the lambda-calculus. Our extension includes novel definitions of alpha-equivalence and establishes automatically the reasoning infrastructure for -alpha-equated terms. This includes strong induction principles that have the -usual variable convention already built in. +alpha-equated terms. We can also provide strong induction principles that have +the usual variable convention already built in. \end{abstract}