--- 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 *}
--- 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",
--- 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}