--- a/Paper/Paper.thy Fri Mar 19 12:31:55 2010 +0100
+++ b/Paper/Paper.thy Fri Mar 19 15:43:43 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,26 +194,29 @@
\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}
@@ -240,7 +245,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