# HG changeset patch # User Christian Urban # Date 1269336252 -3600 # Node ID ac69ed8303cce4aab7b7069b15709ee772619856 # Parent e33e37fd4c7ddb7a3a1b5c34f0cfd0784495f7da tuned paper diff -r e33e37fd4c7d -r ac69ed8303cc Paper/Paper.thy --- a/Paper/Paper.thy Tue Mar 23 09:05:23 2010 +0100 +++ b/Paper/Paper.thy Tue Mar 23 10:24:12 2010 +0100 @@ -16,7 +16,7 @@ text {* So far, Nominal Isabelle provides a mechanism for constructing - alpha-equated terms such as + alpha-equated terms, for example \begin{center} $t ::= x \mid t\;t \mid \lambda x. t$ @@ -24,7 +24,7 @@ \noindent where free and bound variables have names. For such terms Nominal Isabelle - derives automatically a reasoning infrastructure, which has been used + derives automatically a reasoning infrastructure that has been used successfully in formalisations of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency @@ -83,7 +83,7 @@ In this paper we will give a general binding mechanism and associated notion of alpha-equivalence that can be used to faithfully represent this kind of binding in Nominal Isabelle. The difficulty of finding the right notion - for alpha-equivalence in this case can be appreciated by considering that the + for alpha-equivalence can be appreciated in this case 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 @@ -178,7 +178,7 @@ 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 to bind in $s$ all the names the - function $bn\,(a)$ returns. This style of specifying terms and bindings is + function call $bn\,(a)$ returns. 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 @@ -191,8 +191,8 @@ \noindent where no clause for variables is given. Such specifications make some sense in - the context of Coq's type theory (which Ott supports), but not at al in a HOL-based - theorem prover where every datatype must have a non-empty set-theoretic model. + the context of Coq's type theory (which Ott supports), but not at all in a HOL-based + environment where every datatype must have a non-empty set-theoretic model. Another reason is that we establish the reasoning infrastructure for alpha-\emph{equated} terms. In contrast, Ott produces a reasoning @@ -221,13 +221,13 @@ 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 + terms is nearly always taken for granted, establishing 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. The construction we - perform in HOL is illustrated by the following picture: + perform in HOL can be illustrated by the following picture: \begin{center} \begin{tikzpicture} @@ -256,25 +256,26 @@ \noindent We take as the starting point a definition of raw terms (defined as a datatype in Isabelle/HOL); identify then the - alpha-equivalence classes in the type of sets of raw terms, according to our + alpha-equivalence classes in the type of sets of raw terms according to our alpha-equivalence relation and finally define the new type as these alpha-equivalence classes (non-emptiness is satisfied whenever the raw terms are - definable as datatype in Isabelle/HOL and the fact that our relation for alpha is an - equivalence relation). + definable as datatype in Isabelle/HOL and the fact that our relation for + alpha-equivalence is indeed an equivalence relation). - The fact that we obtain an isomorphism between between the new type and the non-empty + The fact that we obtain an isomorphism between the new type and the non-empty subset shows that the new type is a faithful representation of alpha-equated terms. That is not the case for example in the representation of terms using the locally - nameless representation of binders \cite{McKinnaPollack99}: there are ``junk'' terms that need to + nameless representation of binders \cite{McKinnaPollack99}: in this representation + there are ``junk'' terms that need to be excluded by reasoning about a well-formedness predicate. The problem with introducing a new type in Isabelle/HOL is that in order to be useful, a reasoning infrastructure needs to be ``lifted'' from the underlying subset to - the new type. This is usually a tricky and arduous task. To ease it + the new type. This is usually a tricky and arduous task. To ease it, we re-implemented in Isabelle/HOL the quotient package described by Homeier \cite{Homeier05}. This package allows us to lift definitions and theorems involving raw terms - to definitions and theorems involving alpha-equated terms. For example + to definitions and theorems involving alpha-equated, terms. For example if we define the free-variable function over lambda terms \begin{center} @@ -296,23 +297,25 @@ \noindent (Note that this means also the term-constructors for variables, applications and lambda are lifted to the quotient level.) This construction, of course, - only works if alpha is an equivalence relation, and the definitions and theorems - are respectful w.r.t.~alpha-equivalence. Hence we will not be able to lift this - a bound-variable function to alpha-equated terms (since it does not respect - alpha-equivalence). To sum up, every lifting needs proofs of some respectfulness - properties. These proofs we are able automate and therefore establish a - useful reasoning infrastructure for alpha-equated lambda terms.\medskip + only works if alpha-equivalence is an equivalence relation, and the + definitions and theorems are respectful w.r.t.~alpha-equivalence. Hence we + will not be able to lift a bound-variable function to alpha-equated terms + (since it does not respect alpha-equivalence). To sum up, every lifting of + theorems to the quotient level needs proofs of some respectfulness + properties. In the paper we show that we are able to automate these + proofs and therefore can establish a reasoning infrastructure for + alpha-equated terms.\medskip \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 + inspired by earlier work of Pitts \cite{Pitts04}. 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 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. + conditions for alpha-equated terms. We are also able to derive, at the moment + only manually, strong induction principles that + have the variable convention already built in. *} section {* A Short Review of the Nominal Logic Work *} @@ -525,10 +528,10 @@ \begin{center} \begin{tabular}{l} - \isacommand{nominal\_datatype} $ty_1 =$\\ - \isacommand{and} $ty_2 =$\\ + \isacommand{nominal\_datatype} $ty_{\alpha{}1} =$\\ + \isacommand{and} $ty_{\alpha{}2} =$\\ $\ldots$\\ - \isacommand{and} $ty_n =$\\ + \isacommand{and} $ty_{\alpha{}}n =$\\ $\ldots$\\ \isacommand{with}\\ $\ldots$\\ diff -r e33e37fd4c7d -r ac69ed8303cc Paper/document/root.bib --- a/Paper/document/root.bib Tue Mar 23 09:05:23 2010 +0100 +++ b/Paper/document/root.bib Tue Mar 23 10:24:12 2010 +0100 @@ -1,3 +1,11 @@ + +@Unpublished{Pitts04, + author = {Andrew Pitts}, + title = {{N}otes on the {R}estriction {M}onad for {N}ominal {S}ets and {C}pos}, + note = {bla}, + year = {2004} +} + @incollection{UrbanNipkow09, author = {C.~Urban and T.~Nipkow}, title = {{N}ominal {V}erification of {A}lgorithm {W}}, diff -r e33e37fd4c7d -r ac69ed8303cc Paper/document/root.tex --- a/Paper/document/root.tex Tue Mar 23 09:05:23 2010 +0100 +++ b/Paper/document/root.tex Tue Mar 23 10:24:12 2010 +0100 @@ -8,6 +8,7 @@ \usepackage{pgf} \usepackage{pdfsetup} \usepackage{ot1patch} +\usepackage{times} \urlstyle{rm} \isabellestyle{it} @@ -50,7 +51,7 @@ \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 involving bound variables that have names (as +programming language calculi involving named bound variables (as opposed to de-Bruijn indices). In this paper we present an extension of Nominal Isabelle for dealing with general bindings, that means term-constructors where multiple variables are bound at once. Such binding