nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:e842807d8268
+:a33e96e62a2b
 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"}},
 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 products, lists, sets, functions and booleans are
+for example permutations acting on atoms, products, lists, permutations, sets,
-given by:
+functions and booleans are given by:
 \begin{equation}\label{permute}
 \mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
 \begin{tabular}{@ {}l@ {}}
+@{text "\<pi> \<bullet> a \<equiv> \<pi> a"}\\
 @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\[2mm]
 @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
 @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
 \end{tabular} &
 \begin{tabular}{@ {}l@ {}}
+@{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", no_vars, THEN eq_reflection]}\\
 @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
 @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f (- \<pi> \<bullet> x))"}\\
 @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}
 \end{tabular}
 \end{tabular}}
 assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text "\<pi>"} such that
 the renamed binders @{term "\<pi> \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen
 as long as it is finitely supported) and also @{text "\<pi>"} does not affect anything
 in the support of @{text x} (that is @{term "supp x \<sharp>* \<pi>"}). The last
 fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders
-@{text as} in @{text x}, because @{term "\<pi> \<bullet> x = x"}. Note that @{term "supp x \<sharp>* \<pi>"}
+@{text as} in @{text x}, because @{term "\<pi> \<bullet> x = x"}.
+Note that @{term "supp x \<sharp>* \<pi>"}
 is equivalent with @{term "supp \<pi> \<sharp>* x"}, which means we could also formulate
 Propositions \ref{supppermeq} and \ref{avoiding} in the other `direction', however the
 reasoning infrastructure of Nominal Isabelle is set up so that it provides more
-automation for the original formulation.
+automation for the formulation given above.
 Most properties given in this section are described in detail in \cite{HuffmanUrban10}
 and all are formalised in Isabelle/HOL. In the next sections we will make
 use of these properties in order to define alpha-equivalence in
 the presence of multiple binders.
 where @{term set} is the function that coerces a list of atoms into a set of atoms.
 Now the last clause ensures that the order of the binders matters (since @{text as}
 and @{text bs} are lists of atoms).
 If we do not want to make any difference between the order of binders \emph{and}
-also allow vacuous binders, that means \emph{restrict} names, then we keep sets of binders, but drop
+also allow vacuous binders, that means according to Pitts \emph{restrict} names
+\cite{Pitts04}, then we keep sets of binders, but drop
 condition {\it (iv)} in Definition~\ref{alphaset}:
 \begin{defi}[Alpha-Equivalence for Set+-Bindings]\label{alphares}\mbox{}\\
 \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}
 @{term "alpha_res_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\<equiv>"} &
 support).  For this we are going to introduce
 three abstraction types that are quotients of the relations
 \begin{equation}
 \begin{array}{r}
-@{term "alpha_abs_set (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_set_ex (as, x) equal supp (bs, y)"}\\
+@{term "alpha_set_ex (as, x) equal supp (bs, y)"}\smallskip\\
-@{term "alpha_abs_res (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_res_ex (as, x) equal supp (bs, y)"}\\
+@{term "alpha_res_ex (as, x) equal supp (bs, y)"}\smallskip\\
-@{term "alpha_abs_lst (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_lst_ex (as, x) equal supp (bs, y)"}\\
+@{term "alpha_lst_ex (as, x) equal supp (bs, y)"}\\
 \end{array}
 \end{equation}\smallskip
 \noindent
 Note that in these relation we replaced the free-atom function @{text "fa"}
 with @{term "supp"} and the relation @{text R} with equality. We can show
 the following properties:
 \begin{lem}\label{alphaeq}
-The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_set+}}$
+The relations $\approx_{\,\textit{set}}^{=, \textit{supp}}$,
-and $\approx_{\,\textit{abs\_list}}$ are equivalence relations and equivariant.
+$\approx_{\,\textit{set+}}^{=, \textit{supp}}$
+and $\approx_{\,\textit{list}}^{=, \textit{supp}}$ are
+equivalence relations and equivariant.
 \end{lem}
 \begin{proof}
 Reflexivity is by taking @{text "\<pi>"} to be @{text "0"}. For symmetry we have
-a permutation @{text "\<pi>"} and for the proof obligation take @{term "- \<pi>"}. In case
+a permutation @{text "\<pi>"} and for the proof obligation take @{term "-
-of transitivity, we have two permutations @{text "\<pi>\<^isub>1"} and @{text "\<pi>\<^isub>2"}, and for the
+\<pi>"}. In case of transitivity, we have two permutations @{text "\<pi>\<^isub>1"}
-proof obligation use @{text "\<pi>\<^isub>1 + \<pi>\<^isub>2"}. Equivariance means
+and @{text "\<pi>\<^isub>2"}, and for the proof obligation use @{text
-@{term "abs_set (\<pi> \<bullet> as, \<pi> \<bullet> x) (\<pi> \<bullet> bs, \<pi> \<bullet> y)"} holds provided
+"\<pi>\<^isub>1 + \<pi>\<^isub>2"}. Equivariance means @{term "alpha_set_ex (\<pi> \<bullet> as,
-\mbox{@{term "abs_set (as, x) (bs, y)"}} holds. To show this, we need to unfold the
+\<pi> \<bullet> x) equal supp (\<pi> \<bullet> bs, \<pi> \<bullet> y)"} holds provided \mbox{@{term
-definitions and `pull out' the permutations, which is possible since all
+"alpha_set_ex (as, x) equal supp(bs, y)"}} holds. To show this, we need to
-operators, such as @{text "#\<^sup>*, -, set"} and @{text "supp"}, are equivariant
+unfold the definitions and `pull out' the permutations, which is possible
-(see \cite{HuffmanUrban10}). Finally we apply the permutation operation on booleans.
+since all operators, such as @{text "#\<^sup>*, -, set"} and @{text "supp"},
+are equivariant (see \cite{HuffmanUrban10}). Finally we apply the
+permutation operation on booleans.
 \end{proof}
 \noindent
 Recall the picture shown in \eqref{picture} about new types in HOL.
 The lemma above allows us to use our quotient package for introducing
 expected to return either a set of atoms (for \isacommand{binds (set)} and
 \isacommand{binds (set+)}) or a list of atoms (for \isacommand{binds}). They need
 to be defined by recursion over the corresponding type; the equations
 must be given in the binding function part of the scheme shown in
 \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with
-tuple patterns might be specified as:
+tuple patterns may be specified as:
 \begin{equation}\label{letpat}
 \mbox{%
 \begin{tabular}{l}
 \isacommand{nominal\_datatype} @{text trm} $=$\\
 \end{tabular}}
 \end{equation}\smallskip
 \noindent
 In this specification the function @{text "bn"} determines which atoms of
-the pattern @{text p} are bound in the argument @{text "t"}. Note that in the
+the pattern @{text p} (fifth line) are bound in the argument @{text "t"}. Note that in the
 second-last @{text bn}-clause the function @{text "atom"} coerces a name
 into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This
 allows us to treat binders of different atom type uniformly.
 For deep binders we allow binding clauses such as
 \hspace{5mm}$\mid$~@{text "bn(ACons' x y t as) = [atom x] @ bn(as)"}\\
 \end{tabular}}
 \end{equation}\smallskip
 \noindent
-In this example the term constructor @{text "ACons'"} has four arguments and
+In this example the term constructor @{text "ACons'"} has four arguments with
-contains a binding clause. This constructor is also used in the definition
+a binding clause for two of them. This constructor is also used in the definition
 of the binding function. The restriction we have to impose is that the
 binding function can only return free atoms, that is the ones that are not
 mentioned in a binding clause.  Therefore @{text "y"} cannot be used in the
 binding function @{text "bn"} (since it is bound in @{text "ACons'"} by the
 binding clause), but @{text x} can (since it is a free atom). This
 \begin{equation}\label{ceqvt}
 @{text "\<pi> \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (\<pi> \<bullet> z\<^isub>1) \<dots> (\<pi> \<bullet> z\<^isub>n)"}
 \end{equation}\smallskip
 The first non-trivial step we have to perform is the generation of
-\emph{free-atom functions} from the specification.\footnote{Admittedly, the
+\emph{free-atom functions} from the specifications.\footnote{Admittedly, the
 details of our definitions will be somewhat involved. However they are still
 conceptually simple in comparison with the ``positional'' approach taken in
-Ott \cite[Pages 88--95]{ott-jfp}, which uses \emph{occurences} and
+Ott \cite[Pages 88--95]{ott-jfp}, which uses the notions of \emph{occurences} and
 \emph{partial equivalence relations} over sets of occurences.} For the
 \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
 \begin{equation}\label{fvars}
 \mbox{@{text "fa_ty"}$_{1..n}$}
 \mbox{\isacommand{binds (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
 \end{equation}\smallskip
 \noindent
 In this case we define a premise @{text P} using the relation
-$\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly
+$\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ given in Section~\ref{sec:binders} (similarly
-$\approx_{\,\textit{set+}}$ and $\approx_{\,\textit{list}}$ for the other
+$\approx_{\,\textit{set+}}^{\textit{R}, \textit{fa}}$ and
+$\approx_{\,\textit{list}}^{\textit{R}, \textit{fa}}$ for the other
 binding modes). This premise defines alpha-equivalence of two abstractions
 involving multiple binders. As above, we first build the tuples @{text "D"} and
 @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding
 compound alpha-relation @{text "R"} (shown in \eqref{rempty}).
-For $\approx_{\,\textit{set}}$  we also need
+For $\approx_{\,\textit{set}}^{R, fa}$  we also need
 a compound free-atom function for the bodies defined as
 \[
 \mbox{@{text "fa \<equiv> (fa_ty\<^isub>1,\<dots>, fa_ty\<^isub>q)"}}
 \]\smallskip
 \]\smallskip
 \noindent
 This completes the definition of alpha-equivalence. As a sanity check, we can show
 that the premises of empty binding clauses are a special case of the clauses for
-non-empty ones (we just have to unfold the definition of $\approx_{\,\textit{set}}$ and take @{text "0"}
+non-empty ones (we just have to unfold the definition of
+$\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ and take @{text "0"}
 for the existentially quantified permutation).
-Again let us take a look at a concrete example for these definitions. For \eqref{letrecs}
+Again let us take a look at a concrete example for these definitions. For
+teh specification given in \eqref{letrecs}
 we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
 $\approx_{\textit{bn}}$ with the following clauses:
 \[\mbox{
 \begin{tabular}{@ {}c @ {}}
 \end{tabular}
 \end{tabular}}
 \]\smallskip
 \noindent
-Note the difference between  $\approx_{\textit{assn}}$ and
+Notice the difference between  $\approx_{\textit{assn}}$ and
 $\approx_{\textit{bn}}$: the latter only ``tracks'' alpha-equivalence of
 the components in an assignment that are \emph{not} bound. This is needed in the
 clause for @{text "Let"} (which has
 a non-recursive binder).
 The underlying reason is that the terms inside an assignment are not meant
 to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"},
 because there all components of an assignment are ``under'' the binder.
+Note also that in case of more than one body (e.g.~@{text "Let_rec"}-case)
+we need to parametrise the relation $\approx_{\textit{list}}$ with compound
+equivalence relations and compund free-atom functions.
 *}
 section {* Establishing the Reasoning Infrastructure *}
 text {*
 any nominal techniques.  To our knowledge there is no concrete mathematical
 result concerning this notion of alpha-equivalence and free variables. We
 have proved that our definitions lead to alpha-equated terms, whose support
 is as expected (that means bound names are removed from the support). We
 also showed that our specifications lift from a raw type to a type of
-alpha-equivalence classes. For this we were able to establish then every
+alpha-equivalence classes. For this we had to establish (automatically) that every
 term-constructor and function is repectful w.r.t.~alpha-equivalence.
 Although we were heavily inspired by the syntax of Ott, its definition of
 alpha-equi\-valence is unsuitable for our extension of Nominal
 Isabelle. First, it is far too complicated to be a basis for automated
 \noindent
 In the first term-constructor we have a single body that happens to be
 ``spread'' over two arguments; in the second term-constructor we have two
 independent bodies in which the same variables are bound. As a result we
 have\footnote{Assuming @{term "a \<noteq> b"}, there is no permutation that can
-make @{text "(a, b)"} equal with @{text "(a, b)"} and @{text "(b, a)"}, but
+make @{text "(a, b)"} equal with both @{text "(a, b)"} and @{text "(b, a)"}, but
 there are two permutations so that we can make @{text "(a, b)"} and @{text
 "(a, b)"} equal with one permutation, and @{text "(a, b)"} and @{text "(b,
 a)"} with the other.}
 alpha-equivalence, which also uses a permutation operation (like ours).
 Still, this definition is rather different from ours and he only proves that
 it defines an equivalence relation. A complete reasoning infrastructure is
 well beyond the purposes of his language. Similar work for Haskell with
 similar results was reported by Cheney \cite{Cheney05a} and more recently
-by ???
+by Weirich et al \cite{WeirichYorgeySheard11}.
 In a slightly different domain (programming with dependent types),
-Altenkirch et al present a calculus with a notion of alpha-equivalence
+Altenkirch et al \cite{Altenkirch10} present a calculus with a notion of
-related to our binding mode \isacommand{binds (set+)} \cite{Altenkirch10}.
+alpha-equivalence related to our binding mode \isacommand{binds (set+)}.
 Their definition is similar to the one by Pottier, except that it has a more
 operational flavour and calculates a partial (renaming) map. In this way,
 the definition can deal with vacuous binders. However, to our best
 knowledge, no concrete mathematical result concerning this definition of
 alpha-equivalence has been proved.
 terms. We also introduced two binding modes (set and set+) that do not exist
 in Ott. We have tried out the extension with calculi such as Core-Haskell,
 type-schemes and approximately a dozen of other typical examples from
 programming language research~\cite{SewellBestiary}. The code will
 eventually become part of the next Isabelle distribution.\footnote{It
-can be downloaded already from the Mercurial repository linked at
+can be downloaded from \href{http://isabelle.in.tum.de/nominal/download}
-\href{http://isabelle.in.tum.de/nominal/download}
 {http://isabelle.in.tum.de/nominal/download}.}
 We have left out a discussion about how functions can be defined over
 alpha-equated terms involving general binders. In earlier versions of Nominal
 Isabelle this turned out to be a thorny issue.  We

changeset 3011	a33e96e62a2b
parent 3010	e842807d8268
child 3012	e2c4ee6e3ee7