# HG changeset patch # User Christian Urban # Date 1268946388 -3600 # Node ID 926245dd5b53a638820f44331d5b31364dfb16be # Parent eb95360d6ac6fae8120af4ee72edede381849910 tuned diff -r eb95360d6ac6 -r 926245dd5b53 Paper/Paper.thy --- a/Paper/Paper.thy Thu Mar 18 19:39:01 2010 +0100 +++ b/Paper/Paper.thy Thu Mar 18 22:06:28 2010 +0100 @@ -15,16 +15,16 @@ section {* Introduction *} text {* - So far, Nominal Isabelle provided a mechanism to construct - automatically alpha-equated lambda terms sich as + So far, Nominal Isabelle provides a mechanism for constructing + automatically alpha-equated terms such as \begin{center} $t ::= x \mid t\;t \mid \lambda x. t$ \end{center} \noindent - For such calculi, it derived automatically a convenient reasoning - infrastructure. With this it has been used to formalise an equivalence + For such terms it 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 \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result @@ -32,9 +32,9 @@ used by Pollack for formalisations in the locally-nameless approach to binding \cite{SatoPollack10}. - However, Nominal Isabelle has fared less well in a formalisation of - the algorithm W \cite{UrbanNipkow09} where types and type-schemes - are represented by + However, Nominal Isabelle fared less well in a formalisation of + the algorithm W \cite{UrbanNipkow09}, where types and type-schemes + are of the form \begin{center} \begin{tabular}{l} @@ -43,108 +43,115 @@ \end{center} \noindent - While it is possible to formalise the finite set of variables that are - abstracted in a type-scheme by iterating single abstractions, it leads to a very - clumsy formalisation. This need of iterating single binders for representing - multiple binders is also the reason why Nominal Isabelle and other theorem - provers have so far not fared very well with the more advanced tasks in the POPLmark - challenge, because also there one would like to abstract several variables + and the quantification abstracts over 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 + 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. - There are interesting points to note with binders that abstract multiple - variables. First in the case of type-schemes we do not like to make a distinction - about the order of the binders. So we would like to regard the following two - type-schemes as alpha-equivalent: + 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 + 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$ \end{center} \noindent - but assuming $x$, $y$ and $z$ are distinct, the following two should be \emph{not} - alpha-equivalent: + but the following two should \emph{not} be alpha-equivalent \begin{center} $\forall \{x, y\}. x \rightarrow y \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z$ \end{center} \noindent - However we do like to regard type-schemes as alpha-equivalent, if they - differ only on \emph{vacuous} binders, such as + assuming that $x$, $y$ and $z$ are distinct. Moreover, we like to regard type-schemes as + alpha-equivalent, if they differ only on \emph{vacuous} binders, such as \begin{center} $\forall \{x\}. x \rightarrow y \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y$ \end{center} \noindent - In this paper we will give a general abstraction mechanism and assciated notion of alpha-equivalence - which can be used to represent type-schemes. The difficulty in finding the notion of alpha-equivalence - can be appreciated by considering that the definition given by Leroy in \cite{Leroy92} is incorrect - (it omits a side-condition). + 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 + for alpha-equivalence in this case can be appreciated by considering that the + definition given by Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). + + However, the notion of alpha-equivalence that is preserved by vacuous binders is not - alway wanted. For example in constructs like + alway wanted. For example in terms like \begin{center} - $\LET x = 3 \AND y = 2 \IN x \backslash y \END$ + $\LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END$ \end{center} \noindent - we might not care in which order the associations $x = 3$ and $y = 2$ are - given, but it would be unusual to regard this term as alpha-equivalent with + 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 + 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\,\backslash\,y \END$ \end{center} \noindent - We will provide a separate abstraction mechanism for this case where the - order of binders does not matter, but the ``cardinality'' of the binders - has to be the same. + 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. - However, this is still not sufficient for covering language constructs frequently - occuring in programming language research. For example in patters like + 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$ + $\LET (x, y) = (3, 2) \IN x\,\backslash\,y \END$ \end{center} \noindent we want to bind all variables from the pattern (there might be an arbitrary - number of them) inside the body of the let, but we also care about the order - of these variables, since we do not want to identify this term with + 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 \begin{center} - $\LET (y, x) = (3, 2) \IN x \backslash y \END$ + $\LET (y, x) = (3, 2) \IN x\,\backslash y\,\END$ \end{center} \noindent - Therefore we have identified three abstraction mechanisms for multiple binders - and allow the user to chose which one is intended. + 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 + programming language calculus. - By providing general abstraction mechanisms that allow the binding of multiple - variables, we have to work around aproblem that has been first pointed out - by Pottier in \cite{Pottier}: in let-constructs such as + By providing these general abstraction mechanisms, however, we have to work around + a problem that has been pointed out by Pottier in \cite{Pottier06}: in + $\mathtt{let}$-constructs of the form \begin{center} $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$ \end{center} \noindent - where the $x_i$ are bound in $s$. In this term we might not care about the order in + 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 specify the + as many $x_i$ as there are $t_i$. We lose this information if we represent the $\mathtt{let}$-constructor as something like \begin{center} - $\LET [x_1,\ldots,x_n].s\; [t_1,\ldots,t_n]$ + $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$ \end{center} \noindent - where the $[\_].\_$ indicates that a list of variables become bound + 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 - elaborate reasoning (see \cite{BengtsonParow09}). + unintelligible reasoning (see for example~\cite{BengtsonParow09}). diff -r eb95360d6ac6 -r 926245dd5b53 Paper/document/root.bib --- a/Paper/document/root.bib Thu Mar 18 19:39:01 2010 +0100 +++ b/Paper/document/root.bib Thu Mar 18 22:06:28 2010 +0100 @@ -9,6 +9,16 @@ series = {LNCS} } +@INPROCEEDINGS{Pottier06, + author = {F.~Pottier}, + title = {{A}n {O}verview of {C$\alpha$ml}}, + year = {2006}, + booktitle = {ACM Workshop on ML}, + pages = {27--52}, + volume = {148}, + number = {2}, + series = {ENTCS} +} @Unpublished{HuffmanUrban10, author = {B.~Huffman and C.~Urban}, @@ -32,6 +42,21 @@ note = {Personal communication.} } +@InProceedings{challenge05, + author = {B.~E.~Aydemir and A.~Bohannon and M.~Fairbairn and + J.~N.~Foster and B.~C.~Pierce and P.~Sewell and + D.~Vytiniotis and G.~Washburn and S.~Weirich and + S.~Zdancewic}, + title = {{M}echanized {M}etatheory for the {M}asses: {T}he \mbox{Popl}{M}ark + {C}hallenge}, + booktitle = {Proc.~of the 18th International Conference on Theorem Proving in Higher-Order + Logics (TPHOLs)}, + pages = {50--65}, + year = {2005}, + volume = {3603}, + series = {LNCS} +} + @Unpublished{SatoPollack10, author = {M.~Sato and R.~Pollack}, title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus}, diff -r eb95360d6ac6 -r 926245dd5b53 Paper/document/root.tex --- a/Paper/document/root.tex Thu Mar 18 19:39:01 2010 +0100 +++ b/Paper/document/root.tex Thu Mar 18 22:06:28 2010 +0100 @@ -48,13 +48,13 @@ Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem prover. It provides a proving infrastructure for convenient reasoning about programming language calculi. In this paper we present an extension of Nominal -Isabelle for dealing with general binding structures. Such binding structures +Isabelle in order to deal with general binding structures. Such binding structures are ubiquitous in programming language research and only very poorly supported -by theorem provers providing only single binding as in the lambda-calculus. We -give in this paper novel definitions for alpha-equivalence and establish -automatically the reasoning structure for alpha-equated terms. For example we -provide a strong induction principle that has the variable convention already -built in. +with single binders, as for example found 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 a strong induction principle which has the variable convention +already built in. \end{abstract}