# HG changeset patch # User Cezary Kaliszyk # Date 1269020609 -3600 # Node ID 572064152e8a49fb1dac554b3151bad3afc22aa8 # Parent 4355eb3b7161006487b74047fcfbf0947e12733c# Parent d14b8b21bef2d9b09b13be4701b378a681ff4e8c merge diff -r 4355eb3b7161 -r 572064152e8a Paper/Paper.thy --- a/Paper/Paper.thy Fri Mar 19 18:42:57 2010 +0100 +++ b/Paper/Paper.thy Fri Mar 19 18:43:29 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,31 +194,56 @@ \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} - figure - %\begin{pspicture}(0.5,0.0)(8,2.5) + \begin{tikzpicture} + %\draw[step=2mm] (-4,-1) grid (4,1); + + \draw[very thick] (0.7,0.4) circle (4.25mm); + \draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9); + \draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05); + + \draw (-2.0, 0.845) -- (0.7,0.845); + \draw (-2.0,-0.045) -- (0.7,-0.045); + + \draw ( 0.7, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}}; + \draw (-2.4, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}}; + \draw (1.8, 0.48) node[right=-0.1mm] + {\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}}; + \draw (0.9, -0.35) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}}; + \draw (-3.25, 0.55) node {\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}}; + + \draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3); + \draw (-0.95, 0.3) node[above=0mm] {isomorphism}; + + %\rput(3.7,1.75){isomorphism} + \end{tikzpicture} + + %%\begin{pspicture}(0.5,0.0)(8,2.5) %%\showgrid %\psframe[linewidth=0.4mm,framearc=0.2](5,0.0)(7.7,2.5) %\pscircle[linewidth=0.3mm,dimen=middle](6,1.5){0.6} @@ -240,7 +267,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 @@ -250,9 +277,9 @@ inspired by earlier work of Pitts \cite{}. By means of automatic proofs, we establish a reasoning infrastructure for alpha-equated terms, including properties about support, freshness and equality - conditions for alpha-equated terms. We will also derive for these - terms a strong induction principle that has the variable convention - already built in. + conditions for alpha-equated terms. We re also able to derive, at the moment + only manually, for these terms a strong induction principle that + has the variable convention already built in. *} section {* A Short Review of the Nominal Logic Work *} diff -r 4355eb3b7161 -r 572064152e8a Paper/document/root.bib --- a/Paper/document/root.bib Fri Mar 19 18:42:57 2010 +0100 +++ b/Paper/document/root.bib Fri Mar 19 18:43:29 2010 +0100 @@ -11,8 +11,7 @@ @InProceedings{Homeier05, author = {P.~Homeier}, title = {{A} {D}esign {S}tructure for {H}igher {O}rder {Q}uotients}, - booktitle = {Proc.~of the 18th International Conference on Theorem - Proving in Higher Order Logics (TPHOLs)}, + booktitle = {Proc.~of the 18th TPHOLs Conference}, pages = {130--146}, year = {2005}, volume = {3603}, @@ -28,7 +27,7 @@ S.~Sarkar and R.~Strni\v{s}a}, title = {{Ott}: {E}ffective {T}ool {S}upport for the {W}orking {S}emanticist}, - journal = {Journal of Functional Programming}, + journal = {J.~of Functional Programming}, year = {2010}, volume = {20}, number = {1}, @@ -49,7 +48,7 @@ @Unpublished{HuffmanUrban10, author = {B.~Huffman and C.~Urban}, title = {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle}, - note = {To appear at ITP 2010}, + note = {To appear at {\it ITP'10 Conference}}, annote = {http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf}, year = {2010} } @@ -75,8 +74,7 @@ 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)}, + booktitle = {Proc.~of the 18th TPHOLs Conference}, pages = {50--65}, year = {2005}, volume = {3603}, @@ -86,7 +84,7 @@ @Unpublished{SatoPollack10, author = {M.~Sato and R.~Pollack}, title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus}, - note = {To appear in {\it Journal of Symbolic Computation}} + note = {To appear in {\it J.~of Symbolic Computation}} } @article{GabbayPitts02, @@ -112,8 +110,7 @@ @InProceedings{BengtsonParrow07, author = {J.~Bengtson and J.~Parrow}, title = {Formalising the pi-{C}alculus using {N}ominal {L}ogic}, - booktitle = {Proc.~of the 10th International Conference on - Foundations of Software Science and Computation Structures (FOSSACS)}, + booktitle = {Proc.~of the 10th FOSSACS Conference}, year = 2007, pages = {63--77}, series = {LNCS}, @@ -123,8 +120,7 @@ @inproceedings{BengtsonParow09, author = {J.~Bengtson and J.~Parrow}, title = {{P}si-{C}alculi in {I}sabelle}, - booktitle = {Proc of the 22nd Conference on Theorem Proving in - Higher Order Logics (TPHOLs)}, + booktitle = {Proc of the 22nd TPHOLs Conference}, year = 2009, pages = {99--114}, series = {LNCS}, @@ -133,8 +129,7 @@ @inproceedings{TobinHochstadtFelleisen08, author = {S.~Tobin-Hochstadt and M.~Felleisen}, - booktitle = {Proc.~of the 35rd Symposium on - Principles of Programming Languages (POPL)}, + booktitle = {Proc.~of the 35rd POPL Symposium}, title = {{T}he {D}esign and {I}mplementation of {T}yped {S}cheme}, publisher = {ACM}, year = {2008}, @@ -146,14 +141,13 @@ title = "{M}echanizing the {M}etatheory of {LF}", pages = "45--56", year = 2008, - booktitle = "Proc.~of the 23rd IEEE Symposium on Logic in Computer Science (LICS)" + booktitle = "Proc.~of the 23rd LICS Symposium" } @InProceedings{UrbanZhu08, title = "{R}evisiting {C}ut-{E}limination: {O}ne {D}ifficult {P}roof is {R}eally a {P}roof", author = "C.~Urban and B.~Zhu", - booktitle = "Proc.~of the 9th International Conference on Rewriting Techniques - and Applications (RTA)", + booktitle = "Proc.~of the 9th RTA Conference", year = "2008", pages = "409--424", series = "LNCS", diff -r 4355eb3b7161 -r 572064152e8a Paper/document/root.tex --- a/Paper/document/root.tex Fri Mar 19 18:42:57 2010 +0100 +++ b/Paper/document/root.tex Fri Mar 19 18:43:29 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}