nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:89f9d7e85e88
+:8bda1d947df3
 \noindent
 and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of
 type-variables.  While it is possible to implement this kind of more general
 binders by iterating single binders, like @{text "\<forall>x\<^isub>1.\<forall>x\<^isub>2...\<forall>x\<^isub>n.T"}, this leads to a rather clumsy
-formalisation of W. For example, the usual definition when a
+formalisation of W. For example, the usual definition for a
-type is an instance of a type-scheme requires in the iterated version
+type being an instance of a type-scheme requires in the iterated version
-the following auxiliary \emph{unbinding relation}
+the following auxiliary \emph{unbinding relation}:
 \[
 \infer{@{text T} \hookrightarrow ([], @{text T})}{}\qquad
 \infer{\forall @{text x.S} \hookrightarrow (@{text x}\!::\!@{text xs}, @{text T})}
 {@{text S} \hookrightarrow (@{text xs}, @{text T})}
 \]\smallskip
 \noindent
 Its purpose is to relate a type-scheme with a list of type-variables and a type. It is used to
 address the following problem:
-Given a type-scheme @{text S}, how does one get access to the bound type-variables
+Given a type-scheme, say @{text S}, how does one get access to the bound type-variables
-and the type-part of @{text S}? The unbinding relation gives an answer, though in general
+and the type-part of @{text S}? The unbinding relation gives an answer to this problem, though
-we will only get access to some type-variables and some type that are
+in general it will only provide some list of type-variables together with a type that are
 ``alpha-equivalent'' to @{text S}. This is because unbinding is a relation; it cannot be a function
-for alpha-equated type-schemes.
+for alpha-equated type-schemes. With this
-Still, with this
+definition in place we can formally define when a type is an instance of a type-scheme as follows:
-definition in place we can formally define when a type is an instance of a type-scheme
-as follows:
 \[
 @{text "T \<prec> S \<equiv> \<exists>xs T' \<sigma>. S \<hookrightarrow> (xs, T') \<and> dom \<sigma> = set xs \<and> \<sigma>(T') = T"}
 \]\smallskip
 \noindent
 This means there exists a list of type-variables @{text xs} and a type @{text T'} to which
-the type-scheme @{text S} unbinds, and there exists a substitution whose domain is
+the type-scheme @{text S} unbinds, and there exists a substitution @{text "\<sigma>"} whose domain is
 @{text xs} (seen as set) such that @{text "\<sigma>(T') = T"}.
 The problem with this definition is that we cannot follow the usual proofs
 that are by induction on the type-part of the type-scheme (since it is under
 an existential quantifier and only an alpha-variant). The representation of
 type-schemes using iterations of single binders
 prevents us from directly ``unbinding'' the bound type-variables and the type-part.
+Clearly, some more dignified approach to formalising algorithm W is desirable.
 The purpose of this paper is to introduce general binders, which
 allow us to represent type-schemes so that they can bind multiple variables at once
-and as a result solve this problem.
+and as a result solve this problem more straightforwardly.
 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 so far not fared very well with
 the more advanced tasks in the POPLmark challenge \cite{challenge05},
 because also there one would like to bind multiple variables at once.
 two-place permutation operation written
 @{text "_ \<bullet> _ "} and having the type @{text "perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
 where the generic type @{text "\<beta>"} is the type of the object
 over which the permutation
 acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
-the composition of two permutations @{term "\<pi>\<^isub>1"} and @{term "\<pi>\<^isub>2"} as \mbox{@{term "\<pi>\<^isub>1 + \<pi>\<^isub>2"}},
+the composition of two permutations @{term "\<pi>\<^isub>1"} and @{term "\<pi>\<^isub>2"} as \mbox{@{term "\<pi>\<^isub>1 + \<pi>\<^isub>2"}}
+(even if this operation is non-commutative),
 and the inverse permutation of @{term "\<pi>"} as @{text "- \<pi>"}. The permutation
 operation is defined over Isabelle/HOL's type-hierarchy \cite{HuffmanUrban10};
 for example permutations acting on atoms, products, lists, permutations, sets,
 functions and booleans are given by:
 Consequently we exclude specifications such as
 \[\mbox{
 \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
 @{text "Baz\<^isub>1 p::pat t::trm"} &
-\isacommand{binds} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
+\isacommand{binds} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text "p t"}\\
 @{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} &
-\isacommand{binds} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},
+\isacommand{binds} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "p t\<^isub>1"},
-\isacommand{binds} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\
+\isacommand{binds} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "p t\<^isub>2"}\\
 \end{tabular}}
 \]\smallskip
 \noindent
 Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick
 out different atoms to become bound, respectively be free,
-in @{text "p"}.\footnote{Although harmless, in our implementation
+in @{text "p"}.\footnote{Since the Ott-tool does not derive a reasoning
-we exlude such specifications even
-if @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} are the same binding
-functions.}$^,$\footnote{Since the Ott-tool does not derive a reasoning
 infrastructure for
 alpha-equated terms with deep binders, it can permit such specifications.}
 We also need to restrict the form of the binding functions in order to
 empty set or empty list (as in case @{text ANil'}), a singleton set or
 singleton list containing an atom (case @{text PVar} in \eqref{letpat}), or
 unions of atom sets or appended atom lists (case @{text ACons'}). This
 restriction will simplify some automatic definitions and proofs later on.
-In order to simplify our definitions of free atoms and alpha-equivalence,
+To sum up this section, we introduced nominal datatype
-we shall assume specifications
+specifications, which are like standard datatype specifications in
-of term-calculi are implicitly \emph{completed}. By this we mean that
+Isabelle/HOL extended with specifications for binding
-for every argument of a term-constructor that is \emph{not}
+functions. Each constructor argument in our specification can also
-already part of a binding clause given by the user, we add implicitly a special \emph{empty} binding
+have an optional label. These labels are used in the binding clauses
-clause, written \isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
+of a constructor; there can be several binding clauses for each
-of the lambda-terms, the completion produces
+constructor, but bodies of binding clauses can only occur in a
+single one. Binding clauses come in three modes: \isacommand{binds},
+\isacommand{binds (set)} and \isacommand{binds (set+)}.  Binders
+fall into two categories: shallow binders and deep binders. Shallow
+binders can occur in more than one binding clause and only have to
+respect the binding mode (i.e.~be of the right type). Deep binders
+can also occur in more than one binding clause, unless they are
+recursive in which case they can only occur once. Each of the deep
+binders can only have a single binding function.  Binding functions
+are defined by recursion over a nominal datatype.  They can only
+return the empty set, singleton atoms and unions of sets of atoms
+(for binding modes \isacommand{binds (set)} and \isacommand{binds
+(set+)}), and the empty list, singleton atoms and appended lists of
+atoms (for mode \isacommand{bind}). However, they can only return
+atoms that are not mentioned in any binding clause.  In order to
+simplify our definitions of free atoms and alpha-equivalence, we
+shall assume specifications of term-calculi are implicitly
+\emph{completed}. By this we mean that for every argument of a
+term-constructor that is \emph{not} already part of a binding clause
+given by the user, we add implicitly a special \emph{empty} binding
+clause, written \isacommand{binds}~@{term
+"{}"}~\isacommand{in}~@{text "labels"}. In case of the lambda-terms,
+the completion produces
 \[\mbox{
 \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
 \isacommand{nominal\_datatype} @{text lam} =\\
 \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}

changeset 3159	8bda1d947df3
parent 3154	990f066609c9
child 3160	603a36f19bfe