# HG changeset patch # User Christian Urban # Date 1278032059 -3600 # Node ID e90f6a26d74b154ecfc2f5d474d692c2f15397d1 # Parent 36aeb97fabb0cbfe6fcd77cc241499f793bf6ff0 finished fv-section diff -r 36aeb97fabb0 -r e90f6a26d74b Paper/Paper.thy --- a/Paper/Paper.thy Thu Jul 01 14:18:36 2010 +0100 +++ b/Paper/Paper.thy Fri Jul 02 01:54:19 2010 +0100 @@ -946,13 +946,14 @@ %of the specifications (the corresponding $\alpha$-equivalence will differ). We will %show this later with an example. - There are also some restrictions we need to impose on binding clauses: the + There are also some restrictions we need to impose on binding clauses. The main idea behind these restrictions is that we obtain a sensible notion of $\alpha$-equivalence where it is ensured that within a given scope a - variable occurence cannot be bound and free at the same time. First, a body can only occur in + variable occurence cannot be both bound and free at the same time. The first + restriction is that a body can only occur in \emph{one} binding clause of a term constructor (this ensures that the bound variables of a body cannot be free at the same time by specifying an - alternative binder for the body). For binders we distinguish between + 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 @@ -1040,7 +1041,7 @@ \end{center} \noindent - where the argument of the deep binder is also in the body. We call such + where the argument of the deep binder also occurs in the body. We call such binders \emph{recursive}. To see the purpose of such recursive binders, compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following specification: @@ -1070,8 +1071,8 @@ function and $\alpha$-equivalence relation, which we are going to define later. To make sure that variables bound by deep binders cannot be free at the - same time, we have to impose some further restrictions. First, - we cannot have more than one binding function for one binder. So we exclude: + same time, we cannot have more than one binding function for one binder. + Consequently we exclude specifications such as \begin{center} \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}} @@ -1084,12 +1085,12 @@ \end{center} \noindent - Otherwise it is be possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} pick - out different atoms to become bound in @{text "p"}. + Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} pick + out different atoms to become bound, respectively be free, in @{text "p"}. - - We also need to restrict the form of the binding functions. As will shortly - become clear, we cannot return an atom in a binding function that is also + 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 + 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 not have a binding clause (all arguments are used to define @{text "bn"}). @@ -1168,22 +1169,18 @@ non-empty and the types in the constructors only occur in positive position (see \cite{Berghofer99} for an indepth description of the datatype package in Isabelle/HOL). We then define the user-specified binding - functions, called @{term "bn"}, by recursion over the corresponding + 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 the - argument types @{text "ty"}$_{1..n}$ we have that + recursion so that for each term constructor @{text "C"} with + arguments @{text "z"}$_{1..n}$ 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)"} \end{equation} - \noindent - where the variables @{text "z"}$_{1..n}$ are of types @{text "ty"}$_{1..n}$. - The first non-trivial step we have to perform is the generation of - free-variable functions from the specifications. Given a raw term, these - functions return sets of atoms. Assuming a nominal datatype - specification as in \eqref{scheme} and its \emph{raw} types @{text "ty"}$_{1..n}$, + free-variable functions from the specifications. For the + \emph{raw} types @{text "ty"}$_{1..n}$ of a specification, we define the free-variable functions % \begin{equation}\label{fvars} @@ -1206,120 +1203,113 @@ 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. Given a - term-constructor @{text "C"} of type @{text ty} and some associated binding - clauses @{text "bc\<^isub>1\bc\<^isub>k"}, the result of the @{text "fv_ty (C z\<^isub>1 \ z\<^isub>n)"} will be - the union @{text "fv(bc\<^isub>1) \ \ \ fv(bc\<^isub>k)"} of free variables calculated for - each binding clause. Given a binding clause @{text bc} is of the form + binding mechanisms their definitions are somewhat involved. The functions + are defined by recursion defining a clause for each term-constructor. 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 % \begin{equation} - \mbox{\isacommand{bind} @{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 - where the body labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$; the binders - @{text b}$_{1..p}$ + in which the body-labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$, + 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 - free variables of the bodies is the set @{text "D"}, the bound variables of the binders - is the set @{text B} and the free variables of the non-recursive deep binders is @{text "B'"} - then the free variables of the binding clause @{text bc} is + set @{text "D"} stands for the free atoms in the bodies, @{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 % \begin{center} - @{text "fv(bc) = (D - B) \ B'"} + @{text "fv(bc\<^isub>i) \ (D - B) \ B'"} \end{center} \noindent - Formally the set @{text D} is the union of the free variables for the bodies + The set @{text D} is defined as % \begin{center} - @{text "D = fv_ty\<^isub>1 d\<^isub>1 \ ... \ fv_ty\<^isub>q d\<^isub>q"} + @{text "D \ fv_ty\<^isub>1 d\<^isub>1 \ ... \ fv_ty\<^isub>q d\<^isub>q"} \end{center} \noindent - whereby the free variable functions @{text "fv_ty\<^isub>i"} are the ones in \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"}. - - -if @{text "d\<^isub>i"} is a label - for an atomic type we use the following auxiliary free variable functions - + 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 + for atom types to which shallow binders have to refer + % \begin{center} \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} - @{text "fv_atom a"} & @{text "="} & @{text "{atom a}"}\\ - @{text "fv_atom_set as"} & @{text "="} & @{text "atoms as"}\\ - @{text "fv_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 set of atoms to a set of the generic atom type. - It is defined as @{text "atoms as \ {atom a | a \ as}"}. Otherwise - + 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 + % + \begin{center} + @{text "B \ bn_ty\<^isub>1 b\<^isub>1 \ ... \ bn_ty\<^isub>p b\<^isub>p"} + \end{center} - -the values, @{text v}, calculated by the rules for each bining clause: + \noindent + The set @{text "B'"} collects all free atoms in non-recursive deep + binders. Lets assume these binders in @{text "bc\<^isub>i"} are % - \begin{equation}\label{deepbinderA} - \mbox{% - \begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}} - \multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ - $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} is of type @{text "ty"}\smallskip\\ - % - \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "x\<^isub>1\x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1\y\<^isub>m"}:}\\ - $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \ .. \ fv_ty\<^isub>m y\<^isub>m)"}\\ - & \hspace{15mm}@{text "- (fv_aty\<^isub>1 x\<^isub>1 \ .. \ fv_aty\<^isub>n x\<^isub>n)"}\\ - & provided the bodies @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$ and the - binders @{text "x"}$_{1..n}$ of atomic types @{text "aty"}$_{1..n}$\smallskip\\ - \end{tabular}} - \end{equation} - \begin{equation}\label{deepbinderB} - \mbox{% - \begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}} - \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1\y\<^isub>m"}:}\\ - $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \ .. \ fv_ty\<^isub>m y\<^isub>m) - set (bn x) \ (fv_bn x)"}\\ - $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \ .. \ fv_ty\<^isub>m y\<^isub>m) - set (bn x)"}\\ - & provided the @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$; the first - clause applies for @{text x} being a non-recursive deep binder (that is - @{text "x \ y"}$_{1..m}$), the second for a recursive deep binder - \end{tabular}} - \end{equation} + \begin{center} + @{text "bn\<^isub>1 a\<^isub>1, \, bn\<^isub>r a\<^isub>r"} + \end{center} + + \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 + % + \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. Note that in a non-recursive deep - binder, we have to add all atoms that are left unbound by the binding - function @{text "bn"}. For this we define the function @{text "fv_bn"}. Assume - for the constructor @{text "C"} the binding function is of the form @{text - "bn (C z\<^isub>1 \ z\<^isub>n) = rhs"}. We again define a value - @{text v} which is exactly as in \eqref{deepbinderA}/\eqref{deepbinderB} for shallow and deep - binding clauses, except for empty binding clauses are defined as follows: + Similarly for the other binding modes. + + 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 + a @{text bn}-clause of the form % - \begin{equation}\label{bnemptybinder} - \mbox{% - \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} - \multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ - $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} does not occur in @{text "rhs"} - and the free-variable function for the type of @{text "y"} is @{text "fv_ty"}\\ - $\bullet$ & @{term "v = fv_bn y"} provided @{text "y"} occurs in @{text "rhs"} - with a recursive call @{text "bn y"}\\ - $\bullet$ & @{term "v = {}"} provided @{text "y"} occurs in @{text "rhs"}, - but without a recursive call\\ - \end{tabular}} - \end{equation} + \begin{center} + @{text "bn (C z\<^isub>1 \ z\<^isub>n) = rhs"} + \end{center} \noindent - The reason why we only have to treat the empty binding clauses specially in - the definition of @{text "fv_bn"} is that binding functions can only use arguments - that do not occur in binding clauses. Otherwise the @{text "bn"} function cannot - be lifted to $\alpha$-equated terms. + 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 + % + \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_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"}\\ + $\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. + 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 this specification we need to define three free-variable functions, namely - @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}. They are as follows: + 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>"}: % \begin{center} \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} @@ -1363,6 +1353,8 @@ \noindent holds for any @{text "bn"}-function defined for the type @{text "ty"}. + TBD below. + 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. @@ -1382,7 +1374,8 @@ conclusions of the form % \begin{center} - @{text "C x\<^isub>1 \ x\<^isub>n \ty C y\<^isub>1 \ y\<^isub>n"} + \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)"}}} \end{center} \noindent @@ -2060,24 +2053,6 @@ \end{tabular} \end{center} - To see this, consider the following equations - - \begin{center} - \begin{tabular}{c} - @{term "Abs_print [a,b] (a, b) = Abs_print [a,b] (b, a)"}\\ - @{term "Abs_print [a,b] (a, b) = Abs_print [a,b] (a, b)"}\\ - \end{tabular} - \end{center} - - \noindent - The interesting point is that they do not imply - - \begin{center} - \begin{tabular}{c} - @{term "Abs_print [a,b] ((a, b), (a, b)) = Abs_print [a,b] ((a, b), (b, a))"}\\ - \end{tabular} - \end{center} - Because of how we set up our definitions, we had to impose 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 diff -r 36aeb97fabb0 -r e90f6a26d74b Paper/document/root.bib --- a/Paper/document/root.bib Thu Jul 01 14:18:36 2010 +0100 +++ b/Paper/document/root.bib Fri Jul 02 01:54:19 2010 +0100 @@ -67,7 +67,7 @@ @InProceedings{CoreHaskell, author = {M.~Sulzmann and M.~Chakravarty and S.~Peyton Jones and K.~Donnelly}, title = {{S}ystem {F} with {T}ype {E}quality {C}oercions}, - booktitle = {Proc of the TLDI Workshop}, + booktitle = {Proc.~of the TLDI Workshop}, pages = {53-66}, year = {2007} } @@ -173,7 +173,7 @@ @article{MckinnaPollack99, author = {J.~McKinna and R.~Pollack}, title = {{S}ome {T}ype {T}heory and {L}ambda {C}alculus {F}ormalised}, - journal = {Journal of Automated Reasoning}, + journal = {J.~of Automated Reasoning}, volume = 23, number = {1-4}, year = 1999