diff -r e842807d8268 -r a33e96e62a2b LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Mon Sep 12 21:48:26 2011 +0200 +++ b/LMCS-Paper/Paper.thy Tue Sep 13 09:30:34 2011 +0200 @@ -463,17 +463,19 @@ the composition of two permutations @{term "\\<^isub>1"} and @{term "\\<^isub>2"} as \mbox{@{term "\\<^isub>1 + \\<^isub>2"}}, and the inverse permutation of @{term "\"} as @{text "- \"}. 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 - given by: + for example permutations acting on atoms, products, lists, permutations, sets, + functions and booleans are given by: \begin{equation}\label{permute} \mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}} \begin{tabular}{@ {}l@ {}} + @{text "\ \ a \ \ a"}\\ @{thm permute_prod.simps[where p="\", no_vars, THEN eq_reflection]}\\[2mm] @{thm permute_list.simps(1)[where p="\", no_vars, THEN eq_reflection]}\\ @{thm permute_list.simps(2)[where p="\", no_vars, THEN eq_reflection]}\\ \end{tabular} & \begin{tabular}{@ {}l@ {}} + @{thm permute_perm_def[where p="\" and q="\'", no_vars, THEN eq_reflection]}\\ @{thm permute_set_eq[where p="\", no_vars, THEN eq_reflection]}\\ @{text "\ \ f \ \x. \ \ (f (- \ \ x))"}\\ @{thm permute_bool_def[where p="\", no_vars, THEN eq_reflection]} @@ -623,11 +625,13 @@ as long as it is finitely supported) and also @{text "\"} does not affect anything in the support of @{text x} (that is @{term "supp x \* \"}). The last fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders - @{text as} in @{text x}, because @{term "\ \ x = x"}. Note that @{term "supp x \* \"} + @{text as} in @{text x}, because @{term "\ \ x = x"}. + + Note that @{term "supp x \* \"} is equivalent with @{term "supp \ \* 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 @@ -707,7 +711,8 @@ 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{}\\ @@ -756,9 +761,9 @@ \begin{equation} \begin{array}{r} - @{term "alpha_abs_set (as, x) (bs, y)"}~~@{text "\"}~~@{term "alpha_set_ex (as, x) equal supp (bs, y)"}\\ - @{term "alpha_abs_res (as, x) (bs, y)"}~~@{text "\"}~~@{term "alpha_res_ex (as, x) equal supp (bs, y)"}\\ - @{term "alpha_abs_lst (as, x) (bs, y)"}~~@{text "\"}~~@{term "alpha_lst_ex (as, x) equal supp (bs, y)"}\\ + @{term "alpha_set_ex (as, x) equal supp (bs, y)"}\smallskip\\ + @{term "alpha_res_ex (as, x) equal supp (bs, y)"}\smallskip\\ + @{term "alpha_lst_ex (as, x) equal supp (bs, y)"}\\ \end{array} \end{equation}\smallskip @@ -768,20 +773,24 @@ the following properties: \begin{lem}\label{alphaeq} - The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_set+}}$ - and $\approx_{\,\textit{abs\_list}}$ are equivalence relations and equivariant. + The relations $\approx_{\,\textit{set}}^{=, \textit{supp}}$, + $\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 "\"} to be @{text "0"}. For symmetry we have - a permutation @{text "\"} and for the proof obligation take @{term "- \"}. In case - of transitivity, we have two permutations @{text "\\<^isub>1"} and @{text "\\<^isub>2"}, and for the - proof obligation use @{text "\\<^isub>1 + \\<^isub>2"}. Equivariance means - @{term "abs_set (\ \ as, \ \ x) (\ \ bs, \ \ y)"} holds provided - \mbox{@{term "abs_set (as, x) (bs, y)"}} holds. To show this, we need to unfold the - definitions and `pull out' the permutations, which is possible since all - operators, such as @{text "#\<^sup>*, -, set"} and @{text "supp"}, are equivariant - (see \cite{HuffmanUrban10}). Finally we apply the permutation operation on booleans. + a permutation @{text "\"} and for the proof obligation take @{term "- + \"}. In case of transitivity, we have two permutations @{text "\\<^isub>1"} + and @{text "\\<^isub>2"}, and for the proof obligation use @{text + "\\<^isub>1 + \\<^isub>2"}. Equivariance means @{term "alpha_set_ex (\ \ as, + \ \ x) equal supp (\ \ bs, \ \ y)"} holds provided \mbox{@{term + "alpha_set_ex (as, x) equal supp(bs, y)"}} holds. To show this, we need to + unfold the definitions and `pull out' the permutations, which is possible + 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 @@ -1080,7 +1089,7 @@ 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{% @@ -1105,7 +1114,7 @@ \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. @@ -1191,8 +1200,8 @@ \end{equation}\smallskip \noindent - In this example the term constructor @{text "ACons'"} has four arguments and - contains a binding clause. This constructor is also used in the definition + In this example the term constructor @{text "ACons'"} has four arguments with + 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 @@ -1274,10 +1283,10 @@ \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 @@ -1562,13 +1571,14 @@ \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+}}$ and $\approx_{\,\textit{list}}$ for the other + $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ given in Section~\ref{sec:binders} (similarly + $\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 \[ @@ -1651,10 +1661,12 @@ \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: @@ -1684,7 +1696,7 @@ \]\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 @@ -1692,6 +1704,9 @@ 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 *} @@ -2371,7 +2386,7 @@ 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 @@ -2401,7 +2416,7 @@ ``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 \ 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.} @@ -2445,11 +2460,11 @@ 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 - related to our binding mode \isacommand{binds (set+)} \cite{Altenkirch10}. + Altenkirch et al \cite{Altenkirch10} present a calculus with a notion of + 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 @@ -2474,8 +2489,7 @@ 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 - \href{http://isabelle.in.tum.de/nominal/download} + can be downloaded from \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