--- a/Paper/Paper.thy Thu Mar 18 23:39:48 2010 +0100
+++ b/Paper/Paper.thy Fri Mar 19 09:40:34 2010 +0100
@@ -16,15 +16,15 @@
text {*
So far, Nominal Isabelle provides a mechanism for constructing
- automatically alpha-equated terms such as
+ alpha-equated terms such as
\begin{center}
$t ::= x \mid t\;t \mid \lambda x. t$
\end{center}
\noindent
- where bound variables have a name.
- For such terms it derives automatically a reasoning
+ where free and bound variables have names.
+ For such terms Nominal Isabelle 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
@@ -33,7 +33,7 @@
used by Pollack for formalisations in the locally-nameless approach to
binding \cite{SatoPollack10}.
- However, Nominal Isabelle fared less well in a formalisation of
+ However, Nominal Isabelle has fared less well in a formalisation of
the algorithm W \cite{UrbanNipkow09}, where types and type-schemes
are of the form
@@ -44,17 +44,17 @@
\end{center}
\noindent
- and the quantification abstracts over a finite (possibly empty) set of type variables.
+ and the quantification binds 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
+ this leads to a rather clumsy formalisation of W. This need of iterating single binders
+ in order to representing multiple binders is also one 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.
+ in the POPLmark challenge \cite{challenge05}, because also there one would like
+ to bind multiple variables at once.
- 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
+ Binding multiple variables in a single abstraction 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
@@ -78,6 +78,7 @@
\end{center}
\noindent
+ where $z$ does not occur freely in the type.
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
@@ -89,13 +90,13 @@
However, the notion of alpha-equivalence that is preserved by vacuous binders is not
alway wanted. For example in terms like
- \begin{center}
- $\LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END$
- \end{center}
+ \begin{equation}\label{one}
+ \LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END
+ \end{equation}
\noindent
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
+ given, but it would be unusual to regard \eqref{one} as alpha-equivalent
with
\begin{center}
@@ -105,29 +106,28 @@
\noindent
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.
+ binders has to agree.
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$
- \end{center}
+ \begin{equation}\label{two}
+ \LET (x, y) = (3, 2) \IN x\,\backslash\,y \END
+ \end{equation}
\noindent
- we want to bind all variables from the pattern (there might be an arbitrary
- 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
+ we want to bind all variables from the pattern inside the body of the
+ $\mathtt{let}$, but we also care about the order of these variables, since
+ we do not want to identify \eqref{two} with
\begin{center}
$\LET (y, x) = (3, 2) \IN x\,\backslash y\,\END$
\end{center}
\noindent
- 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
+ As a result, we provide three general abstraction mechanisms for binding multiple
+ variables and allow the user to chose which one is intended when formalising a
programming language calculus.
By providing these general abstraction mechanisms, however, we have to work around
@@ -149,9 +149,9 @@
\end{center}
\noindent
- 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
+ where the notation $[\_\!\_].\_\!\_$ indicates that a set of variables becomes
+ bound in $s$. In this representation we need 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 for example specifications of $\mathtt{let}$s
as follows
@@ -168,21 +168,22 @@
\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
+ the $\mathtt{let}$. This function can be defined as
\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}.
+ This style of specifying terms and bindings is heavily
+ inspired by the syntax of the Ott-tool \cite{ott-jfp}.
- We will not be able to deal with all specifications that are allowed by
+ 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
- specifiactions a reasoning infrastructure involving concrete,
- \emph{non}-alpha-equated terms. To see the difference, note that working
+ specifiactions a reasoning infrastructure for terms that have names for
+ bound variables, but these terms are 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
@@ -191,25 +192,23 @@
\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.
+ are not just alpha-equal, but actually equal. 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 for this is that the HOL-logic underlying
+ Nominal Isabelle allows us to replace ``equals-by-equals''. In contrast,
+ replacing ``alpha-equals-by-alpha-equals'' requires a lot of extra work.
+
- Although a reasoning infrastructure for alpha-equated terms with names
- is in informal reasoning nearly always taken for granted, establishing
+ Although in informal settings a reasoning infrastructure for alpha-equated
+ terms that have names is 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
+ For every specification we will need to construct a type containing as
+ elements exactly those sets containing alpha-equal 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
+ 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
@@ -271,8 +270,8 @@
logic work are sorted atoms and permutations of atoms. The sorted atoms
represent different kinds of variables, such as term- and type-variables in
Core-Haskell, and it is assumed that there is an infinite supply of atoms
- for each sort. However, in order to simplify the description of our work, we
- shall assume in this paper that there is only a single sort of atoms.
+ for each sort. However, in order to simplify the description, we
+ shall assume in what follows that there is only a single sort of atoms.
Permutations are bijective functions from atoms to atoms that are
the identity everywhere except on a finite number of atoms. There is a
--- a/Paper/document/root.bib Thu Mar 18 23:39:48 2010 +0100
+++ b/Paper/document/root.bib Fri Mar 19 09:40:34 2010 +0100
@@ -1,3 +1,13 @@
+@incollection{UrbanNipkow09,
+ author = {C.~Urban and T.~Nipkow},
+ title = {{N}ominal {V}erification of {A}lgorithm {W}},
+ booktitle={From Semantics to Computer Science. Essays in Honour of Gilles Kahn},
+ editor={G.~Huet and J.-J.~L{\'e}vy and G.~Plotkin},
+ publisher={Cambridge University Press},
+ pages={363--382},
+ year=2009
+}
+
@InProceedings{Homeier05,
author = {P.~Homeier},
title = {{A} {D}esign {S}tructure for {H}igher {O}rder {Q}uotients},