# HG changeset patch # User Christian Urban # Date 1268951966 -3600 # Node ID d6ee4a1b34ce425055ae4d78da4cb537d773c0d2 # Parent e1c74b864b1bf1f09ec6ac164cf34535f788f022 more tuning on the paper diff -r e1c74b864b1b -r d6ee4a1b34ce Paper/Paper.thy --- a/Paper/Paper.thy Thu Mar 18 23:38:01 2010 +0100 +++ b/Paper/Paper.thy Thu Mar 18 23:39:26 2010 +0100 @@ -23,6 +23,7 @@ \end{center} \noindent + where bound variables have a name. 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 @@ -148,19 +149,79 @@ \end{center} \noindent - where the $[\_\!\_].\_\!\_$ indicates that a list of variables becomes bound - in $s$. In this representation we need additional predicates to ensure + 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 unintelligible reasoning (see for example~\cite{BengtsonParow09}). + To avoid this, we will allow for example specifications of $\mathtt{let}$s + as follows + + \begin{center} + \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l} + $trm$ & $::=$ & \ldots\\ + & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;t\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN t$\\[1mm] + $assn$ & $::=$ & $\mathtt{anil}$\\ + & $\mid$ & $\mathtt{acons}\;\;name\;\;trm\;\;assn$ + \end{tabular} + \end{center} + + \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 + + \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}. + + 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 + with alpha-equated terms means that the two type-schemes with $x$, $y$ and + $z$ being distinct + + \begin{center} + $\forall \{x\}. x \rightarrow y \;=\; \forall \{x, z\}. x \rightarrow y$ + \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. + + Although a reasoning infrastructure for alpha-equated terms with names + is in informal reasoning 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 + 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 + can perform in HOL is illustrated by the following picture: + - - Contributions: We provide definitions for when terms involving general bindings are alpha-equivelent. - %\begin{center} + \begin{center} + figure %\begin{pspicture}(0.5,0.0)(8,2.5) %%\showgrid %\psframe[linewidth=0.4mm,framearc=0.2](5,0.0)(7.7,2.5) @@ -180,9 +241,24 @@ %\rput[c](1.7,1.5){$\lama$} %\rput(3.7,1.75){isomorphism} %\end{pspicture} - %\end{center} + \end{center} + + \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 + re-implementation will automate the proofs we require for our + reasoning infrastructure over alpha-equated terms.\medskip - quotient package \cite{Homeier05} + \noindent + {\bf Contributions:} We provide new definitions for when terms + involving multiple binders are alpha-equivalent. These definitions are + 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. *} section {* A Short Review of the Nominal Logic Work *} @@ -291,10 +367,11 @@ \medskip \noindent - {\bf Acknowledgements:} We are very grateful to Andrew Pitts for the + {\bf Acknowledgements:} We are very grateful to Andrew Pitts for many discussions about Nominal Isabelle. We thank Peter Sewell for making the informal notes \cite{SewellBestiary} available to us and - also for explaining some of the finer points of the OTT-tool. + also for explaining some of the finer points about the abstract + definitions and about the implmentation of the Ott-tool. *} diff -r e1c74b864b1b -r d6ee4a1b34ce Paper/document/root.bib --- a/Paper/document/root.bib Thu Mar 18 23:38:01 2010 +0100 +++ b/Paper/document/root.bib Thu Mar 18 23:39:26 2010 +0100 @@ -9,6 +9,22 @@ series = {LNCS} } +@article{ott-jfp, + author = {P.~Sewell and + F.~Z.~Nardelli and + S.~Owens and + G.~Peskine and + T.~Ridge and + 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}, + year = {2010}, + volume = {20}, + number = {1}, + pages = {70--122} +} + @INPROCEEDINGS{Pottier06, author = {F.~Pottier}, title = {{A}n {O}verview of {C$\alpha$ml}}, diff -r e1c74b864b1b -r d6ee4a1b34ce Paper/document/root.tex --- a/Paper/document/root.tex Thu Mar 18 23:38:01 2010 +0100 +++ b/Paper/document/root.tex Thu Mar 18 23:39:26 2010 +0100 @@ -47,14 +47,15 @@ \begin{abstract} 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 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 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. +programming language calculi involving bound variables that have names (as +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 +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 +variable convention already built in. \end{abstract}