# HG changeset patch # User Christian Urban # Date 1271018865 -7200 # Node ID 08e4d3cbcf8c4318b9e74465ff8b44cd17ec88a4 # Parent d7a2c45b447abe75315cafb22293b14319d63e01 folded changes from the conference version diff -r d7a2c45b447a -r 08e4d3cbcf8c Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Sun Apr 11 22:01:56 2010 +0200 +++ b/Pearl-jv/Paper.thy Sun Apr 11 22:47:45 2010 +0200 @@ -214,15 +214,18 @@ simple formalisation of the nominal logic work.\smallskip \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 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 + {\bf Contributions of the paper:} Using a single atom type to represent + atoms of different sorts and representing permutations as functions are not + new ideas. The main contribution of this paper is to show an example of how + to make better theorem proving tools by choosing the right level of + abstraction for the underlying theory---our design choices take advantage of + Isabelle's type system, type classes, and reasoning infrastructure. + The novel + technical contribution is a mechanism for dealing with ``Church-style'' lambda-terms \cite{Church40} and HOL-based languages \cite{PittsHOL4} where variables and variable binding depend on type annotations. + *} section {* Sorted Atoms and Sort-Respecting Permutations *} @@ -338,7 +341,7 @@ are \emph{equal}. We do not have to use the equivalence relation shown in~\eqref{permequ} to identify them, as we would if they had been represented as lists of pairs. Another advantage of the function representation is that - they form an (additive non-commutative) group provided we define + they form a (non-commutative) group provided we define \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}l} @@ -363,9 +366,9 @@ \noindent Again this is in contrast to the list-of-pairs representation which does not - form a group. The technical importance of this fact is that for groups we - can rely on Isabelle/HOL's rich simplification infrastructure. This will - come in handy when we have to do calculations with permutations. + form a group. The technical importance of this fact is that we can rely on + Isabelle/HOL's existing simplification infrastructure for groups, which will + come in handy when we have to do calculations with permutations. Note that Isabelle/HOL defies standard conventions of mathematical notation by using additive syntax even for non-commutative groups. Obviously, composition of permutations is not commutative in general, because @{text @@ -500,11 +503,13 @@ text {* - One huge advantage of using bijective permutation functions (as opposed to - non-bijective renaming substitutions employed in traditional works syntax) is - the property of \emph{equivariance} - and the fact that most HOL-functions (this includes constants) whose argument - and result types are permutation types satisfy this property: + An \emph{equivariant} function or predicate is one that is invariant under + the swapping of atoms. Having a notion of equivariance with nice logical + properties is a major advantage of bijective permutations over traditional + renaming substitutions \cite[\S2]{Pitts03}. Equivariance can be defined + uniformly for all permutation types, and it is satisfied by most HOL + functions and constants. + \begin{definition}\label{equivariance} A function @{text f} is \emph{equivariant} if @{term "\\. \ \ f = f"}. @@ -741,7 +746,7 @@ provided @{thm (prem 1) finite_supp_unique[no_vars]}, @{thm (prem 2) finite_supp_unique[no_vars]}, and for all @{text "a \ S"} and all @{text "b \ S"}, with @{text a} - and @{text b} having the same sort, then \mbox{@{term "(a \ b) \ x \ x"}} + and @{text b} having the same sort, \mbox{@{term "(a \ b) \ x \ x"}} \end{lemma} \begin{proof} @@ -1154,9 +1159,9 @@ 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 - about simple type theory. + Our hope is that with this approach Benzmueller and Paulson can make + headway with formalising their results + about simple type theory \cite{PaulsonBenzmueller}. 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 HOL-based languages. @@ -1201,7 +1206,7 @@ zero to return zero. We noticed only one disadvantage of the permutations-as-functions: Over - lists we can easily perform inductions. For permutation made up from + lists we can easily perform inductions. For permutations made up from functions, we have to manually derive an appropriate induction principle. We can establish such a principle, but we have no real experience yet whether ours is the most useful principle: such an induction principle was not needed in