# HG changeset patch # User Christian Urban # Date 1285676507 14400 # Node ID 93a73eabbffc8ae359c8243bb4a715ec6821c1f3 # Parent 11133eb76f61a524f47bd31ddd1e36ce39a10bfd# Parent 1c18f2cf39238301749d1a329a07707e7307170d merged diff -r 11133eb76f61 -r 93a73eabbffc Paper/Paper.thy --- a/Paper/Paper.thy Tue Sep 28 05:56:11 2010 -0400 +++ b/Paper/Paper.thy Tue Sep 28 08:21:47 2010 -0400 @@ -230,7 +230,10 @@ \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding clause states that all the names the function @{text "bn(as)"} returns should be bound in @{text s}. This style of specifying terms and bindings is heavily - inspired by the syntax of the Ott-tool \cite{ott-jfp}. + inspired by the syntax of the Ott-tool \cite{ott-jfp}. Though, Ott + has only one binding mode, namely the one where the order of + binders matters. Consequently, type-schemes with binding sets + of names cannot be modelled in Ott. However, we will not be able to cope with all specifications that are allowed by Ott. One reason is that Ott lets the user specify ``empty'' @@ -381,7 +384,10 @@ induction principles that have the variable convention already built in. The method behind our specification of general binders is taken from the Ott-tool, but we introduce crucial restrictions, and also extensions, so - that our specifications make sense for reasoning about $\alpha$-equated terms. + that our specifications make sense for reasoning about $\alpha$-equated terms. The main improvement over Ott is that we introduce three binding modes, + provide precise definitions for $\alpha$-equivalence and for free + variables of our terms, and provide automated proofs inside the + Isabelle theorem prover. \begin{figure} @@ -929,8 +935,8 @@ \begin{center} \begin{tabular}{l} \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\ - \isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\ - \isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\ + \isacommand{bind (set)}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\ + \isacommand{bind (res)}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\ \end{tabular} \end{center} @@ -956,8 +962,8 @@ \noindent Similarly for the other binding modes. - %Interestingly, in case of \isacommand{bind\_set} - %and \isacommand{bind\_res} the binding clauses above will make a difference to the semantics + %Interestingly, in case of \isacommand{bind (set)} + %and \isacommand{bind (res)} the binding clauses above will make a difference to the semantics %of the specifications (the corresponding $\alpha$-equivalence will differ). We will %show this later with an example. @@ -972,7 +978,7 @@ alternative binder for the same body). For binders we distinguish between \emph{shallow} and \emph{deep} binders. Shallow binders are just labels. The restriction we need to impose on them is that in case of - \isacommand{bind\_set} and \isacommand{bind\_res} the labels must either + \isacommand{bind (set)} and \isacommand{bind (res)} the labels must either refer to atom types or to sets of atom types; in case of \isacommand{bind} the labels must refer to atom types or lists of atom types. Two examples for the use of shallow binders are the specification of lambda-terms, where a @@ -982,7 +988,7 @@ \begin{center} \begin{tabular}{@ {}cc@ {}} - \begin{tabular}{@ {}l@ {\hspace{-1mm}}} + \begin{tabular}{@ {}l@ {\hspace{-2mm}}} \isacommand{nominal\_datatype} @{text lam} $=$\\ \hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\ \hspace{5mm}$\mid$~@{text "App lam lam"}\\ @@ -994,7 +1000,7 @@ \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{24mm}\isacommand{bind\_res} @{text xs} \isacommand{in} @{text T}\\ + \hspace{21mm}\isacommand{bind (res)} @{text xs} \isacommand{in} @{text T}\\ \end{tabular} \end{tabular} \end{center} @@ -1004,7 +1010,7 @@ "fset"} to the type of finite sets. Note that for @{text lam} it does not matter which binding mode we use. The reason is that we bind only a single @{text name}. However, having - \isacommand{bind\_set} or \isacommand{bind} in the second case makes a + \isacommand{bind (set)} or \isacommand{bind} in the second case makes a difference to the semantics of the specification (which we will define in the next section). @@ -1012,8 +1018,8 @@ the atoms in one argument of the term-constructor, which can be bound in other arguments and also in the same argument (we will call such binders \emph{recursive}, see below). The binding functions are - expected to return either a set of atoms (for \isacommand{bind\_set} and - \isacommand{bind\_res}) or a list of atoms (for \isacommand{bind}). They can + expected to return either a set of atoms (for \isacommand{bind (set)} and + \isacommand{bind (res)}) or a list of atoms (for \isacommand{bind}). They can 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 @@ -1225,11 +1231,11 @@ binding clauses @{text "bc\<^isub>1\bc\<^isub>k"}, the result of @{text "fa_ty (C z\<^isub>1 \ z\<^isub>n)"} will be the union @{text "fa(bc\<^isub>1) \ \ \ fa(bc\<^isub>k)"} where we will define below what @{text "fa"} for a binding - clause means. We only show the details for the mode \isacommand{bind\_set} (the other modes are similar). + clause means. We only show the details for the mode \isacommand{bind (set)} (the other modes are similar). Suppose the binding clause @{text bc\<^isub>i} is of the form % \begin{center} - \mbox{\isacommand{bind\_set} @{text "b\<^isub>1\b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}} + \mbox{\isacommand{bind (set)} @{text "b\<^isub>1\b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}} \end{center} \noindent @@ -1425,7 +1431,7 @@ empty binding clause of the form % \begin{center} - \mbox{\isacommand{bind\_set} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}.} + \mbox{\isacommand{bind (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}.} \end{center} \noindent @@ -1457,7 +1463,7 @@ Now suppose the binding clause @{text "bc\<^isub>i"} is of the general form % \begin{equation}\label{nonempty} - \mbox{\isacommand{bind\_set} @{text "b\<^isub>1\b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}.} + \mbox{\isacommand{bind (set)} @{text "b\<^isub>1\b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}.} \end{equation} \noindent @@ -2113,16 +2119,16 @@ 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{bind\_set} and - \isacommand{bind\_res}. Consider the examples + for our notion of $\alpha$-equivalence in case of \isacommand{bind (set)} and + \isacommand{bind (res)}. Consider the examples \begin{center} \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}} @{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} & - \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "t s"}\\ + \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\ @{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} & - \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "t"}, - \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "s"}\\ + \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t"}, + \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "s"}\\ \end{tabular} \end{center} @@ -2165,7 +2171,7 @@ 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{bind\_res}. + $\alpha$-equivalence related to our binding mode \isacommand{bind (res)}. 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 @@ -2182,7 +2188,8 @@ $\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. + them in others so that they make sense in the context of $\alpha$-equated terms. We also introduced two binding modes (set and res) that do not + exist in Ott. We have tried out the extension with terms from Core-Haskell, type-schemes and the lambda-calculus, and our code will eventually become part of the next Isabelle distribution.\footnote{For the moment diff -r 11133eb76f61 -r 93a73eabbffc Paper/document/root.tex --- a/Paper/document/root.tex Tue Sep 28 05:56:11 2010 -0400 +++ b/Paper/document/root.tex Tue Sep 28 08:21:47 2010 -0400 @@ -67,7 +67,8 @@ \maketitle \begin{abstract} -Nominal Isabelle is a definitional extension of the poular Isabelle/HOL theorem +Nominal Isabelle is a definitional extension of the popular Isabelle/HOL +theorem prover. It provides a proving infrastructure for convenient reasoning about programming language calculi involving named bound variables (as opposed to de-Bruijn indices). In this paper we present an extension of