# HG changeset patch # User Christian Urban # Date 1315856906 -7200 # Node ID e842807d8268e0ac37155e88c8986a8ba5aec5cf # Parent 41c1e98c686f9e581bc65f3422b4b916e791b764 more on the paper diff -r 41c1e98c686f -r e842807d8268 LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Sun Sep 11 18:04:29 2011 +0100 +++ b/LMCS-Paper/Paper.thy Mon Sep 12 21:48:26 2011 +0200 @@ -664,7 +664,7 @@ {\it (iii)} ``moves'' their bound names so that we obtain modulo a relation, say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)} @{text \} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The - requirements {\it (i)} to {\it (iv)} can be stated formally as the conjunction of: + requirements {\it (i)} to {\it (iv)} can be stated formally as: \begin{defi}[Alpha-Equivalence for Set-Bindings]\label{alphaset}\mbox{}\\ \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl} @@ -899,6 +899,19 @@ Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes the first equation of Theorem~\ref{suppabs}. + Recall the definition of support \eqref{suppdef}, and note the difference between + the support of a ``raw'' pair and an abstraction + + \[ + @{term "supp (as, x) = supp as \ supp x"}\hspace{15mm} + @{term "supp (Abs_set as x) = supp x - as"} + \]\smallskip + + \noindent + While the permutation operations behave in both cases the same (the permutation + is just moved to the arguments), the notion of equality is different for pairs and + abstractions. Therefore we have different supports. + The method of first considering abstractions of the form @{term "Abs_set as x"} etc is motivated by the fact that we can conveniently establish at the Isabelle/HOL level properties about them. It would be extremely laborious @@ -1022,25 +1035,27 @@ Shallow binders are just labels. The restriction we need to impose on them is that in case of \isacommand{binds (set)} and \isacommand{binds (set+)} the labels must either refer to atom types or to sets of atom types; in case of - \isacommand{binds} the labels must refer to atom types or lists of atom + \isacommand{binds} the labels must refer to atom types or to lists of atom types. Two examples for the use of shallow binders are the specification of lambda-terms, where a single name is bound, and type-schemes, where a finite set of names is bound: \[\mbox{ - \begin{tabular}{@ {}c@ {\hspace{5mm}}c@ {}} + \begin{tabular}{@ {}c@ {\hspace{8mm}}c@ {}} \begin{tabular}{@ {}l} \isacommand{nominal\_datatype} @{text lam} $=$\\ \hspace{2mm}\phantom{$\mid$}~@{text "Var name"}\\ \hspace{2mm}$\mid$~@{text "App lam lam"}\\ \hspace{2mm}$\mid$~@{text "Lam x::name t::lam"}\hspace{3mm}% \isacommand{binds} @{text x} \isacommand{in} @{text t}\\ + \\ \end{tabular} & \begin{tabular}{@ {}l@ {}} \isacommand{nominal\_datatype}~@{text ty} $=$\\ - \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\ - \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\ - \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\hspace{3mm}% + \hspace{2mm}\phantom{$\mid$}~@{text "TVar name"}\\ + \hspace{2mm}$\mid$~@{text "TFun ty ty"}\\ + \isacommand{and}~@{text "tsc ="}\\ + \hspace{2mm}\phantom{$\mid$}~@{text "TAll xs::(name fset) T::ty"}\hspace{3mm}% \isacommand{binds (set+)} @{text xs} \isacommand{in} @{text T}\\ \end{tabular} \end{tabular}} @@ -1176,16 +1191,16 @@ \end{equation}\smallskip \noindent - In this example the term constructor @{text "ACons'"} contains a binding - clause, and also is 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 restriction is sufficient for lifting - the binding function to alpha-equated terms. If we would permit that @{text "bn"} - can also return @{text "y"}, then it would not be respectful and therefore - cannot be lifted. + In this example the term constructor @{text "ACons'"} has four arguments and + contains a binding clause. 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 + restriction is sufficient for lifting the binding function to alpha-equated + terms. If we would permit that @{text "bn"} can also return @{text "y"}, + then it would not be respectful and therefore cannot be lifted. In the version of Nominal Isabelle described here, we also adopted the restriction from the Ott-tool that binding functions can only return: the @@ -1499,7 +1514,7 @@ \noindent The task below is to specify what the premises corresponding to a binding - clause are. To understand better whet the general pattern is, let us first + clause are. To understand better what the general pattern is, let us first treat the special instance where @{text "bc\<^isub>i"} is the empty binding clause of the form @@ -1508,27 +1523,33 @@ \]\smallskip \noindent - In this binding clause no atom is bound and we only have to `alpha-relate' the bodies. For this - we build first the tuples @{text "D \ (d\<^isub>1,\, d\<^isub>q)"} and @{text "D' \ (d\\<^isub>1,\, d\\<^isub>q)"} - whereby the labels @{text "d"}$_{1..q}$ refer to arguments @{text "z"}$_{1..n}$ and - respectively @{text "d\"}$_{1..q}$ to @{text "z\"}$_{1..n}$. In order to relate - two such tuples we define the compound alpha-equivalence relation @{text "R"} as follows - + In this binding clause no atom is bound and we only have to `alpha-relate' + the bodies. For this we build first the tuples @{text "D \ (d\<^isub>1,\, + d\<^isub>q)"} and @{text "D' \ (d\\<^isub>1,\, d\\<^isub>q)"} + whereby the labels @{text "d"}$_{1..q}$ refer to the arguments @{text + "z"}$_{1..n}$ and respectively @{text "d\"}$_{1..q}$ to @{text + "z\"}$_{1..n}$ of the term-constructor. In order to relate two such + tuples we define the compound alpha-equivalence relation @{text "R"} as + follows + \begin{equation}\label{rempty} \mbox{@{text "R \ (R\<^isub>1,\, R\<^isub>q)"}} - \end{equation} + \end{equation}\smallskip \noindent - with @{text "R\<^isub>i"} being @{text "\ty\<^isub>i"} if the corresponding labels @{text "d\<^isub>i"} and - @{text "d\\<^isub>i"} refer - to a recursive argument of @{text C} with type @{text "ty\<^isub>i"}; otherwise - we take @{text "R\<^isub>i"} to be the equality @{text "="}. This lets us define - the premise for an empty binding clause succinctly as @{text "prems(bc\<^isub>i) \ D R D'"}, - which can be unfolded to the series of premises + with @{text "R\<^isub>i"} being @{text "\ty\<^isub>i"} if the corresponding + labels @{text "d\<^isub>i"} and @{text "d\\<^isub>i"} refer to a + recursive argument of @{text C} with type @{text "ty\<^isub>i"}; otherwise + we take @{text "R\<^isub>i"} to be the equality @{text "="}. Again the + latter is because @{text "ty\<^isub>i"} is not part of the specified types + and alpha-equivalence of any previously defined type is supposed to coincide + with equality. This lets us now define the premise for an empty binding + clause succinctly as @{text "prems(bc\<^isub>i) \ D R D'"}, which can be + unfolded to the series of premises - \begin{center} + \[ @{text "d\<^isub>1 R\<^isub>1 d\\<^isub>1 \ d\<^isub>q R\<^isub>q d\\<^isub>q"}. - \end{center} + \]\smallskip \noindent We will use the unfolded version in the examples below. @@ -1537,7 +1558,7 @@ \begin{equation}\label{nonempty} \mbox{\isacommand{binds (set)} @{text "b\<^isub>1\b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}.} - \end{equation} + \end{equation}\smallskip \noindent In this case we define a premise @{text P} using the relation @@ -1550,83 +1571,82 @@ For $\approx_{\,\textit{set}}$ we also need a compound free-atom function for the bodies defined as - \begin{center} + \[ \mbox{@{text "fa \ (fa_ty\<^isub>1,\, fa_ty\<^isub>q)"}} - \end{center} + \]\smallskip \noindent with the assumption that the @{text "d"}$_{1..q}$ refer to arguments of types @{text "ty"}$_{1..q}$. The last ingredient we need are the sets of atoms bound in the bodies. For this we take - \begin{center} + \[ @{text "B \ bn_ty\<^isub>1 b\<^isub>1 \ \ \ bn_ty\<^isub>p b\<^isub>p"}\;.\\ - \end{center} + \]\smallskip \noindent Similarly for @{text "B'"} using the labels @{text "b\"}$_{1..p}$. This lets us formally define the premise @{text P} for a non-empty binding clause as: - \begin{center} + \[ \mbox{@{term "P \ alpha_set_ex (B, D) R fa (B', D')"}}\;. - \end{center} + \]\smallskip \noindent This premise accounts for alpha-equivalence of the bodies of the binding - clause. - However, in case the binders have non-recursive deep binders, this premise - is not enough: - we also have to ``propagate'' alpha-equivalence inside the structure of - these binders. An example is @{text "Let"} where we have to make sure the - right-hand sides of assignments are alpha-equivalent. For this we use - relations @{text "\bn"}$_{1..m}$ (which we will formally define shortly). - Let us assume the non-recursive deep binders in @{text "bc\<^isub>i"} are + clause. However, in case the binders have non-recursive deep binders, this + premise is not enough: we also have to ``propagate'' alpha-equivalence + inside the structure of these binders. An example is @{text "Let"} where we + have to make sure the right-hand sides of assignments are + alpha-equivalent. For this we use relations @{text "\bn"}$_{1..m}$ (which we + will formally define shortly). Let us assume the non-recursive deep binders + in @{text "bc\<^isub>i"} are - \begin{center} + \[ @{text "bn\<^isub>1 l\<^isub>1, \, bn\<^isub>r l\<^isub>r"}. - \end{center} + \]\smallskip \noindent - The tuple @{text L} is then @{text "(l\<^isub>1,\,l\<^isub>r)"} (similarly @{text "L'"}) - and the compound equivalence relation @{text "R'"} is @{text "(\bn\<^isub>1,\,\bn\<^isub>r)"}. - All premises for @{text "bc\<^isub>i"} are then given by + The tuple @{text L} consists then of all these binders @{text "(l\<^isub>1,\,l\<^isub>r)"} + (similarly @{text "L'"}) and the compound equivalence relation @{text "R'"} + is @{text "(\bn\<^isub>1,\,\bn\<^isub>r)"}. All premises for @{text "bc\<^isub>i"} are then given by - \begin{center} + \[ @{text "prems(bc\<^isub>i) \ P \ L R' L'"} - \end{center} + \]\smallskip \noindent The auxiliary alpha-equivalence relations @{text "\bn"}$_{1..m}$ in @{text "R'"} are defined as follows: assuming a @{text bn}-clause is of the form - \begin{center} + \[ @{text "bn (C z\<^isub>1 \ z\<^isub>s) = rhs"} - \end{center} + \]\smallskip \noindent where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$, then the corresponding alpha-equivalence clause for @{text "\bn"} has the form - \begin{center} + \[ \mbox{\infer{@{text "C z\<^isub>1 \ z\<^isub>s \bn C z\\<^isub>1 \ z\\<^isub>s"}} {@{text "z\<^isub>1 R\<^isub>1 z\\<^isub>1 \ z\<^isub>s R\<^isub>s z\\<^isub>s"}}} - \end{center} + \]\smallskip \noindent In this clause the relations @{text "R"}$_{1..s}$ are given by - \begin{center} + \[\mbox{ \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}} $\bullet$ & @{text "z\<^isub>i \ty z\\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs} and - is a recursive argument of @{text C},\\ + is a recursive argument of @{text C},\smallskip\\ $\bullet$ & @{text "z\<^isub>i = z\\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs} - and is a non-recursive argument of @{text C},\\ + and is a non-recursive argument of @{text C},\smallskip\\ $\bullet$ & @{text "z\<^isub>i \bn\<^isub>i z\\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text rhs} - with the recursive call @{text "bn\<^isub>i x\<^isub>i"} and\\ + with the recursive call @{text "bn\<^isub>i x\<^isub>i"} and\smallskip\\ $\bullet$ & @{text True} provided @{text "z\<^isub>i"} occurs in @{text rhs} but without a recursive call. - \end{tabular} - \end{center} + \end{tabular}} + \]\smallskip \noindent This completes the definition of alpha-equivalence. As a sanity check, we can show @@ -1638,30 +1658,30 @@ we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and $\approx_{\textit{bn}}$ with the following clauses: - \begin{center} + \[\mbox{ \begin{tabular}{@ {}c @ {}} \infer{@{text "Let as t \\<^bsub>trm\<^esub> Let as' t'"}} - {@{term "alpha_lst_ex (bn as, t) alpha_trm fa_trm (bn as', t')"} & @{text "as \\<^bsub>bn\<^esub> as'"}}\smallskip\\ + {@{term "alpha_lst_ex (bn as, t) alpha_trm fa_trm (bn as', t')"} & + \hspace{5mm}@{text "as \\<^bsub>bn\<^esub> as'"}}\\ + \\ \makebox[0mm]{\infer{@{text "Let_rec as t \\<^bsub>trm\<^esub> Let_rec as' t'"}} - {@{term "alpha_lst_ex (bn as, ast) alpha_trm2 fa_trm2 (bn as', ast')"}}} - \end{tabular} - \end{center} + {@{term "alpha_lst_ex (bn as, ast) alpha_trm2 fa_trm2 (bn as', ast')"}}}\\ + \\ - \begin{center} \begin{tabular}{@ {}c @ {}} \infer{@{text "ANil \\<^bsub>assn\<^esub> ANil"}}{}\hspace{9mm} \infer{@{text "ACons a t as \\<^bsub>assn\<^esub> ACons a' t' as"}} - {@{text "a = a'"} & @{text "t \\<^bsub>trm\<^esub> t'"} & @{text "as \\<^bsub>assn\<^esub> as'"}} - \end{tabular} - \end{center} + {@{text "a = a'"} & \hspace{5mm}@{text "t \\<^bsub>trm\<^esub> t'"} & \hspace{5mm}@{text "as \\<^bsub>assn\<^esub> as'"}} + \end{tabular}\\ + \\ - \begin{center} \begin{tabular}{@ {}c @ {}} \infer{@{text "ANil \\<^bsub>bn\<^esub> ANil"}}{}\hspace{9mm} \infer{@{text "ACons a t as \\<^bsub>bn\<^esub> ACons a' t' as"}} - {@{text "t \\<^bsub>trm\<^esub> t'"} & @{text "as \\<^bsub>bn\<^esub> as'"}} + {@{text "t \\<^bsub>trm\<^esub> t'"} & \hspace{5mm}@{text "as \\<^bsub>bn\<^esub> as'"}} \end{tabular} - \end{center} + \end{tabular}} + \]\smallskip \noindent Note the difference between $\approx_{\textit{assn}}$ and @@ -1677,37 +1697,81 @@ section {* Establishing the Reasoning Infrastructure *} text {* - Having made all necessary definitions for raw terms, we can start - with establishing the reasoning infrastructure for the alpha-equated types - @{text "ty\"}$_{1..n}$, that is the types the user originally specified. We sketch - in this section the proofs we need for establishing this infrastructure. One - main point of our work is that we have completely automated these proofs in Isabelle/HOL. + Having made all necessary definitions for raw terms, we can start with + establishing the reasoning infrastructure for the alpha-equated types @{text + "ty\"}$_{1..n}$, that is the types the user originally specified. We + give in this section and the next the proofs we need for establishing this + infrastructure. One main point of our work is that we have completely + automated these proofs in Isabelle/HOL. + + First we establish that the free-variable functions, the binding functions and the + alpha-equivalences are equivariant. - First we establish that the - alpha-equivalence relations defined in the previous section are - equivalence relations. + \begin{lem}\mbox{}\\ + @{text "(i)"} The functions @{text "fa_ty"}$_{1..n}$, @{text "fa_bn"}$_{1..m}$ and + @{text "bn"}$_{1..m}$ are equivariant.\\ + @{text "(ii)"} The relations @{text "\ty"}$_{1..n}$ and + @{text "\bn"}$_{1..m}$ are equivariant. + \end{lem} + + \begin{proof} + The function package of Isabelle/HOL allows us to prove the first part is by mutual + induction over the definitions of the functions. The second is by a straightforward + induction over the rules of @{text "\ty"}$_{1..n}$ and @{text "\bn"}$_{1..m}$ using + the first part. + \end{proof} + + \noindent + Next we establish that the alpha-equivalence relations defined in the + previous section are equivalence relations. \begin{lem}\label{equiv} - Given the raw types @{text "ty"}$_{1..n}$ and binding functions - @{text "bn"}$_{1..m}$, the relations @{text "\ty"}$_{1..n}$ and - @{text "\bn"}$_{1..m}$ are equivalence relations. and equivariant. + The relations @{text "\ty"}$_{1..n}$ and @{text "\bn"}$_{1..m}$ are + equivalence relations. \end{lem} \begin{proof} The proof is by mutual induction over the definitions. The non-trivial cases involve premises built up by $\approx_{\textit{set}}$, $\approx_{\textit{set+}}$ and $\approx_{\textit{list}}$. They - can be dealt with as in Lemma~\ref{alphaeq}. + can be dealt with as in Lemma~\ref{alphaeq}. However, the transitivity + case needs in addition the fact that the relations are equivariant. \end{proof} \noindent We can feed this lemma into our quotient package and obtain new types @{text "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types @{text "ty"}$_{1..n}$. + We also obtain definitions for the term-constructors @{text - "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text - "C"}$_{1..k}$, and similar definitions for the free-atom functions @{text - "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the binding functions @{text - "bn"}$^\alpha_{1..m}$. However, these definitions are not really useful to the + "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text "C"}$_{1..k}$, + and similar definitions for the free-atom functions @{text + "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the + binding functions @{text "bn"}$^\alpha_{1..m}$. For this we have to show + by induction over the definitions of alpha-equivalences that the ``raw'' + functions are respectful. This means we need to establish that + + \[\mbox{ + \begin{tabular}{lll} + @{text "x \ty\<^isub>i x'"} & implies & @{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x'"}\\ + @{text "x \ty\<^isub>l x'"} & implies & @{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x'"}\\ + @{text "x \ty\<^isub>l x'"} & implies & @{text "bn\<^isub>j x = bn\<^isub>j x'"}\\ + \end{tabular} + }\]\smallskip + + \noindent + holds whereby @{text "ty\<^isub>l"} is the type over which @{text "bn\<^isub>j"} is defined. A + similar property is needed for the constructors @{text "C"}$_{1..k}$. In order + to establish it we need to prove that + + \[\mbox{ + \begin{tabular}{lll} + @{text "x \ty\<^isub>l x'"} & implies & @{text "x \bn\<^isub>j x'"}\\ + \end{tabular} + }\]\smallskip + + \noindent + The respectfulness properties are crucial, ... ??? + However, these definitions are not really useful to the user, since they are given in terms of the isomorphisms we obtained by creating new types in Isabelle/HOL (recall the picture shown in the Introduction). @@ -1716,19 +1780,19 @@ term-constructors are not equal, that is - \begin{equation}\label{distinctalpha} + \[\label{distinctalpha} \mbox{@{text "C"}$^\alpha$~@{text "x\<^isub>1 \ x\<^isub>r"}~@{text "\"}~% @{text "D"}$^\alpha$~@{text "y\<^isub>1 \ y\<^isub>s"}} - \end{equation} + \]\smallskip \noindent whenever @{text "C"}$^\alpha$~@{text "\"}~@{text "D"}$^\alpha$. In order to derive this fact, we use the definition of alpha-equivalence and establish that - \begin{equation}\label{distinctraw} + \[\label{distinctraw} \mbox{@{text "C x\<^isub>1 \ x\<^isub>r"}\;$\not\approx$@{text ty}\;@{text "D y\<^isub>1 \ y\<^isub>s"}} - \end{equation} + \]\smallskip \noindent holds for the corresponding raw term-constructors. @@ -1774,20 +1838,20 @@ Having established respectfulness for the raw term-constructors, the quotient package is able to automatically deduce \eqref{distinctalpha} from - \eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can + \eqref{distinctraw}. ??? Having the facts \eqref{fnresp} at our disposal, we can also lift properties that characterise when two raw terms of the form - % - \begin{center} - @{text "C x\<^isub>1 \ x\<^isub>r \ty C x\\<^isub>1 \ x\\<^isub>r"} - \end{center} + + \[ + \mbox{@{text "C x\<^isub>1 \ x\<^isub>r \ty C x\\<^isub>1 \ x\\<^isub>r"}} + \]\smallskip \noindent are alpha-equivalent. This gives us conditions when the corresponding alpha-equated terms are \emph{equal}, namely - \begin{center} + \[ @{text "C\<^sup>\ x\<^isub>1 \ x\<^isub>r = C\<^sup>\ x\\<^isub>1 \ x\\<^isub>r"}. - \end{center} + \]\smallskip \noindent We call these conditions as \emph{quasi-injectivity}. They correspond to @@ -1803,8 +1867,8 @@ As a result we can add the equations \begin{equation}\label{calphaeqvt} - @{text "p \ (C\<^sup>\ x\<^isub>1 \ x\<^isub>r) = C\<^sup>\ (p \ x\<^isub>1) \ (p \ x\<^isub>r)"} - \end{equation} + @{text "\ \ (C\<^sup>\ x\<^isub>1 \ x\<^isub>r) = C\<^sup>\ (\ \ x\<^isub>1) \ (\ \ x\<^isub>r)"} + \end{equation}\smallskip \noindent to our infrastructure. In a similar fashion we can lift the defining equations @@ -1821,7 +1885,7 @@ \begin{equation}\label{weakinduct} \mbox{@{text "P\<^isub>1 x\<^isub>1 \ \ \ P\<^isub>n x\<^isub>n "}} - \end{equation} + \end{equation} \smallskip \noindent whereby the @{text P}$_{1..n}$ are predicates and the @{text x}$_{1..n}$ @@ -1830,7 +1894,7 @@ \begin{equation}\label{weakprem} \mbox{@{text "\x\<^isub>1\x\<^isub>r. P\<^isub>i x\<^isub>i \ \ \ P\<^isub>j x\<^isub>j \ P (C\<^sup>\ x\<^isub>1 \ x\<^isub>r)"}} - \end{equation} + \end{equation}\smallskip \noindent in which the @{text "x"}$_{i..j}$ @{text "\"} @{text "x"}$_{1..r}$ are @@ -1840,24 +1904,25 @@ can first show that the free-atom functions and binding functions are equivariant, namely - \begin{center} - \begin{tabular}{rcl@ {\hspace{10mm}}rcl} - @{text "p \ (fa_ty\\<^isub>i x)"} & $=$ & @{text "fa_ty\\<^isub>i (p \ x)"} & - @{text "p \ (bn\\<^isub>j x)"} & $=$ & @{text "bn\\<^isub>j (p \ x)"}\\ - @{text "p \ (fa_bn\\<^isub>j x)"} & $=$ & @{text "fa_bn\\<^isub>j (p \ x)"}\\ - \end{tabular} - \end{center} + \[\mbox{ + \begin{tabular}{rcl} + @{text "\ \ (fa_ty\\<^isub>i x)"} & $=$ & @{text "fa_ty\\<^isub>i (\ \ x)"}\\ + @{text "\ \ (fa_bn\\<^isub>j x)"} & $=$ & @{text "fa_bn\\<^isub>j (\ \ x)"}\\ + @{text "\ \ (bn\\<^isub>j x)"} & $=$ & @{text "bn\\<^isub>j (\ \ x)"}\\ + \end{tabular}} + \] + \noindent - These properties can be established using the induction principle for the types @{text "ty\"}$_{1..n}$. - in \eqref{weakinduct}. - Having these equivariant properties established, we can - show that the support of term-constructors @{text "C\<^sup>\"} is included in - the support of its arguments, that means + These properties can be established using the induction principle for the + types @{text "ty\"}$_{1..n}$. in \eqref{weakinduct}. Having these + equivariant properties established, we can show that the support of + term-constructors @{text "C\<^sup>\"} is included in the support of its + arguments, that means - \begin{center} + \[ @{text "supp (C\<^sup>\ x\<^isub>1 \ x\<^isub>r) \ (supp x\<^isub>1 \ \ \ supp x\<^isub>r)"} - \end{center} + \]\smallskip \noindent holds. This allows us to prove by induction that @@ -2244,37 +2309,42 @@ text {* To our knowledge the earliest usage of general binders in a theorem prover - is described in \cite{NaraschewskiNipkow99} about a formalisation of the - algorithm W. This formalisation implements binding in type-schemes using a - de-Bruijn indices representation. Since type-schemes in W contain only a single - place where variables are bound, different indices do not refer to different binders (as in the usual - de-Bruijn representation), but to different bound variables. A similar idea - has been recently explored for general binders in the locally nameless - approach to binding \cite{chargueraud09}. There, de-Bruijn indices consist - of two numbers, one referring to the place where a variable is bound, and the - other to which variable is bound. The reasoning infrastructure for both - representations of bindings comes for free in theorem provers like Isabelle/HOL or - Coq, since the corresponding term-calculi can be implemented as ``normal'' - datatypes. However, in both approaches it seems difficult to achieve our - fine-grained control over the ``semantics'' of bindings (i.e.~whether the - order of binders should matter, or vacuous binders should be taken into - account). To do so, one would require additional predicates that filter out - unwanted terms. Our guess is that such predicates result in rather - intricate formal reasoning. + is described by Nara\-schew\-ski and Nipkow \cite{NaraschewskiNipkow99} with a + formalisation of the algorithm W. This formalisation implements binding in + type-schemes using a de-Bruijn indices representation. Since type-schemes in + W contain only a single place where variables are bound, different indices + do not refer to different binders (as in the usual de-Bruijn + representation), but to different bound variables. A similar idea has been + recently explored for general binders by Chargu\'eraud in the locally nameless + approach to + binding \cite{chargueraud09}. There, de-Bruijn indices consist of two + numbers, one referring to the place where a variable is bound, and the other + to which variable is bound. The reasoning infrastructure for both + representations of bindings comes for free in theorem provers like + Isabelle/HOL or Coq, since the corresponding term-calculi can be implemented + as ``normal'' datatypes. However, in both approaches it seems difficult to + achieve our fine-grained control over the ``semantics'' of bindings + (i.e.~whether the order of binders should matter, or vacuous binders should + be taken into account). To do so, one would require additional predicates + that filter out unwanted terms. Our guess is that such predicates result in + rather intricate formal reasoning. We are not aware of any non-trivial + formalisation that uses Chargu\'eraud's idea. + Another technique for representing binding is higher-order abstract syntax - (HOAS). , which for example is implemented in the Twelf system. - This representation - technique supports very elegantly many aspects of \emph{single} binding, and - impressive work has been done that uses HOAS for mechanising the metatheory - of SML~\cite{LeeCraryHarper07}. We are, however, not aware how multiple - binders of SML are represented in this work. Judging from the submitted - Twelf-solution for the POPLmark challenge, HOAS cannot easily deal with - binding constructs where the number of bound variables is not fixed. For example - In the second part of this challenge, @{text "Let"}s involve - patterns that bind multiple variables at once. In such situations, HOAS - seems to have to resort to the iterated-single-binders-approach with - all the unwanted consequences when reasoning about the resulting terms. + (HOAS), which for example is implemented in the Twelf system. This + representation technique supports very elegantly many aspects of + \emph{single} binding, and impressive work by Lee et al has been done that + uses HOAS for mechanising the metatheory of SML~\cite{LeeCraryHarper07}. We + are, however, not aware how multiple binders of SML are represented in this + work. Judging from the submitted Twelf-solution for the POPLmark challenge, + HOAS cannot easily deal with binding constructs where the number of bound + variables is not fixed. For example In the second part of this challenge, + @{text "Let"}s involve patterns that bind multiple variables at once. In + such situations, HOAS seems to have to resort to the + iterated-single-binders-approach with all the unwanted consequences when + reasoning about the resulting terms. + Two formalisations involving general binders have been performed in older @@ -2285,117 +2355,126 @@ the need to ``unbind'' variables. This can be done in one step with our general binders described in this paper, but needs a cumbersome iteration with single binders. The resulting formal reasoning turned out to - be rather unpleasant. The hope is that the extension presented in this paper - is a substantial improvement. + be rather unpleasant. - The most closely related work to the one presented here is the Ott-tool - \cite{ott-jfp} and the C$\alpha$ml language \cite{Pottier06}. Ott is a nifty - front-end for creating \LaTeX{} documents from specifications of - term-calculi involving general binders. For a subset of the specifications - Ott can also generate theorem prover code using a raw representation of - terms, and in Coq also a locally nameless representation. The developers of - this tool have also put forward (on paper) a definition for - alpha-equivalence of terms that can be specified in Ott. This definition is - rather different from ours, not using any nominal techniques. To our - knowledge there is no concrete mathematical result concerning this - notion of alpha-equivalence. Also the definition for the - notion of free variables - is work in progress. + The most closely related work to the one presented here is the Ott-tool by + Sewell et al \cite{ott-jfp} and the C$\alpha$ml language by Pottier + \cite{Pottier06}. Ott is a nifty front-end for creating \LaTeX{} documents + from specifications of term-calculi involving general binders. For a subset + of the specifications Ott can also generate theorem prover code using a raw + representation of terms, and in Coq also a locally nameless + representation. The developers of this tool have also put forward (on paper) + a definition for alpha-equivalence and free variables for terms that can be + specified in Ott. This definition is rather different from ours, not using + 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 + 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 proofs implemented on the ML-level of Isabelle/HOL. Second, it - covers cases of binders depending on other binders, which just do not make - sense for our alpha-equated terms. Third, it allows empty types that have no - meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's - binding clauses. In Ott you specify binding clauses with a single body; we - allow more than one. We have to do this, because this makes a difference - for our notion of alpha-equivalence in case of \isacommand{binds (set)} and - \isacommand{binds (set+)}. + 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 + proofs implemented on the ML-level of Isabelle/HOL. Second, it covers cases + of binders depending on other binders, which just do not make sense for our + alpha-equated terms. Third, it allows empty types that have no meaning in a + HOL-based theorem prover. We also had to generalise slightly Ott's binding + clauses. In Ott one specifies binding clauses with a single body; we allow + more than one. We have to do this, because this makes a difference for our + notion of alpha-equivalence in case of \isacommand{binds (set)} and + \isacommand{binds (set+)}. Consider the examples - Consider the examples - - \begin{center} + \[\mbox{ \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}} @{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} & \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\ @{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} & \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "t"}, \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "s"}\\ - \end{tabular} - \end{center} - - \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 - - \begin{center} - \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l} - @{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ & - @{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}\\ - @{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ & - @{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\ - \end{tabular} - \end{center} + \end{tabular}} + \]\smallskip \noindent - and therefore need the extra generality to be able to distinguish between - both specifications. - Because of how we set up our definitions, we also had to impose some restrictions - (like a single binding function for a deep binder) that are not present in Ott. - Our - expectation is that we can still cover many interesting term-calculi from - programming language research, for example Core-Haskell. + 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 \ b"}, there is no permutation that can + make @{text "(a, b)"} equal with @{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.} + + + \[\mbox{ + \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l} + @{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ & + @{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"} + \end{tabular}} + \]\smallskip + + \noindent + but - Pottier presents in \cite{Pottier06} a language, called C$\alpha$ml, for - representing terms with general binders inside OCaml. This language is - implemented as a front-end that can be translated to OCaml with the help of - a library. He presents a type-system in which the scope of general binders - can be specified using special markers, written @{text "inner"} and - @{text "outer"}. It seems our and his specifications can be - inter-translated as long as ours use the binding mode - \isacommand{binds} only. - However, we have not proved this. Pottier gives a definition for + \[\mbox{ + \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l} + @{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ & + @{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\ + \end{tabular}} + \]\smallskip + + \noindent + and therefore need the extra generality to be able to distinguish between + both specifications. Because of how we set up our definitions, we also had + to impose some restrictions (like a single binding function for a deep + binder) that are not present in Ott. Our expectation is that we can still + cover many interesting term-calculi from programming language research, for + example Core-Haskell. ??? + + Pottier presents a programming language, called C$\alpha$ml, for + representing terms with general binders inside OCaml \cite{Pottier06}. This + language is implemented as a front-end that can be translated to OCaml with + the help of a library. He presents a type-system in which the scope of + general binders can be specified using special markers, written @{text + "inner"} and @{text "outer"}. It seems our and his specifications can be + inter-translated as long as ours use the binding mode \isacommand{binds} + only. However, we have not proved this. Pottier gives a definition for 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}. - - In a slightly different domain (programming with dependent types), the - paper \cite{Altenkirch10} presents a calculus with a notion of - alpha-equivalence related to our binding mode \isacommand{binds (set+)}. - The definition in \cite{Altenkirch10} 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. + 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 ??? + + 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}. + 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. *} section {* Conclusion *} text {* - Telsescopes by de Bruijn (AUTOMATH project does not provide an automatic infrastructure). + %%Telsescopes by de Bruijn (AUTOMATH project does not provide an automatic infrastructure). - We have presented an extension of Nominal Isabelle for dealing with - general binders, that is term-constructors having multiple bound - variables. For this extension we introduced new definitions of - alpha-equivalence and automated all necessary proofs in Isabelle/HOL. - To specify general binders we used the specifications from Ott, but extended them - in some places and restricted - them in others so that they make sense in the context of alpha-equated 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{For the moment - it can be downloaded from the Mercurial repository linked at + We have presented an extension of Nominal Isabelle for dealing with general + binders, that is term-constructors having multiple bound variables. For this + extension we introduced new definitions of alpha-equivalence and automated + all necessary proofs in Isabelle/HOL. To specify general binders we used + the syntax from Ott, but extended it in some places and restricted + it in others so that they make sense in the context of alpha-equated + 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 \href{http://isabelle.in.tum.de/nominal/download} {http://isabelle.in.tum.de/nominal/download}.} @@ -2412,7 +2491,9 @@ datatype definitions allow one to specify, for instance, the function kinds in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To - achieve this, we need a slightly more clever implementation than we have at the moment. + achieve this, we need more clever implementation than we have + at the moment. However, really lifting this restriction will involve major + work on the datatype package of Isabelle/HOL. A more interesting line of investigation is whether we can go beyond the simple-minded form of binding functions that we adopted from Ott. At the moment, binding @@ -2420,18 +2501,18 @@ of atom sets (similarly for lists). It remains to be seen whether properties like - \begin{center} - @{text "fa_ty x = bn x \ fa_bn x"}. - \end{center} + \[ + \mbox{@{text "fa_ty x = bn x \ fa_bn x"}} + \]\smallskip \noindent allow us to support more interesting binding functions. We have also not yet played with other binding modes. For example we can - imagine that there is need for a binding mode where instead of lists, we - abstract lists of distinct elements. Once we feel confident about such - binding modes, our implementation can be easily extended to accommodate - them.\medskip + imagine that there is need for a binding mode where instead of usual lists, + we abstract lists of distinct elements (the corresponding type @{text + "dlist"} already exists in the library of Isabelle/HOL). We expect the + presented work can be easily extended to accommodate them.\medskip \noindent {\bf Acknowledgements:} We are very grateful to Andrew Pitts for many