# HG changeset patch # User Christian Urban # Date 1315584698 -3600 # Node ID 4baa2fccfb6142f89682faa55068a5aabab8e687 # Parent 4df720c9b660707ebba19f54bd145393d654e89f paper diff -r 4df720c9b660 -r 4baa2fccfb61 LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Fri Sep 09 11:52:24 2011 +0100 +++ b/LMCS-Paper/Paper.thy Fri Sep 09 17:11:38 2011 +0100 @@ -15,6 +15,17 @@ definition "equal \ (op =)" +fun alpha_set_ex where + "alpha_set_ex (bs, x) R f (cs, y) = (\pi. alpha_set (bs, x) R f pi (cs, y))" + +fun alpha_res_ex where + "alpha_res_ex (bs, x) R f pi (cs, y) = (\pi. alpha_res (bs, x) R f pi (cs, y))" + +fun alpha_lst_ex where + "alpha_lst_ex (bs, x) R f pi (cs, y) = (\pi. alpha_lst (bs, x) R f pi (cs, y))" + + + notation (latex output) swap ("'(_ _')" [1000, 1000] 1000) and fresh ("_ # _" [51, 51] 50) and @@ -22,9 +33,9 @@ supp ("supp _" [78] 73) and uminus ("-_" [78] 73) and If ("if _ then _ else _" 10) and - alpha_set ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and - alpha_lst ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and - alpha_res ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set+}}$}}>\<^bsup>_, _, _\<^esup> _") and + alpha_set_ex ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _\<^esup> _") and + alpha_lst_ex ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _\<^esup> _") and + alpha_res_ex ("_ \\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set+}}$}}>\<^bsup>_, _\<^esup> _") and abs_set ("_ \\<^raw:{$\,_{\textit{abs\_set}}$}> _") and abs_set2 ("_ \\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup> _") and fv ("fa'(_')" [100] 100) and @@ -657,7 +668,8 @@ \begin{defi}[Alpha-Equivalence for Set-Bindings]\label{alphaset}\mbox{}\\ \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl} - @{term "(as, x) \set R fa \ (bs, y)"}\hspace{2mm}@{text "\"} + @{term "alpha_set_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\"} & + \multicolumn{2}{@ {}l}{if there exists a @{text "\"} such that:}\\ & \mbox{\it (i)} & @{term "fa(x) - as = fa(y) - bs"}\\ & \mbox{\it (ii)} & @{term "(fa(x) - as) \* \"}\\ & \mbox{\it (iii)} & @{text "(\ \ x) R y"} \\ @@ -666,9 +678,7 @@ \end{defi} \noindent - Note that this relation depends on the permutation @{text - "\"}; alpha-equivalence between two pairs is then the relation where we - existentially quantify over this @{text "\"}. Also note that the relation is + Note that the relation is dependent on a free-atom function @{text "fa"} and a relation @{text "R"}. The reason for this extra generality is that we will use $\approx_{\,\textit{set}}$ for both ``raw'' terms and alpha-equated terms. In @@ -682,7 +692,8 @@ \begin{defi}[Alpha-Equivalence for List-Bindings]\label{alphalist}\mbox{}\\ \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl} - @{term "(as, x) \lst R fa \ (bs, y)"}\hspace{2mm}@{text "\"} + @{term "alpha_lst_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\"} & + \multicolumn{2}{@ {}l}{if there exists a @{text "\"} such that:}\\ & \mbox{\it (i)} & @{term "fa(x) - (set as) = fa(y) - (set bs)"}\\ & \mbox{\it (ii)} & @{term "(fa(x) - set as) \* \"}\\ & \mbox{\it (iii)} & @{text "(\ \ x) R y"}\\ @@ -701,7 +712,8 @@ \begin{defi}[Alpha-Equivalence for Set+-Bindings]\label{alphares}\mbox{}\\ \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl} - @{term "(as, x) \res R fa \ (bs, y)"}\hspace{2mm}@{text "\"} + @{term "alpha_res_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\"} & + \multicolumn{2}{@ {}l}{if there exists a @{text "\"} such that:}\\ & \mbox{\it (i)} & @{term "fa(x) - as = fa(y) - bs"}\\ & \mbox{\it (ii)} & @{term "(fa(x) - as) \* \"}\\ & \mbox{\it (iii)} & @{text "(\ \ x) R y"}\\ @@ -737,24 +749,25 @@ shown that all three notions of alpha-equivalence coincide, if we only abstract a single atom. - In the rest of this section we are going to introduce three abstraction - types. For this we define the relations + In the rest of this section we are going to show that the alpha-equivalences really + lead to abstractions where some atoms are bound. For this we are going to introduce + three abstraction types that are quotients with respect to the relations \begin{equation} \begin{array}{r} - @{term "alpha_abs_set (as, x) (bs, y) \ \\. alpha_set (as, x) equal supp \ (bs, y)"}\\ - @{term "alpha_abs_res (as, x) (bs, y) \ \\. alpha_res (as, x) equal supp \ (bs, y)"}\\ - @{term "alpha_abs_lst (as, x) (bs, y) \ \\. alpha_lst (as, x) equal supp \ (bs, y)"}\\ + @{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)"}\\ \end{array} \end{equation}\smallskip \noindent - We can show that these relations are equivalence - relations and equivariant. + In these relation we replaced the free-atom function @{text "fa"} with @{term "supp"} and the + relation @{text R} with equality. We can show the following properties: \begin{lem}\label{alphaeq} - The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$ - and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations and equivariant. + The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_set+}}$ + and $\approx_{\,\textit{abs\_list}}$ are equivalence relations and equivariant. \end{lem} \begin{proof} @@ -763,10 +776,10 @@ 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 - @{term "abs_set (as, x) (bs, y)"}. To show this, we need to unfold the + \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}). + (see \cite{HuffmanUrban10}). Finally we apply the permutation operation on booleans. \end{proof} \noindent @@ -803,15 +816,17 @@ \end{thm} \noindent - In effect, this theorem states that the bound names do not appear in the support - of abstractions. This can be seen as test that our Definitions \ref{alphaset}, \ref{alphalist} - and \ref{alphares} capture the idea of alpha-equivalence relations. - Below we will show the first equation of Theorem \ref{suppabs}. The others follow by similar - arguments. By definition of the abstraction type @{text "abs\<^bsub>set\<^esub>"} we have + In effect, this theorem states that the atoms @{text "as"} are bound in the + abstraction. As stated earlier, this can be seen as test that our + Definitions \ref{alphaset}, \ref{alphalist} and \ref{alphares} capture the + idea of alpha-equivalence relations. Below we will give the proof for the + first equation of Theorem \ref{suppabs}. The others follow by similar + arguments. By definition of the abstraction type @{text + "abs\<^bsub>set\<^esub>"} we have \begin{equation}\label{abseqiff} @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\;\text{if and only if}\;\;\; - @{term "\\. alpha_set (as, x) equal supp \ (bs, y)"} + @{term "alpha_set_ex (as, x) equal supp (bs, y)"} \end{equation}\smallskip \noindent @@ -836,6 +851,7 @@ \begin{proof} This lemma is straightforward using \eqref{abseqiff} and observing that the assumptions give us @{term "(a \ b) \ (supp x - as) = (supp x - as)"}. + We therefore can use as permutation the swapping @{term "(a \ b)"}. \end{proof} \noindent @@ -867,7 +883,7 @@ \]\smallskip \noindent - using fact about function applications in \eqref{supps}. Assuming + using the fact about the support of function applications in \eqref{supps}. Assuming @{term "supp x - as"} is a finite set, we further obtain \begin{equation}\label{halftwo} @@ -875,7 +891,7 @@ \end{equation}\smallskip \noindent - since for every finite sets of atoms, say @{text "bs"}, we have + This is because for every finite sets of atoms, say @{text "bs"}, we have @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}. Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes Theorem~\ref{suppabs}. @@ -898,7 +914,7 @@ collection of (possibly mutual recursive) type declarations, say @{text "ty\\<^isub>1, \, ty\\<^isub>n"}, and an associated collection of binding functions, say @{text "bn\\<^isub>1, \, bn\\<^isub>m"}. The - syntax in Nominal Isabelle for such specifications is roughly as follows: + syntax in Nominal Isabelle for such specifications is schematically as follows: \begin{equation}\label{scheme} \mbox{\begin{tabular}{@ {}p{2.5cm}l} @@ -910,7 +926,7 @@ \raisebox{2mm}{$\ldots$}\\[-2mm] \isacommand{and} @{text "ty\\<^isub>n = \"}\\ \end{tabular}} - \end{cases}$\\ + \end{cases}$\\[2mm] binding \mbox{function part} & $\begin{cases} \mbox{\begin{tabular}{l} @@ -986,9 +1002,17 @@ that we obtain a sensible notion of alpha-equivalence where it is ensured that within a given scope an atom occurrence 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 - atoms of a body cannot be free at the same time by specifying an alternative - binder for the same body). + \emph{one} binding clause of a term constructor. So for example + + \[\mbox{ + @{text "Foo x::name y::name t::trm"}\hspace{3mm} + \isacommand{binds} @{text "x"} \isacommand{in} @{text "t"}, + \isacommand{binds} @{text "y"} \isacommand{in} @{text "t"}} + \]\smallskip + + \noindent + is not allowed. This ensures that the bound atoms of a body cannot be free + at the same time by specifying an 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 @@ -1021,9 +1045,9 @@ \noindent In these specifications @{text "name"} refers to an atom type, and @{text - "fset"} to the type of finite sets. Note that for @{text lam} it does not + "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{binds (set)} or \isacommand{binds} + @{text name}. However, having \isacommand{binds (set)} or just \isacommand{binds} in the second case makes a difference to the semantics of the specification (which we will define in the next section). @@ -1108,16 +1132,16 @@ To make sure that atoms bound by deep binders cannot be free at the same time, we cannot have more than one binding function for a deep binder. Consequently we exclude specifications such as - % - \begin{center} + + \[\mbox{ \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}} @{text "Baz\<^isub>1 p::pat t::trm"} & \isacommand{binds} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\ @{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} & \isacommand{binds} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"}, \isacommand{binds} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\ - \end{tabular} - \end{center} + \end{tabular}} + \]\smallskip \noindent Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} pick @@ -1125,24 +1149,45 @@ (Since the Ott-tool does not derive a reasoning infrastructure for alpha-equated terms with deep binders, it can permit such specifications.) - We also need to restrict the form of the binding functions in order - to ensure the @{text "bn"}-functions can be defined for alpha-equated - terms. The main restriction is that we cannot return an atom in a binding function that is also - bound in the corresponding term-constructor. That means in \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"}). - In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons} - may have a binding clause involving the argument @{text trm} (the only one that - is \emph{not} used in the definition of the binding function). This restriction - is sufficient for lifting the binding function to alpha-equated terms. + We also need to restrict the form of the binding functions in order to + ensure the @{text "bn"}-functions can be defined for alpha-equated + terms. The main restriction is that we cannot return an atom in a binding + function that is also bound in the corresponding term-constructor. + Consider again the specification for @{text "trm"} and a contrived + version for assignments, @{text "assn"}: - In the version of - Nominal Isabelle described here, we also adopted the restriction from the - Ott-tool that binding functions can only return: the empty set or empty list - (as in case @{text PNil}), a singleton set or singleton list containing an - atom (case @{text PVar}), or unions of atom sets or appended atom lists - (case @{text PTup}). This restriction will simplify some automatic definitions and proofs - later on. + \begin{equation}\label{bnexp} + \mbox{% + \begin{tabular}{@ {}l@ {}} + \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\ + \isacommand{and} @{text "assn"} $=$\\ + \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\ + \hspace{5mm}$\mid$~@{text "ACons x::name y::name t::trm assn"} + \;\;\isacommand{binds} @{text "y"} \isacommand{in} @{text t}\\ + \isacommand{binder} @{text "bn::assn \ atom list"}\\ + \isacommand{where}~@{text "bn(ANil) = []"}\\ + \hspace{5mm}$\mid$~@{text "bn(ACons x y t as) = [atom x] @ bn(as)"}\\ + \end{tabular}} + \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 allow that @{text "bn"} + can return also @{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 + empty set or empty list (as in case @{text ANil}), a singleton set or + singleton list containing an atom (case @{text PVar} in \eqref{letpat}), or + unions of atom sets or appended atom lists (case @{text ACons}). This + restriction will simplify some automatic definitions and proofs later on. In order to simplify our definitions of free atoms and alpha-equivalence, we shall assume specifications @@ -1152,7 +1197,7 @@ clause, written \isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case of the lambda-terms, the completion produces - \begin{center} + \[\mbox{ \begin{tabular}{@ {}l@ {\hspace{-1mm}}} \isacommand{nominal\_datatype} @{text lam} =\\ \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"} @@ -1161,8 +1206,8 @@ \;\;\isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1 t\<^isub>2"}\\ \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"} \;\;\isacommand{binds}~@{text x} \isacommand{in} @{text t}\\ - \end{tabular} - \end{center} + \end{tabular}} + \]\smallskip \noindent The point of completion is that we can make definitions over the binding @@ -1174,16 +1219,16 @@ text {* Having dealt with all syntax matters, the problem now is how we can turn specifications into actual type definitions in Isabelle/HOL and then - establish a reasoning infrastructure for them. As - Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just - re-arranging the arguments of - term-constructors so that binders and their bodies are next to each other will - result in inadequate representations in cases like @{text "Let x\<^isub>1 = t\<^isub>1\x\<^isub>n = t\<^isub>n in s"}. - Therefore we will first - extract ``raw'' datatype definitions from the specification and then define - explicitly an alpha-equivalence relation over them. We subsequently + establish a reasoning infrastructure for them. As Pottier and Cheney pointed + out \cite{Cheney05,Pottier06}, just re-arranging the arguments of + term-constructors so that binders and their bodies are next to each other + will result in inadequate representations in cases like \mbox{@{text "Let + x\<^isub>1 = t\<^isub>1\x\<^isub>n = t\<^isub>n in s"}}. Therefore we will + first extract ``raw'' datatype definitions from the specification and then + define explicitly an alpha-equivalence relation over them. We subsequently construct the quotient of the datatypes according to our alpha-equivalence. + The ``raw'' datatype definition can be obtained by stripping off the binding clauses and the labels from the types. We also have to invent new names for the types @{text "ty\<^sup>\"} and term-constructors @{text "C\<^sup>\"} @@ -1203,18 +1248,22 @@ functions @{term "bn"}$_{1..m}$ by recursion over the corresponding raw datatype. We can also easily define permutation operations by 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)"} - \end{equation} + @{text "\ \ (C z\<^isub>1 \ z\<^isub>n) = C (\ \ z\<^isub>1) \ (\ \ z\<^isub>n)"} + \end{equation}\smallskip The first non-trivial step we have to perform is the generation of - free-atom functions from the specification. For the + \emph{free-atom functions} from the specification.\footnote{Admittedly, the + details of our definitions are 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 + \emph{partial equivalence relations} over sets of occurences.} For the \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions - + \begin{equation}\label{fvars} \mbox{@{text "fa_ty"}$_{1..n}$} - \end{equation} + \end{equation}\smallskip \noindent by recursion. @@ -1222,9 +1271,9 @@ the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$ we define - \begin{center} - @{text "fa_bn"}$_{1..m}$. - \end{center} + \[ + @{text "fa_bn"}\mbox{$_{1..m}$}. + \]\smallskip \noindent The reason for this setup is that in a deep binder not all atoms have to be @@ -1241,110 +1290,111 @@ clause means. We only show the details for the mode \isacommand{binds (set)} (the other modes are similar). Suppose the binding clause @{text bc\<^isub>i} is of the form - \begin{center} + \[ \mbox{\isacommand{binds (set)} @{text "b\<^isub>1\b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}} - \end{center} + \]\smallskip \noindent - 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 - @{text "D"} stands for the set of free atoms of the bodies, @{text B} for the - set of binding atoms in the binders and @{text "B'"} for the set of free atoms in - non-recursive deep binders, - then the free atoms of the binding clause @{text bc\<^isub>i} are\\[-2mm] - % + 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 @{text "D"} + stands for the set of free atoms of the bodies, @{text B} for the set of + binding atoms in the binders and @{text "B'"} for the set of free atoms in + non-recursive deep binders, then the free atoms of the binding clause @{text + bc\<^isub>i} are + \begin{equation}\label{fadef} \mbox{@{text "fa(bc\<^isub>i) \ (D - B) \ B'"}}. - \end{equation} - % + \end{equation}\smallskip + \noindent The set @{text D} is formally defined as - \begin{center} + \[ @{text "D \ fa_ty\<^isub>1 d\<^isub>1 \ ... \ fa_ty\<^isub>q d\<^isub>q"} - \end{center} + \]\smallskip \noindent where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function - we are defining by recursion; - (see \eqref{fvars}); - otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}. + we are defining by recursion; otherwise we set \mbox{@{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}}. The reason + for the latter choice is that @{text "ty"}$_i$ is not a type that is part of the specification, and + we assume @{text supp} is the generic notion that characterises the free variables of + a type (in fact in the next section we will show that the free-variable functions we + define here, are equal to the support once lifted to alpha-equivalence classes). In order to formally define the set @{text B} we use the following auxiliary @{text "bn"}-functions for atom types to which shallow binders may refer\\[-4mm] - \begin{center} + \[\mbox{ \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)"} - \end{tabular} - \end{center} + @{text "bn\<^bsub>atom\<^esup> a"} & @{text "\"} & @{text "{atom a}"}\\ + @{text "bn\<^bsub>atom_set\<^esup> as"} & @{text "\"} & @{text "atoms as"}\\ + @{text "bn\<^bsub>atom_list\<^esub> as"} & @{text "\"} & @{text "atoms (set as)"} + \end{tabular}} + \]\smallskip - \begin{center} - @{text "bn\<^bsub>atom\<^esub> a \ {atom a}"}\hfill - @{text "bn\<^bsub>atom_set\<^esub> as \ atoms as"}\hfill - @{text "bn\<^bsub>atom_list\<^esub> as \ atoms (set as)"} - \end{center} - % \noindent Like the function @{text atom}, the function @{text "atoms"} coerces a 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 formally defined as\\[-4mm] - % - \begin{center} + The set @{text B} is then formally defined as + + \begin{equation}\label{bdef} @{text "B \ bn_ty\<^isub>1 b\<^isub>1 \ ... \ bn_ty\<^isub>p b\<^isub>p"} - \end{center} - % + \end{equation}\smallskip + \noindent - where we use the auxiliary binding functions for shallow binders. - The set @{text "B'"} collects all free atoms in non-recursive deep - binders. Let us assume these binders in @{text "bc\<^isub>i"} are - - \begin{center} + where we use the auxiliary binding functions for shallow binders (that means + when @{text "ty"}$_i$ is of type @{text "atom"}, @{text "atom set"} or + @{text "atom list"}). The set @{text "B'"} collects all free atoms in + non-recursive deep binders. Let us assume these binders in the binding + clause @{text "bc\<^isub>i"} are + + \[ \mbox{@{text "bn\<^isub>1 l\<^isub>1, \, bn\<^isub>r l\<^isub>r"}} - \end{center} + \]\smallskip \noindent - with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ and none of the - @{text "l"}$_{1..r}$ being among the bodies @{text - "d"}$_{1..q}$. The set @{text "B'"} is defined as\\[-5mm] - % - \begin{center} - @{text "B' \ fa_bn\<^isub>1 l\<^isub>1 \ ... \ fa_bn\<^isub>r l\<^isub>r"}\\[-9mm] - \end{center} - % + with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ (see + \eqref{bdef}) and none of the @{text "l"}$_{1..r}$ being among the bodies + @{text "d"}$_{1..q}$. The set @{text "B'"} is defined as + + \begin{equation}\label{bprimedef} + @{text "B' \ fa_bn\<^isub>1 l\<^isub>1 \ ... \ fa_bn\<^isub>r l\<^isub>r"} + \end{equation}\smallskip + \noindent This completes the definition of the free-atom functions @{text "fa_ty"}$_{1..n}$. Note that for non-recursive deep binders, we have to add in \eqref{fadef} the set of atoms that are left unbound by the binding functions @{text - "bn"}$_{1..m}$. We used for the definition of - this set the functions @{text "fa_bn"}$_{1..m}$, which are also defined by mutual - recursion. Assume the user specified a @{text bn}-clause of the form + "bn"}$_{1..m}$, see also the definition in \eqref{bprimedef}. We used for + the definition of this set the functions @{text "fa_bn"}$_{1..m}$. The + definition for those functions needs to be extracted from the clauses the + user provided for @{text "bn"}$_{1..m}$ Assume the user specified a @{text + bn}-clause 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}$. For each of - the arguments we calculate the free atoms as follows: + where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$. For + each of the arguments we calculate the free atoms as follows: - \begin{center} + \[\mbox{ \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}} - $\bullet$ & @{term "fa_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"} - (that means nothing is bound in @{text "z\<^isub>i"} by the binding function),\\ + $\bullet$ & @{term "fa_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"}\\ + & (that means nothing is bound in @{text "z\<^isub>i"} by the binding function),\smallskip\\ $\bullet$ & @{term "fa_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"}, and\\ + with the recursive call @{text "bn\<^isub>i z\<^isub>i"}, and\smallskip\\ $\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"}, - but without a recursive call. - \end{tabular} - \end{center} + but without a recursive call\\ + & (that means @{text "z\<^isub>i"} is supposed to become bound by the binding function)\\ + \end{tabular}} + \]\smallskip \noindent For defining @{text "fa_bn (C z\<^isub>1 \ z\<^isub>n)"} we just union up all these sets. @@ -1356,77 +1406,79 @@ assignments, we have three free-atom functions, namely @{text "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text "fa\<^bsub>bn\<^esub>"} as follows: - % - \begin{center} + + \[\mbox{ \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} @{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \ fa\<^bsub>bn\<^esub> as"}\\ - @{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \ fa\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm] + @{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \ fa\<^bsub>trm\<^esub> t) - set (bn as)"}\smallskip\\ @{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\ - @{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \ (fa\<^bsub>trm\<^esub> t) \ (fa\<^bsub>assn\<^esub> as)"}\\[1mm] + @{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \ (fa\<^bsub>trm\<^esub> t) \ (fa\<^bsub>assn\<^esub> as)"}\smallskip\\ @{text "fa\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\ @{text "fa\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t) \ (fa\<^bsub>bn\<^esub> as)"} - \end{tabular} - \end{center} + \end{tabular}} + \]\smallskip + \noindent - Recall that @{text ANil} and @{text "ACons"} have no - binding clause in the specification. The corresponding free-atom - function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all free atoms - of an assignment (in case of @{text "ACons"}, they are given in - terms of @{text supp}, @{text "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}). - The binding only takes place in @{text Let} and - @{text "Let_rec"}. In case of @{text "Let"}, 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 - "fa\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are - free in @{text "as"}. This is - in contrast with @{text "Let_rec"} where we have a recursive - binder to 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 both @{text "fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}. - Like the function @{text "bn"}, the function @{text "fa\<^bsub>bn\<^esub>"} traverses the - list of assignments, but instead returns the free atoms, which means in this - example the free atoms in the argument @{text "t"}. + Recall that @{text ANil} and @{text "ACons"} have no binding clause in the + specification. The corresponding free-atom function @{text + "fa\<^bsub>assn\<^esub>"} therefore returns all free atoms of an assignment + (in case of @{text "ACons"}, they are given in terms of @{text supp}, @{text + "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}). The binding + only takes place in @{text Let} and @{text "Let_rec"}. In case of @{text + "Let"}, 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 "fa\<^bsub>trm\<^esub> t"}. However, we also need + to add all atoms that are free in @{text "as"}. This is in contrast with + @{text "Let_rec"} where we have a recursive binder to 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 both @{text + "fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}. Like the + function @{text "bn"}, the function @{text "fa\<^bsub>bn\<^esub>"} traverses + the list of assignments, but instead returns the free atoms, which means in + this example the free atoms in the argument @{text "t"}. - An interesting point in this - example is that a ``naked'' assignment (@{text "ANil"} or @{text "ACons"}) does not bind any - atoms, even if the binding function is specified over assignments. - Only in the context of a @{text Let} or @{text "Let_rec"}, where the binding clauses are given, will - some atoms actually 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"}-functions to alpha-equated terms if they act on - atoms that are bound. In that case, these functions would \emph{not} respect - alpha-equivalence. - Next we define the alpha-equivalence relations for the raw types @{text - "ty"}$_{1..n}$ from the specification. We write them as + An interesting point in this example is that a ``naked'' assignment (@{text + "ANil"} or @{text "ACons"}) does not bind any atoms, even if the binding + function is specified over assignments. Only in the context of a @{text Let} + or @{text "Let_rec"}, where the binding clauses are given, will some atoms + actually 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"}-functions to alpha-equated terms if they + act on atoms that are bound. In that case, these functions would \emph{not} + respect alpha-equivalence. + + Having the free atom functions at our disposal, we can next define the + alpha-equivalence relations for the raw types @{text + "ty"}$_{1..n}$. We write them as - \begin{center} - @{text "\ty"}$_{1..n}$. - \end{center} + \[ + \mbox{@{text "\ty"}$_{1..n}$}. + \]\smallskip \noindent Like with the free-atom functions, we also need to define auxiliary alpha-equivalence relations - \begin{center} - @{text "\bn\<^isub>"}$_{1..m}$ - \end{center} + \[ + \mbox{@{text "\bn\<^isub>"}$_{1..m}$} + \]\smallskip \noindent for the binding functions @{text "bn"}$_{1..m}$, To simplify our definitions we will use the following abbreviations for \emph{compound equivalence relations} and \emph{compound free-atom functions} acting on tuples. - \begin{center} + \[\mbox{ \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} - @{text "(x\<^isub>1,\, x\<^isub>n) (R\<^isub>1,\, R\<^isub>n) (x\\<^isub>1,\, x\\<^isub>n)"} & @{text "\"} & - @{text "x\<^isub>1 R\<^isub>1 x\\<^isub>1 \ \ \ x\<^isub>n R\<^isub>n x\\<^isub>n"}\\ + @{text "(x\<^isub>1,\, x\<^isub>n) (R\<^isub>1,\, R\<^isub>n) (y\<^isub>1,\, y\<^isub>n)"} & @{text "\"} & + @{text "x\<^isub>1 R\<^isub>1 y\<^isub>1 \ \ \ x\<^isub>n R\<^isub>n y\<^isub>n"}\\ @{text "(fa\<^isub>1,\, fa\<^isub>n) (x\<^isub>1,\, x\<^isub>n)"} & @{text "\"} & @{text "fa\<^isub>1 x\<^isub>1 \ \ \ fa\<^isub>n x\<^isub>n"}\\ - \end{tabular} - \end{center} + \end{tabular}} + \]\smallskip The alpha-equivalence relations are defined as inductive predicates @@ -1434,22 +1486,23 @@ term-constructor @{text C} is of type @{text ty} and has the binding clauses @{term "bc"}$_{1..k}$, then the alpha-equivalence clause has the form - \begin{center} + \[ \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} + \]\smallskip \noindent - The task below is to specify what the premises of a binding clause are. As a - special instance, we first treat the case where @{text "bc\<^isub>i"} is the - empty binding clause of the form - - \begin{center} + 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 + treat the special instance where @{text "bc\<^isub>i"} is the empty binding clause + of the form + + \[ \mbox{\isacommand{binds (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}.} - \end{center} + \]\smallskip \noindent - In this binding clause no atom is bound and we only have to alpha-relate the bodies. For this + 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 @@ -1509,7 +1562,7 @@ lets us formally define the premise @{text P} for a non-empty binding clause as: \begin{center} - \mbox{@{term "P \ \p. (B, D) \set R fa p (B', D')"}}\;. + \mbox{@{term "P \ alpha_set_ex (B, D) R fa (B', D')"}}\;. \end{center} \noindent @@ -1582,9 +1635,9 @@ \begin{center} \begin{tabular}{@ {}c @ {}} \infer{@{text "Let as t \\<^bsub>trm\<^esub> Let as' t'"}} - {@{term "\p. (bn as, t) \lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \\<^bsub>bn\<^esub> as'"}}\smallskip\\ + {@{term "alpha_lst_ex (bn as, t) alpha_trm fa_trm (bn as', t')"} & @{text "as \\<^bsub>bn\<^esub> as'"}}\smallskip\\ \makebox[0mm]{\infer{@{text "Let_rec as t \\<^bsub>trm\<^esub> Let_rec as' t'"}} - {@{term "\p. (bn as, ast) \lst alpha_trm2 fa_trm2 p (bn as', ast')"}}} + {@{term "alpha_lst_ex (bn as, ast) alpha_trm2 fa_trm2 (bn as', ast')"}}} \end{tabular} \end{center}