# HG changeset patch # User Christian Urban # Date 1270708849 -7200 # Node ID b7e524e7ee83e37bae7dade063b41f511fe103aa # Parent 4c2e424cb8586680187e63ac5ea963697441c6f7 final version of the pearl paper diff -r 4c2e424cb858 -r b7e524e7ee83 Pearl/Paper.thy --- a/Pearl/Paper.thy Wed Apr 07 22:08:46 2010 +0200 +++ b/Pearl/Paper.thy Thu Apr 08 08:40:49 2010 +0200 @@ -48,7 +48,7 @@ programming languages. It has been used to formalise 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 + \cite{BengtsonParrow07} and a strong normalisation result for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been used by Pollack for formalisations in the locally-nameless approach to binding \cite{SatoPollack10}. @@ -218,7 +218,7 @@ \noindent {\bf Contributions of the paper:} Our use of a single atom type for representing atoms of different sorts and of functions for representing - permutations drastically reduces the number of type classes to just + permutations is not novel, but drastically reduces the number of type classes to just two (permutation types and finitely supported types) that we need in order reason abstractly about properties from the nominal logic work. The novel technical contribution of this paper is a mechanism for dealing with @@ -242,10 +242,11 @@ text {* \noindent - whereby the string argument specifies the sort of the atom. (We use type - \emph{string} merely for convenience; any countably infinite type would work - as well.) A similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09} - for their variables. + whereby the string argument specifies the sort of the atom.\footnote{A similar + design choice was made by Gunter et al \cite{GunterOsbornPopescu09} + for their variables.} (The use type + \emph{string} is merely for convenience; any countably infinite type would work + as well.) We have an auxiliary function @{text sort} that is defined as @{thm sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X} of atoms and every sort @{text s} the property: @@ -367,7 +368,7 @@ come in handy when we have to do calculations with permutations. However, note that in this case Isabelle/HOL neglects well-entrenched mathematical terminology that associates with an additive group a commutative - operation. Obviously, permutations are not commutative in general---@{text + operation. Obviously, permutations are not commutative in general, because @{text "p + q \ q + p"}. However, it is quite difficult to work around this idiosyncrasy of Isabelle/HOL, unless we develop our own algebraic hierarchy and infrastructure. But since the point of this paper is to implement the @@ -813,11 +814,7 @@ fresh atom with arbitrary sort. This is an important operation in Nominal Isabelle in situations where, for example, a bound variable needs to be renamed. To allow such a choice, we only have to assume \emph{one} premise - of the form - - @{text [display,indent=10] "finite (supp x)"} - - \noindent + of the form @{text "finite (supp x)"} for each @{text x}. Compare that with the sequence of premises in our earlier version of Nominal Isabelle (see~\eqref{fssequence}). For more convenience we can define a type class for types where every element has finite support, and @@ -926,7 +923,7 @@ defines an overloaded function that maps from the concrete type into the generic atom type, which we will write @{text "|_|"}. For each class instance, this function must be injective and equivariant, and its outputs - must all have the same sort. + must all have the same sort, that is \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% i) \hspace{1mm}if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\hspace{4mm} @@ -1153,8 +1150,8 @@ user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"} where the argument, or arguments, are datatypes for which we can automatically define an injective function like @{text "sort_ty"} (see \eqref{sortty}). - Our hope is that with this approach Benzmueller and Paulson the authors of - \cite{PaulsonBenzmueller} can make headway with formalising their results + Our hope is that with this approach Benzmueller and Paulson, the authors of + \cite{PaulsonBenzmueller}, can make headway with formalising their results about simple type theory. Because of its limitations, they did not attempt this with the old version of Nominal Isabelle. We also hope we can make progress with formalisations of diff -r 4c2e424cb858 -r b7e524e7ee83 Pearl/document/root.bib --- a/Pearl/document/root.bib Wed Apr 07 22:08:46 2010 +0200 +++ b/Pearl/document/root.bib Thu Apr 08 08:40:49 2010 +0200 @@ -17,8 +17,8 @@ @article{GabbayPitts02, author = {M.~J.~Gabbay and A.~M.~Pitts}, - title = {A New Approach to Abstract Syntax with Variable - Binding}, + title = {{A} {N}ew {A}pproach to {A}bstract {S}yntax with {V}ariable + {B}inding}, journal = {Formal Aspects of Computing}, volume = {13}, year = 2002, @@ -27,8 +27,8 @@ @article{Pitts03, author = {A.~M.~Pitts}, - title = {Nominal Logic, A First Order Theory of Names and - Binding}, + title = {{N}ominal {L}ogic, {A} {F}irst {O}rder {T}heory of {N}ames and + {B}inding}, journal = {Information and Computation}, year = {2003}, volume = {183}, @@ -125,7 +125,7 @@ @Article{Cheney06, author = {J.~Cheney}, - title = {{C}ompleteness and {H}erbrand theorems for {N}ominal {L}ogic}, + title = {{C}ompleteness and {H}erbrand {T}heorems for {N}ominal {L}ogic}, journal = {Journal of Symbolic Logic}, year = {2006}, volume = {71},