# HG changeset patch # User Christian Urban # Date 1278081286 -3600 # Node ID a908ea36054fc11addbf213cc1028ae2bd4dc48a # Parent e90f6a26d74b154ecfc2f5d474d692c2f15397d1 more on the paper diff -r e90f6a26d74b -r a908ea36054f Paper/Paper.thy --- a/Paper/Paper.thy Fri Jul 02 01:54:19 2010 +0100 +++ b/Paper/Paper.thy Fri Jul 02 15:34:46 2010 +0100 @@ -45,7 +45,7 @@ text {* %%% @{text "(1, (2, 3))"} - So far, Nominal Isabelle provides a mechanism for constructing + So far, Nominal Isabelle provided a mechanism for constructing $\alpha$-equated terms, for example lambda-terms \begin{center} @@ -366,7 +366,7 @@ conditions for $\alpha$-equated terms. We are also able to derive strong 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 restrictions, and also one extension, so + from the Ott-tool, but we introduce crucial restrictions, and also one extension, so that our specifications make sense for reasoning about $\alpha$-equated terms. @@ -404,9 +404,9 @@ \end{tabular} \end{center} \end{boxedminipage} - \caption{The term-language of System @{text "F\<^isub>C"} + \caption{The System @{text "F\<^isub>C"} \cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this - version of the term-language we made a modification by separating the + version of @{text "F\<^isub>C"} we made a modification by separating the grammars for type kinds and coercion kinds, as well as for types and coercion types. For this paper the interesting term-constructor is @{text "\"}, which binds multiple type-, coercion- and term-variables.\label{corehas}} @@ -601,7 +601,7 @@ *} -section {* General Binders\label{sec:binders} *} +section {* General Bindings\label{sec:binders} *} text {* In Nominal Isabelle, the user is expected to write down a specification of a @@ -683,7 +683,7 @@ \end{array} \end{equation} - It might be useful to consider first some examples for how these definitions + It might be useful to consider first some examples about how these definitions of $\alpha$-equivalence pan out in practice. For this consider the case of abstracting a set of variables over types (as in type-schemes). We set @{text R} to be the usual equality @{text "="} and for @{text "fv(T)"} we @@ -853,7 +853,7 @@ the definitions for $\alpha$-equivalence will help us in the next section. *} -section {* Specifying General Binders\label{sec:spec} *} +section {* Specifying General Bindings\label{sec:spec} *} text {* Our choice of syntax for specifications is influenced by the existing @@ -989,7 +989,7 @@ 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 - difference to the semantics of the specification (which we will define below). + difference to the semantics of the specification (which we will define in the next section). A \emph{deep} binder uses an auxiliary binding function that ``picks'' out @@ -1068,10 +1068,10 @@ The difference is that with @{text Let} we only want to bind the atoms @{text "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms inside the assignment. This difference has consequences for the free-variable - function and $\alpha$-equivalence relation, which we are going to define later. + function and $\alpha$-equivalence relation. To make sure that variables bound by deep binders cannot be free at the - same time, we cannot have more than one binding function for one binder. + same time, we cannot have more than one binding function for one deep binder. Consequently we exclude specifications such as \begin{center} @@ -1089,7 +1089,7 @@ out different atoms to become bound, respectively be free, in @{text "p"}. We also need to restrict the form of the binding functions in order - to ensure the @{text "bn"}-functions can be lifted defined for $\alpha$-equated + to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated terms. As a result we cannot return an atom in a binding function that is also bound in the corresponding term-constructor. That means in the example \eqref{letpat} that the term-constructors @{text PVar} and @{text PTup} may @@ -1097,7 +1097,7 @@ In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons} may have a binding clause involving the argument @{text t} (the only one that is \emph{not} used in the definition of the binding function). This restriction - means that we can lift the binding function to $\alpha$-equated terms. + is sufficient for defining the binding function over $\alpha$-equated terms. In the version of Nominal Isabelle described here, we also adopted the restriction from the @@ -1171,8 +1171,7 @@ in Isabelle/HOL). We then define the user-specified binding functions @{term "bn"} by recursion over the corresponding raw datatype. We can also easily define permutation operations by - recursion so that for each term constructor @{text "C"} with - arguments @{text "z"}$_{1..n}$ we have that + recursion so that for each term constructor @{text "C"} we have that % \begin{equation}\label{ceqvt} @{text "p \ (C z\<^isub>1 \ z\<^isub>n) = C (p \ z\<^isub>1) \ (p \ z\<^isub>n)"} @@ -1180,7 +1179,7 @@ The first non-trivial step we have to perform is the generation of free-variable functions from the specifications. For the - \emph{raw} types @{text "ty"}$_{1..n}$ of a specification, + \emph{raw} types @{text "ty"}$_{1..n}$ extracted from a specification, we define the free-variable functions % \begin{equation}\label{fvars} @@ -1188,7 +1187,8 @@ \end{equation} \noindent - We define them together with auxiliary free-variable functions for + by recursion over the types @{text "ty"}$_{1..n}$. + We define these functions together with auxiliary free-variable functions for the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$ we define % @@ -1203,13 +1203,13 @@ While the idea behind these free-variable functions is clear (they just collect all atoms that are not bound), because of our rather complicated - binding mechanisms their definitions are somewhat involved. The functions - are defined by recursion defining a clause for each term-constructor. Given + binding mechanisms their definitions are somewhat involved. Given the term-constructor @{text "C"} of type @{text ty} and some associated binding clauses @{text "bc\<^isub>1\bc\<^isub>k"}, the result of @{text "fv_ty (C z\<^isub>1 \ z\<^isub>n)"} will be the union @{text - "fv(bc\<^isub>1) \ \ \ fv(bc\<^isub>k)"}. Given the binding clause @{text - bc\<^isub>i} is of the form + "fv(bc\<^isub>1) \ \ \ fv(bc\<^isub>k)"} where we define below what @{text "fv"} of a binding + clause with mode \isacommand{bin\_set} means (similarly for the other modes). + Suppose the binding clause @{text bc\<^isub>i} is of the form % \begin{equation} \mbox{\isacommand{bind\_set} @{text "b\<^isub>1\b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}} @@ -1220,7 +1220,7 @@ and the binders @{text b}$_{1..p}$ either refer to labels of atom types (in case of shallow binders) or to binding functions taking a single label as argument (in case of deep binders). Assuming the - set @{text "D"} stands for the free atoms in the bodies, @{text B} for the + set @{text "D"} stands for the free atoms in the bodies, the set @{text B} for the binding atoms in the binders and @{text "B'"} for the free atoms in non-recursive deep binders, then the free atoms of the binding clause @{text bc\<^isub>i} are given by @@ -1230,7 +1230,7 @@ \end{center} \noindent - The set @{text D} is defined as + The set @{text D} is formally defined as % \begin{center} @{text "D \ fv_ty\<^isub>1 d\<^isub>1 \ ... \ fv_ty\<^isub>q d\<^isub>q"} @@ -1238,24 +1238,24 @@ \noindent whereby the functions @{text "fv_ty\<^isub>i"} are the ones we are defining by recursion - (see \eqref{fvars}) provided the @{text "d\<^isub>i"} refers to one of the types - @{text "ty"}$_{1..n}$; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}. - In order to define the set @{text B} we use the following auxiliary bn-functions + (see \eqref{fvars}) provided the @{text "d\<^isub>i"} refers to one of the raw types + @{text "ty"}$_{1..n}$ from a specification; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}. + In order to define the set @{text B} we use the following auxiliary @{text "bn"}-functions for atom types to which shallow binders have to refer % \begin{center} \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} - @{text "bn_atom a"} & @{text "="} & @{text "{atom a}"}\\ - @{text "bn_atom_set as"} & @{text "="} & @{text "atoms as"}\\ - @{text "bn_atom_list as"} & @{text "="} & @{text "atoms (set as)"} + @{text "bn_atom a"} & @{text "\"} & @{text "{atom a}"}\\ + @{text "bn_atom_set as"} & @{text "\"} & @{text "atoms as"}\\ + @{text "bn_atom_list as"} & @{text "\"} & @{text "atoms (set as)"} \end{tabular} \end{center} \noindent - In these functions, @{text "atoms"}, like @{text "atom"}, coerces + The function @{text "atoms"} coerces the set of atoms to a set of the generic atom type. It is defined as @{text "atoms as \ {atom a | a \ as}"}. - The set @{text B} is then defined as + The set @{text B} is then formally defined as % \begin{center} @{text "B \ bn_ty\<^isub>1 b\<^isub>1 \ ... \ bn_ty\<^isub>p b\<^isub>p"} @@ -1271,18 +1271,18 @@ \noindent with none of the @{text "a"}$_{1..r}$ being among the bodies @{text - "d"}$_{1..q}$. The set @{text "B'"} is then defined as + "d"}$_{1..q}$. The set @{text "B'"} is defined as % \begin{center} @{text "B' \ fv_bn\<^isub>1 a\<^isub>1 \ ... \ fv_bn\<^isub>r a\<^isub>r"} \end{center} \noindent - Similarly for the other binding modes. + This completes the definition of the free-variable functions. Note that for non-recursive deep binders, we have to add all atoms that are left unbound by the binding function @{text "bn"}. This is the purpose of the functions - @{text "fv_bn"}, also defined by recursion. Assume the user has specified + @{text "fv_bn"}, also defined by recursion. Assume the user specified a @{text bn}-clause of the form % \begin{center} @@ -1291,25 +1291,27 @@ \noindent where the @{text "z"}$_{1..n}$ are of types @{text "ty"}$_{1..n}$. For each of - the arguments we calculate the free atoms as follows + the arguments we calculate the free atoms as follows: % \begin{center} \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} - $\bullet$ & @{term "fv_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"}\\ + $\bullet$ & @{term "fv_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"} + (nothing gets bound in @{text "z\<^isub>i"}),\\ $\bullet$ & @{term "fv_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"} - with the recursive call @{text "bn\<^isub>i z\<^isub>i"}\\ + with the recursive call @{text "bn\<^isub>i z\<^isub>i"}, and\\ $\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"}, but without a recursive call \end{tabular} \end{center} \noindent - For defining @{text "fv_bn (C z\<^isub>1 \ z\<^isub>n)"}, we just union up all these values. + For defining @{text "fv_bn (C z\<^isub>1 \ z\<^isub>n)"} we just union up all these values. To see how these definitions work in practice, let us reconsider the term-constructors - @{text "Let"} and @{text "Let_rec"} from the example shown in \eqref{letrecs}. - For them we consider three free-variable functions, namely - @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}: + @{text "Let"} and @{text "Let_rec"}, as well as @{text "ANil"} and @{text "ACons"} + from the example shown in \eqref{letrecs}. + For them we define three free-variable functions, namely + @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"} as follows: % \begin{center} \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} @@ -1317,7 +1319,7 @@ @{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fv\<^bsub>assn\<^esub> as \ fv\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm] @{text "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\ - @{text "fv\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "{atom a} \ (fv\<^bsub>trm\<^esub> t) \ (fv\<^bsub>assn\<^esub> as)"}\\[1mm] + @{text "fv\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \ (fv\<^bsub>trm\<^esub> t) \ (fv\<^bsub>assn\<^esub> as)"}\\[1mm] @{text "fv\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\ @{text "fv\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t) \ (fv\<^bsub>bn\<^esub> as)"} @@ -1325,42 +1327,48 @@ \end{center} \noindent - Since there are only (implicit) empty binding clauses for the term-constructors @{text ANil} - and @{text "ACons"}, the corresponding free-variable function @{text - "fv\<^bsub>assn\<^esub>"} returns all atoms occurring in an assignment. The - binding only takes place in @{text Let} and @{text "Let_rec"}. In the @{text - "Let"}-clause we want to bind all atoms given by @{text "set (bn as)"} in - @{text t}. Therefore we have to subtract @{text "set (bn as)"} from @{text + To see the ``pattern'', recall that @{text ANil} and @{text "ACons"} have no + binding clause in the specification. The corresponding free-variable + function @{text "fv\<^bsub>assn\<^esub>"} therefore returns all atoms + occurring in an assignment. The binding only takes place in @{text Let} and + @{text "Let_rec"}. In the @{text "Let"}-clause, the binding clause specifies + that all atoms given by @{text "set (bn as)"} have to be bound in @{text + t}. Therefore we have to subtract @{text "set (bn as)"} from @{text "fv\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are - free in @{text "as"}. This is what the purpose of the function @{text - "fv\<^bsub>bn\<^esub>"} is. In contrast, in @{text "Let_rec"} we have a - recursive binder where we want to also bind all occurrences of the atoms - in @{text "set (bn as)"} inside @{text "as"}. Therefore we have to subtract @{text - "set (bn as)"} from @{text "fv\<^bsub>trm\<^esub> t"}, as well as from - @{text "fv\<^bsub>assn\<^esub> as"}. An interesting point in this example is - that an assignment ``alone'' does not have any bound variables. Only in the - context of a @{text Let} or @{text "Let_rec"} will some atoms become bound. - This is a phenomenon - that has also been pointed out in \cite{ott-jfp}. For us it is crucial, because - we would not be able to lift a @{text "bn"}-function that is defined over - arguments that are either binders or bodies. In that case @{text "bn"} would - not respect $\alpha$-equivalence. We can also see that + free in @{text "as"}. In contrast, in @{text "Let_rec"} we have a recursive + binder where we want to also bind all occurrences of the atoms in @{text + "set (bn as)"} also inside @{text "as"}. Therefore we have to subtract + @{text "set (bn as)"} from the union @{text "fv\<^bsub>trm\<^esub> t"} and @{text "fv\<^bsub>assn\<^esub> as"}. + + An interesting point in this + example is that a ``naked'' assignment does not bind any + atoms. Only in the context of a @{text Let} or @{text "Let_rec"} will + some atoms from an assignment become bound. This is a phenomenon that has also been pointed + out in \cite{ott-jfp}. For us this observation is crucial, because we would + not be able to lift the @{text "bn"}-function if it was defined over assignments + where some atoms are bound. In that case @{text "bn"} would \emph{not} respect + $\alpha$-equivalence. + + Next we define $\alpha$-equivalence relations for the raw types @{text + "ty"}$_{1..n}$. We call them % - \begin{equation}\label{bnprop} - @{text "fv_ty x = bn x \ fv_bn x"}. - \end{equation} + \begin{center} + @{text "\ty\<^isub>1, \, \ty\<^isub>n"}. + \end{center} \noindent - holds for any @{text "bn"}-function defined for the type @{text "ty"}. - - TBD below. + Like with the free-variable functions, we also need to + define auxiliary $\alpha$-equivalence relations + % + \begin{center} + @{text "\bn\<^isub>1, \, \bn\<^isub>m"} + \end{center} - Next we define $\alpha$-equivalence relations for the types @{text "ty\<^isub>1, \, ty\<^isub>n"}. We call them - @{text "\ty\<^isub>1, \, \ty\<^isub>n"}. Like with the free-variable functions, - we also need to define auxiliary $\alpha$-equivalence relations for the binding functions. - Say we have binding functions @{text "bn\<^isub>1, \, bn\<^isub>m"}, then we also define @{text "\bn\<^isub>1, \, \bn\<^isub>m"}. - To simplify our definitions we will use the following abbreviations for - relations and free-variable acting on products. + \noindent + for the binding functions @{text "bn"}$_{1..m}$, + To simplify our definitions we will use the following abbreviations for + equivalence relations and free-variable functions acting on pairs + % \begin{center} \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} @@ -1370,16 +1378,17 @@ \end{center} - The relations for $\alpha$-equivalence are inductively defined predicates, whose clauses have - conclusions of the form + The relations for $\alpha$-equivalence are inductively defined + predicates, whose clauses have the form % \begin{center} - \mbox{\infer{@{text "C x\<^isub>1 \ x\<^isub>n \ty C y\<^isub>1 \ y\<^isub>n"}} - {@{text "prems(bc\<^isub>1)"} & @{text "\"} & @{text "prems(bc\<^isub>p)"}}} + \mbox{\infer{@{text "C z\<^isub>1 \ z\<^isub>n \ty C z\\<^isub>1 \ z\\<^isub>n"}} + {@{text "prems(bc\<^isub>1) \ \ \ prems(bc\<^isub>k)"}}} \end{center} \noindent - For what follows, let us assume @{text C} is of type @{text ty}. The task + assuming the term-constructor @{text C} is of type @{text ty} and has + the binding clauses @{term "bc"}$_{1..k}$. The task is to specify what the premises of these clauses are. Again for this we analyse the binding clauses and produce a corresponding premise. *} @@ -1397,6 +1406,8 @@ fv_trm2 ("fv\<^bsub>assn\<^esub> \ fv\<^bsub>trm\<^esub>") (*>*) text {* + *TBD below * + \begin{equation}\label{alpha} \mbox{% \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} @@ -2090,6 +2101,19 @@ section {* Conclusion *} text {* +We can also see that + % + \begin{equation}\label{bnprop} + @{text "fv_ty x = bn x \ fv_bn x"}. + \end{equation} + + \noindent + holds for any @{text "bn"}-function defined for the type @{text "ty"}. + +*} + + +text {* We have presented an extension of Nominal Isabelle for deriving automatically a convenient reasoning infrastructure that can deal with general binders, that is term-constructors binding multiple variables at diff -r e90f6a26d74b -r a908ea36054f Paper/document/root.tex --- a/Paper/document/root.tex Fri Jul 02 01:54:19 2010 +0100 +++ b/Paper/document/root.tex Fri Jul 02 15:34:46 2010 +0100 @@ -38,6 +38,7 @@ \newcommand{\isasymCASE}{$\mathtt{case}$} \newcommand{\isasymOF}{$\mathtt{of}$} \newcommand{\isasymAL}{\makebox[0mm][l]{$^\alpha$}} +\newcommand{\isasymPRIME}{\makebox[0mm][l]{$'$}} \newcommand{\LET}{\;\mathtt{let}\;} \newcommand{\IN}{\;\mathtt{in}\;} \newcommand{\END}{\;\mathtt{end}\;}