# HG changeset patch # User Christian Urban # Date 1286397164 -3600 # Node ID 69780ae147f58193aedd8f840b6b3b84fb321ecb # Parent ae860c95bf9f32977ed613d3d19fe233c88ac899 down to 21 pages and changed strong induction section diff -r ae860c95bf9f -r 69780ae147f5 Nominal/Ex/Let.thy --- a/Nominal/Ex/Let.thy Wed Oct 06 08:13:09 2010 +0100 +++ b/Nominal/Ex/Let.thy Wed Oct 06 21:32:44 2010 +0100 @@ -28,7 +28,7 @@ thm trm_assn.distinct thm trm_assn.supp thm trm_assn.fresh -thm trm_assn.exhaust +thm trm_assn.exhaust[where y="t", no_vars] primrec permute_bn_raw diff -r ae860c95bf9f -r 69780ae147f5 Paper/Paper.thy --- a/Paper/Paper.thy Wed Oct 06 08:13:09 2010 +0100 +++ b/Paper/Paper.thy Wed Oct 06 21:32:44 2010 +0100 @@ -124,9 +124,10 @@ where @{text z} does not occur freely in the type. In this paper we will give a general binding mechanism and associated notion of $\alpha$-equivalence that can be used to faithfully represent this kind of binding in Nominal - Isabelle. The difficulty of finding the right notion for $\alpha$-equivalence - can be appreciated in this case by considering that the definition given by - Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). + Isabelle. + %The difficulty of finding the right notion for $\alpha$-equivalence + %can be appreciated in this case by considering that the definition given by + %Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). However, the notion of $\alpha$-equivalence that is preserved by vacuous binders is not always wanted. For example in terms like @@ -240,7 +241,7 @@ where no clause for variables is given. Arguably, such specifications make some sense in the context of Coq's type theory (which Ott supports), but not at all in a HOL-based environment where every datatype must have a non-empty - set-theoretic model \cite{Berghofer99}. + set-theoretic model. % \cite{Berghofer99}. Another reason is that we establish the reasoning infrastructure for $\alpha$-\emph{equated} terms. In contrast, Ott produces a reasoning @@ -261,14 +262,14 @@ to a variable bound somewhere else, are not excluded by Ott, but we have to). - Our insistence on reasoning with $\alpha$-equated terms comes from the - wealth of experience we gained with the older version of Nominal Isabelle: - for non-trivial properties, reasoning with $\alpha$-equated terms is much - easier than reasoning with raw terms. The fundamental reason for this is - that the HOL-logic underlying Nominal Isabelle allows us to replace - ``equals-by-equals''. In contrast, replacing - ``$\alpha$-equals-by-$\alpha$-equals'' in a representation based on raw terms - requires a lot of extra reasoning work. + %Our insistence on reasoning with $\alpha$-equated terms comes from the + %wealth of experience we gained with the older version of Nominal Isabelle: + %for non-trivial properties, reasoning with $\alpha$-equated terms is much + %easier than reasoning with raw terms. The fundamental reason for this is + %that the HOL-logic underlying Nominal Isabelle allows us to replace + %``equals-by-equals''. In contrast, replacing + %``$\alpha$-equals-by-$\alpha$-equals'' in a representation based on raw terms + %requires a lot of extra reasoning work. Although in informal settings a reasoning infrastructure for $\alpha$-equated terms is nearly always taken for granted, establishing it automatically in @@ -349,9 +350,10 @@ and lambda are lifted to the quotient level.) This construction, of course, only works if $\alpha$-equivalence is indeed an equivalence relation, and the ``raw'' definitions and theorems are respectful w.r.t.~$\alpha$-equivalence. - For example, we will not be able to lift a bound-variable function. Although - this function can be defined for raw terms, it does not respect - $\alpha$-equivalence and therefore cannot be lifted. To sum up, every lifting + %For example, we will not be able to lift a bound-variable function. Although + %this function can be defined for raw terms, it does not respect + %$\alpha$-equivalence and therefore cannot be lifted. + To sum up, every lifting of theorems to the quotient level needs proofs of some respectfulness properties (see \cite{Homeier05}). In the paper we show that we are able to automate these proofs and as a result can automatically establish a reasoning @@ -379,7 +381,7 @@ The main improvement over Ott is that we introduce three binding modes (only one is present in Ott), provide definitions for $\alpha$-equivalence and for free variables of our terms, and also derive a reasoning infrastructure - about our specifications inside Isabelle/HOL. + for our specifications inside Isabelle/HOL. %\begin{figure} @@ -448,7 +450,7 @@ the identity everywhere except on a finite number of atoms. There is a two-place permutation operation written @{text "_ \ _ :: perm \ \ \ \"} - where the generic type @{text "\"} stands for the type of the object + where the generic type @{text "\"} is the type of the object over which the permutation acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"}, the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, @@ -504,9 +506,9 @@ swapping two fresh atoms, say @{text a} and @{text b}, leaves @{text x} unchanged: - \begin{property}\label{swapfreshfresh} + \begin{myproperty}\label{swapfreshfresh} @{thm[mode=IfThen] swap_fresh_fresh[no_vars]} - \end{property} + \end{myproperty} %While often the support of an object can be relatively easily %described, for example for atoms, products, lists, function applications, @@ -546,11 +548,11 @@ %The main point of @{text supports} is that we can establish the following %two properties. % - %\begin{property}\label{supportsprop} + %\begin{myproperty}\label{supportsprop} %Given a set @{text "as"} of atoms. %{\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]} %{\it (ii)} @{thm supp_supports[no_vars]}. - %\end{property} + %\end{myproperty} % %Another important notion in the nominal logic work is \emph{equivariance}. %For a function @{text f}, say of type @{text "\ \ \"}, to be equivariant @@ -589,16 +591,16 @@ proved too unwieldy for dealing with multiple binders. For such binders the following generalisations turned out to be easier to use. - \begin{property}\label{supppermeq} + \begin{myproperty}\label{supppermeq} @{thm[mode=IfThen] supp_perm_eq[no_vars]} - \end{property} + \end{myproperty} - \begin{property}\label{avoiding} + \begin{myproperty}\label{avoiding} For a finite set @{text as} and a finitely supported @{text x} with @{term "as \* x"} and also a finitely supported @{text c}, there exists a permutation @{text p} such that @{term "(p \ as) \* c"} and @{term "supp x \* p"}. - \end{property} + \end{myproperty} \noindent The idea behind the second property is that given a finite set @{text as} @@ -760,15 +762,15 @@ representing $\alpha$-equivalence classes of pairs of type @{text "(atom set) \ \"} (in the first two cases) and of type @{text "(atom list) \ \"} (in the third case). - The elements in these types will be, respectively, written as: - - \begin{center} - @{term "Abs_set as x"} \hspace{5mm} - @{term "Abs_res as x"} \hspace{5mm} - @{term "Abs_lst as x"} - \end{center} - - \noindent + The elements in these types will be, respectively, written as + % + %\begin{center} + @{term "Abs_set as x"}, %\hspace{5mm} + @{term "Abs_res as x"} and %\hspace{5mm} + @{term "Abs_lst as x"}, + %\end{center} + % + %\noindent indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will call the types \emph{abstraction types} and their elements \emph{abstractions}. The important property we need to derive is the support of @@ -875,7 +877,8 @@ text {* Our choice of syntax for specifications is influenced by the existing - datatype package of Isabelle/HOL \cite{Berghofer99} and by the syntax of the + datatype package of Isabelle/HOL %\cite{Berghofer99} + and by the syntax of the Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a collection of (possibly mutual recursive) type declarations, say @{text "ty\\<^isub>1, \, ty\\<^isub>n"}, and an associated collection of @@ -975,7 +978,9 @@ 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). 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 @@ -1108,7 +1113,7 @@ 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"}. (Since the Ott-tool does not derive a reasoning infrastructure for - $\alpha$-equated terms, it can permit such specifications.) + $\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 @@ -1181,10 +1186,11 @@ where @{term ty} is the type used in the quotient construction for @{text "ty\<^sup>\"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}. - The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are - non-empty and the types in the constructors only occur in positive - position (see \cite{Berghofer99} for an in-depth description of the datatype package - in Isabelle/HOL). We subsequently define each of the user-specified binding + %The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are + %non-empty and the types in the constructors only occur in positive + %position (see \cite{Berghofer99} for an in-depth description of the datatype package + %in Isabelle/HOL). + We subsequently define each of the user-specified binding 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 @@ -1674,15 +1680,16 @@ and @{text "x\\<^isub>i"} are recursive arguments of @{text C} and @{text "x\<^isub>i = x\\<^isub>i"} whenever they are non-recursive arguments. We can prove this implication by applying the corresponding rule in our $\alpha$-equivalence - definition and by establishing the following auxiliary facts + definition and by establishing the following auxiliary implications %facts % \begin{equation}\label{fnresp} \mbox{% - \begin{tabular}{l} - @{text "x \ty\<^isub>i x\"}~~implies~@{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x\"}\\ - @{text "x \ty\<^isub>j x\"}~~implies~@{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x\"}\\ - @{text "x \ty\<^isub>j x\"}~~implies~@{text "bn\<^isub>j x = bn\<^isub>j x\"}\\ - @{text "x \ty\<^isub>j x\"}~~implies~@{text "x \bn\<^isub>j x\"}\\ + \begin{tabular}{ll@ {\hspace{7mm}}ll} + \mbox{\it (i)} & @{text "x \ty\<^isub>i x\"}~~@{text "\"}~~@{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x\"} & + \mbox{\it (iii)} & @{text "x \ty\<^isub>j x\"}~~@{text "\"}~~@{text "bn\<^isub>j x = bn\<^isub>j x\"}\\ + + \mbox{\it (ii)} & @{text "x \ty\<^isub>j x\"}~~@{text "\"}~~@{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x\"} & + \mbox{\it (iv)} & @{text "x \ty\<^isub>j x\"}~~@{text "\"}~~@{text "x \bn\<^isub>j x\"}\\ \end{tabular}} \end{equation} @@ -1710,11 +1717,11 @@ 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} - - \noindent + %\begin{center} + @{text "C\<^sup>\ x\<^isub>1 \ x\<^isub>r = C\<^sup>\ x\\<^isub>1 \ x\\<^isub>r"}. + %\end{center} + % + %\noindent We call these conditions as \emph{quasi-injectivity}. They correspond to the premises in our $\alpha$-equivalence relations. @@ -1744,11 +1751,11 @@ for the types @{text "ty\"}$_{i..n}$. The conclusion of the induction principle is of the form % - \begin{equation}\label{weakinduct} + %\begin{equation}\label{weakinduct} \mbox{@{text "P\<^isub>1 x\<^isub>1 \ \ \ P\<^isub>n x\<^isub>n "}} - \end{equation} - - \noindent + %\end{equation} + % + %\noindent whereby the @{text P}$_{1..n}$ are predicates and the @{text x}$_{1..n}$ have types @{text "ty\"}$_{1..n}$. This induction principle has for each term constructor @{text "C"}$^\alpha$ a premise of the form @@ -1766,36 +1773,38 @@ equivariant, namely % \begin{center} - \begin{tabular}{rcl} - @{text "p \ (fa_ty\\<^isub>i x)"} & $=$ & @{text "fa_ty\\<^isub>i (p \ x)"}\\ + \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)"}\\ - @{text "p \ (bn\\<^isub>j x)"} & $=$ & @{text "bn\\<^isub>j (p \ x)"} \end{tabular} \end{center} - + % \noindent - These properties can be established using the induction principle - in \eqref{weakinduct}. + These properties can be established using the induction principle. + %%in \eqref{weakinduct}. Having these equivariant properties established, we can - show for every term-constructor @{text "C\<^sup>\"} that + show that the support of term-constructors @{text "C\<^sup>\"} is included in + the support of its arguments, that means \begin{center} - @{text "(supp x\<^isub>1 \ \ \ supp x\<^isub>r) supports (C\<^sup>\ x\<^isub>1 \ x\<^isub>r)"} + @{text "supp (C\<^sup>\ x\<^isub>1 \ x\<^isub>r) \ (supp x\<^isub>1 \ \ \ supp x\<^isub>r)"} \end{center} \noindent - holds. This together with Property~\ref{supportsprop} allows us to prove - that every @{text x} of type @{text "ty\"}$_{1..n}$ is finitely supported, - namely @{text "finite (supp x)"}. This can be again shown by induction - over @{text "ty\"}$_{1..n}$. Lastly, we can show that the support of + holds. This allows us to prove by induction that + every @{text x} of type @{text "ty\"}$_{1..n}$ is finitely supported. + %This can be again shown by induction + %over @{text "ty\"}$_{1..n}$. + Lastly, we can show that the support of elements in @{text "ty\"}$_{1..n}$ is the same as @{text "fa_ty\"}$_{1..n}$. This fact is important in a nominal setting, but also provides evidence that our notions of free-atoms and $\alpha$-equivalence are correct. - \begin{lemma} - For every @{text "x"} of type @{text "ty\"}$_{1..n}$, we have - @{text "supp x = fa_ty\\<^isub>i x"}. - \end{lemma} + \begin{theorem} + For @{text "x"}$_{1..n}$ with type @{text "ty\"}$_{1..n}$, we have + @{text "supp x\<^isub>i = fa_ty\\<^isub>i x\<^isub>i"}. + \end{theorem} \begin{proof} The proof is by induction. In each case @@ -1888,170 +1897,270 @@ section {* Strong Induction Principles *} text {* - In the previous section we were able to provide induction principles that - allow us to perform structural inductions over $\alpha$-equated terms. - We call such induction principles \emph{weak}, because in case of the - term-constructor @{text "C\<^sup>\ x\<^isub>1 \ x\<^isub>r"}, + In the previous section we derived induction principles for $\alpha$-equated terms. + We call such induction principles \emph{weak}, because for a + term-constructor \mbox{@{text "C\<^sup>\ x\<^isub>1\x\<^isub>r"}} the induction hypothesis requires us to establish the implications \eqref{weakprem}. The problem with these implications is that in general they are difficult to establish. - The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\"} - (for example we cannot assume the variable convention for them). + The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\"}. + %%(for example we cannot assume the variable convention for them). In \cite{UrbanTasson05} we introduced a method for automatically strengthening weak induction principles for terms containing single binders. These stronger induction principles allow the user to make additional assumptions about binders. - These additional assumptions amount to a formal - version of the informal variable convention for binders. A natural question is - whether we can also strengthen the weak induction principles involving - the general binders presented here. We will indeed be able to so, but for this we need an - additional notion for permuting deep binders. - - Given a binding function @{text "bn"} we define an auxiliary permutation - operation @{text "_ \\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder. - Assuming a clause of @{text bn} is given as + %These additional assumptions amount to a formal + %version of the informal variable convention for binders. + To sketch how this strengthening extends to the case of multiple binders, we use as + running example the term-constructors @{text "Lam"} and @{text "Let"} + from example \eqref{letpat}. Instead of establishing @{text " P\<^bsub>trm\<^esub> t \ P\<^bsub>pat\<^esub> p"}, + the stronger induction principles establish properties @{text " P\<^bsub>trm\<^esub> c t \ P\<^bsub>pat\<^esub> c p"} + where the additional parameter @{text c} controls + which freshness assumptions the binders should satisfy. For the two term constructors + this means that the user has to establish in inductions the implications % \begin{center} - @{text "bn (C x\<^isub>1 \ x\<^isub>r) = rhs"}, + \begin{tabular}{l} + @{text "\a t c. {atom a} \\<^sup>* c \ (\d. P\<^bsub>trm\<^esub> d t) \ P\<^bsub>trm\<^esub> c (Lam a t)"}\\ + @{text "\p t c. (set (bn p)) \\<^sup>* c \ (\d. P\<^bsub>pat\<^esub> d p) \ (\d. P\<^bsub>trm\<^esub> d t) \ \ P\<^bsub>trm\<^esub> c (Let p t)"} + \end{tabular} \end{center} - \noindent - then we define + In \cite{UrbanTasson05} we showed how the weaker induction principles imply + the stronger ones. This was done by some quite complicated, nevertheless automated, + induction proofs. In this paper we simplify this work by leveraging the automated proof + methods from the function package of Isabelle/HOL generates. + + The reasoning principle we employ here is well-founded induction. For this we have to discharge + two proof obligations: one is that we have + well-founded measures (for each type @{text "ty"}$^\alpha_{1..n}$) that decrease in + every induction step and the other is that we have covered all cases. + As measures we use are the size functions + @{text "size_ty"}$^\alpha_{1..n}$, which we lifted in the previous section and which are + all well-founded. It is straightforward to establish that these measures decrease + in every induction step. + + What is left to show is that we covered all cases. To do so, we use + a cases lemma derived for each type, which for the terms in \eqref{letpat} + is of the form + % + \begin{equation}\label{weakcases} + \infer{@{text "P\<^bsub>trm\<^esub>"}} + {\begin{array}{l@ {\hspace{9mm}}l} + @{text "\x. t = Var x \ P\<^bsub>trm\<^esub>"} & @{text "\a t'. t = Lam a t' \ P\<^bsub>trm\<^esub>"}\\ + @{text "\t\<^isub>1 t\<^isub>2. t = App t\<^isub>1 t\<^isub>2 \ P\<^bsub>trm\<^esub>"} & @{text "\p t'. t = Let p t' \ P\<^bsub>trm\<^esub>"}\\ + \end{array}} + \end{equation} + % + These cases lemmas have a premise for auch term-constructor. + The idea behind them is that we can conclude with a property @{text "P\<^bsub>trm\<^esub>"}, + provided we can show that this property holds if we substitute for @{text "t"} all + possible term-constructors. + + The only remaining difficulty is that in order to derive the stronger induction + principles conveniently, the cases lemma in \eqref{weakcases} is too weak. For this note that + in order to apply this lemma, we have to establish @{text "P\<^bsub>trm\<^esub>"} for \emph{all} @{text Lam}- and + \emph{all} @{text Let}-terms. + What we need instead is a cases rule where we only have to consider terms that have + binders being fresh w.r.t.~a context @{text "c"}, namely + % + \begin{center} + \begin{tabular}{l} + @{text "\a t'. t = Lam a t' \ {atom a} \\<^sup>* c \ P\<^bsub>trm\<^esub>"}\\ + @{text "\p t'. t = Let p t' \ (set (bn p)) \\<^sup>* c \ P\<^bsub>trm\<^esub>"} + \end{tabular} + \end{center} + % + However, this can be relatively easily be derived from the implications in \eqref{weakcases} + by a renaming using Properties \ref{supppermeq} and \ref{avoiding}. In the first case we know + that @{text "{atom a} \\<^sup>* Lam a t"}. Property \eqref{avoiding} provides us therefore with + a permutation @{text q}, such that @{text "{atom (q \ a)} \\<^sup>* c"} and + @{text "supp (Lam a t) \\<^sup>* q"} hold. + By using Property \ref{supppermeq}, we can infer that @{text "Lam (q \ a) (q \ t) = Lam a t"} + and we are done with this case. + + The @{text Let}-case involving a (non-recursive) deep binder is a bit more complicated. + The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"}, + because @{text p} might contain names that are bound (by @{text bn}) and that are + free. To solve this problem we have to introduce a permutation functions that only + permutes names bound by @{text bn} and leaves the other names unchanged. We do this again + by lifting. Assuming a + clause @{text "bn (C x\<^isub>1 \ x\<^isub>r) = rhs"}, we define % \begin{center} @{text "p \\<^bsub>bn\<^esub> (C x\<^isub>1 \ x\<^isub>r) \ C y\<^isub>1 \ y\<^isub>r"} \end{center} - + % \noindent with @{text "y\<^isub>i"} determined as follows: % \begin{center} - \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} + \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}} $\bullet$ & @{text "y\<^isub>i \ x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\ $\bullet$ & @{text "y\<^isub>i \ p \\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\ $\bullet$ & @{text "y\<^isub>i \ p \ x\<^isub>i"} otherwise \end{tabular} \end{center} + % + Now Properties \ref{supppermeq} and \ref{avoiding} give us a permutation @{text q} such that + @{text "(set (bn (q \\<^bsub>bn\<^esub> p)) \\<^sup>* c"} holds and such that @{text "[q \\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \ t)"} + is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \\<^bsub>bn\<^esub> p) \\<^bsub>bn\<^esub> p"}. But + these facts establish that @{text "Let (q \\<^bsub>bn\<^esub> p) (p \ t) = Let p t"}, as we need. This + completes the interesting cases in \eqref{letpat} for stregthening the induction + principles. - \noindent - Using again the quotient package we can lift the @{text "_ \\<^bsub>bn\<^esub> _"} function to - $\alpha$-equated terms. We can then prove the following two facts + - \begin{lemma}\label{permutebn} - Given a binding function @{text "bn\<^sup>\"} then for all @{text p} - {\it (i)} @{text "p \ (bn\<^sup>\ x) = bn\<^sup>\ (p \\\<^bsub>bn\<^esub> x)"} and {\it (ii)} - @{text "fa_bn\<^isup>\ x = fa_bn\<^isup>\ (p \\\<^bsub>bn\<^esub> x)"}. - \end{lemma} + %A natural question is + %whether we can also strengthen the weak induction principles involving + %the general binders presented here. We will indeed be able to so, but for this we need an + %additional notion for permuting deep binders. - \begin{proof} - By induction on @{text x}. The equations follow by simple unfolding - of the definitions. - \end{proof} + %Given a binding function @{text "bn"} we define an auxiliary permutation + %operation @{text "_ \\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder. + %Assuming a clause of @{text bn} is given as + % + %\begin{center} + %@{text "bn (C x\<^isub>1 \ x\<^isub>r) = rhs"}, + %\end{center} - \noindent - The first property states that a permutation applied to a binding function is - equivalent to first permuting the binders and then calculating the bound - atoms. The second amounts to the fact that permuting the binders has no - effect on the free-atom function. The main point of this permutation - function, however, is that if we have a permutation that is fresh - for the support of an object @{text x}, then we can use this permutation - to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the - @{text "Let"} term-constructor from the example shown - in \eqref{letpat} this means for a permutation @{text "r"} + %\noindent + %then we define + % + %\begin{center} + %@{text "p \\<^bsub>bn\<^esub> (C x\<^isub>1 \ x\<^isub>r) \ C y\<^isub>1 \ y\<^isub>r"} + %\end{center} + + %\noindent + %with @{text "y\<^isub>i"} determined as follows: % - \begin{equation}\label{renaming} - \begin{array}{l} - \mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2) \* r"}}\\ - \qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \\\<^bsub>bn_pat\<^esub> p) t\<^isub>1 (r \ t\<^isub>2)"}} - \end{array} - \end{equation} + %\begin{center} + %\begin{tabular}{c@ {\hspace{2mm}}p{7cm}} + %$\bullet$ & @{text "y\<^isub>i \ x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\ + %$\bullet$ & @{text "y\<^isub>i \ p \\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\ + %$\bullet$ & @{text "y\<^isub>i \ p \ x\<^isub>i"} otherwise + %\end{tabular} + %\end{center} + + %\noindent + %Using again the quotient package we can lift the @{text "_ \\<^bsub>bn\<^esub> _"} function to + %$\alpha$-equated terms. We can then prove the following two facts + + %\begin{lemma}\label{permutebn} + %Given a binding function @{text "bn\<^sup>\"} then for all @{text p} + %{\it (i)} @{text "p \ (bn\<^sup>\ x) = bn\<^sup>\ (p \\\<^bsub>bn\<^esub> x)"} and {\it (ii)} + % @{text "fa_bn\<^isup>\ x = fa_bn\<^isup>\ (p \\\<^bsub>bn\<^esub> x)"}. + %\end{lemma} - \noindent - This fact will be crucial when establishing the strong induction principles below. + %\begin{proof} + %By induction on @{text x}. The equations follow by simple unfolding + %of the definitions. + %\end{proof} + + %\noindent + %The first property states that a permutation applied to a binding function is + %equivalent to first permuting the binders and then calculating the bound + %atoms. The second amounts to the fact that permuting the binders has no + %effect on the free-atom function. The main point of this permutation + %function, however, is that if we have a permutation that is fresh + %for the support of an object @{text x}, then we can use this permutation + %to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the + %@{text "Let"} term-constructor from the example shown + %in \eqref{letpat} this means for a permutation @{text "r"} + %% + %\begin{equation}\label{renaming} + %\begin{array}{l} + %\mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2) \* r"}}\\ + %\qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \\\<^bsub>bn_pat\<^esub> p) t\<^isub>1 (r \ t\<^isub>2)"}} + %\end{array} + %\end{equation} + + %\noindent + %This fact will be crucial when establishing the strong induction principles below. - In our running example about @{text "Let"}, the strong induction - principle means that instead - of establishing the implication + %In our running example about @{text "Let"}, the strong induction + %principle means that instead + %of establishing the implication % - \begin{center} - @{text "\p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \ P\<^bsub>trm\<^esub> t\<^isub>1 \ P\<^bsub>trm\<^esub> t\<^isub>2 \ P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"} - \end{center} - - \noindent - it is sufficient to establish the following implication + %\begin{center} + %@{text "\p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \ P\<^bsub>trm\<^esub> t\<^isub>1 \ P\<^bsub>trm\<^esub> t\<^isub>2 \ P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"} + %\end{center} + % + %\noindent + %it is sufficient to establish the following implication % - \begin{equation}\label{strong} - \mbox{\begin{tabular}{l} - @{text "\p t\<^isub>1 t\<^isub>2 c."}\\ - \hspace{5mm}@{text "set (bn p) #\<^sup>* c \"}\\ - \hspace{5mm}@{text "(\d. P\<^bsub>pat\<^esub> d p) \ (\d. P\<^bsub>trm\<^esub> d t\<^isub>1) \ (\d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\ - \hspace{15mm}@{text "\ P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"} - \end{tabular}} - \end{equation} - - \noindent - While this implication contains an additional argument, namely @{text c}, and - also additional universal quantifications, it is usually easier to establish. - The reason is that we have the freshness - assumption @{text "set (bn\<^sup>\ p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily - chosen by the user as long as it has finite support. - - Let us now show how we derive the strong induction principles from the - weak ones. In case of the @{text "Let"}-example we derive by the weak - induction the following two properties + %\begin{equation}\label{strong} + %\mbox{\begin{tabular}{l} + %@{text "\p t\<^isub>1 t\<^isub>2 c."}\\ + %\hspace{5mm}@{text "set (bn p) #\<^sup>* c \"}\\ + %\hspace{5mm}@{text "(\d. P\<^bsub>pat\<^esub> d p) \ (\d. P\<^bsub>trm\<^esub> d t\<^isub>1) \ (\d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\ + %\hspace{15mm}@{text "\ P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"} + %\end{tabular}} + %\end{equation} + % + %\noindent + %While this implication contains an additional argument, namely @{text c}, and + %also additional universal quantifications, it is usually easier to establish. + %The reason is that we have the freshness + %assumption @{text "set (bn\<^sup>\ p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily + %chosen by the user as long as it has finite support. + % + %Let us now show how we derive the strong induction principles from the + %weak ones. In case of the @{text "Let"}-example we derive by the weak + %induction the following two properties + % + %\begin{equation}\label{hyps} + %@{text "\q c. P\<^bsub>trm\<^esub> c (q \ t)"} \hspace{4mm} + %@{text "\q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \\\<^bsub>bn\<^esub> (q\<^isub>2 \ p))"} + %\end{equation} % - \begin{equation}\label{hyps} - @{text "\q c. P\<^bsub>trm\<^esub> c (q \ t)"} \hspace{4mm} - @{text "\q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \\\<^bsub>bn\<^esub> (q\<^isub>2 \ p))"} - \end{equation} - - \noindent - For the @{text Let} term-constructor we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \ Let p t\<^isub>1 t\<^isub>2)"} - assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}). - By Property~\ref{avoiding} we - obtain a permutation @{text "r"} such that + %\noindent + %For the @{text Let} term-constructor we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \ Let p t\<^isub>1 t\<^isub>2)"} + %assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}). + %By Property~\ref{avoiding} we + %obtain a permutation @{text "r"} such that % - \begin{equation}\label{rprops} - @{term "(r \ set (bn (q \ p))) \* c "}\hspace{4mm} - @{term "supp (Abs_lst (bn (q \ p)) (q \ t\<^isub>2)) \* r"} - \end{equation} - - \noindent - hold. The latter fact and \eqref{renaming} give us + %\begin{equation}\label{rprops} + %@{term "(r \ set (bn (q \ p))) \* c "}\hspace{4mm} + %@{term "supp (Abs_lst (bn (q \ p)) (q \ t\<^isub>2)) \* r"} + %\end{equation} + % + %\noindent + %hold. The latter fact and \eqref{renaming} give us + %% + %\begin{center} + %\begin{tabular}{l} + %@{text "Let (q \ p) (q \ t\<^isub>1) (q \ t\<^isub>2) ="} \\ + %\hspace{15mm}@{text "Let (r \\\<^bsub>bn\<^esub> (q \ p)) (q \ t\<^isub>1) (r \ (q \ t\<^isub>2))"} + %\end{tabular} + %\end{center} % - \begin{center} - \begin{tabular}{l} - @{text "Let (q \ p) (q \ t\<^isub>1) (q \ t\<^isub>2) ="} \\ - \hspace{15mm}@{text "Let (r \\\<^bsub>bn\<^esub> (q \ p)) (q \ t\<^isub>1) (r \ (q \ t\<^isub>2))"} - \end{tabular} - \end{center} - - \noindent - So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \ Let p t\<^isub>1 t\<^isub>2)"}, we can equally - establish @{text "P\<^bsub>trm\<^esub> c (Let (r \\\<^bsub>bn\<^esub> (q \ p)) (q \ t\<^isub>1) (r \ (q \ t\<^isub>2)))"}. - To do so, we will use the implication \eqref{strong} of the strong induction - principle, which requires us to discharge - the following four proof obligations: + %\noindent + %So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \ Let p t\<^isub>1 t\<^isub>2)"}, we can equally + %establish @{text "P\<^bsub>trm\<^esub> c (Let (r \\\<^bsub>bn\<^esub> (q \ p)) (q \ t\<^isub>1) (r \ (q \ t\<^isub>2)))"}. + %To do so, we will use the implication \eqref{strong} of the strong induction + %principle, which requires us to discharge + %the following four proof obligations: + %% + %\begin{center} + %\begin{tabular}{rl} + %{\it (i)} & @{text "set (bn (r \\\<^bsub>bn\<^esub> (q \ p))) #\<^sup>* c"}\\ + %{\it (ii)} & @{text "\d. P\<^bsub>pat\<^esub> d (r \\\<^bsub>bn\<^esub> (q \ p))"}\\ + %{\it (iii)} & @{text "\d. P\<^bsub>trm\<^esub> d (q \ t\<^isub>1)"}\\ + %{\it (iv)} & @{text "\d. P\<^bsub>trm\<^esub> d (r \ (q \ t\<^isub>2))"}\\ + %\end{tabular} + %\end{center} % - \begin{center} - \begin{tabular}{rl} - {\it (i)} & @{text "set (bn (r \\\<^bsub>bn\<^esub> (q \ p))) #\<^sup>* c"}\\ - {\it (ii)} & @{text "\d. P\<^bsub>pat\<^esub> d (r \\\<^bsub>bn\<^esub> (q \ p))"}\\ - {\it (iii)} & @{text "\d. P\<^bsub>trm\<^esub> d (q \ t\<^isub>1)"}\\ - {\it (iv)} & @{text "\d. P\<^bsub>trm\<^esub> d (r \ (q \ t\<^isub>2))"}\\ - \end{tabular} - \end{center} - - \noindent - The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the - others from the induction hypotheses in \eqref{hyps} (in the fourth case - we have to use the fact that @{term "(r \ (q \ t\<^isub>2)) = (r + q) \ t\<^isub>2"}). - - Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps}, - we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}. - This completes the proof showing that the weak induction principles imply - the strong induction principles. + %\noindent + %The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the + %others from the induction hypotheses in \eqref{hyps} (in the fourth case + %we have to use the fact that @{term "(r \ (q \ t\<^isub>2)) = (r + q) \ t\<^isub>2"}). + % + %Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps}, + %we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}. + %This completes the proof showing that the weak induction principles imply + %the strong induction principles. *} @@ -2073,9 +2182,9 @@ 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. + 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. Another representation technique for binding is higher-order abstract syntax (HOAS), which for example is implemented in the Twelf system. This representation @@ -2158,9 +2267,10 @@ %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. + (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 in \cite{Pottier06} a language, called C$\alpha$ml, for representing terms with general binders inside OCaml. This language is @@ -2175,6 +2285,7 @@ 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 diff -r ae860c95bf9f -r 69780ae147f5 Paper/document/root.bib --- a/Paper/document/root.bib Wed Oct 06 08:13:09 2010 +0100 +++ b/Paper/document/root.bib Wed Oct 06 21:32:44 2010 +0100 @@ -1,3 +1,12 @@ + +@InProceedings{cheney05a, + author = {J.~Cheney}, + title = {{S}crap your {N}ameplate ({F}unctional {P}earl)}, + booktitle = {Proc.~of the 10th ICFP Conference}, + pages = {180--191}, + year = {2005} +} + @Inproceedings{Altenkirch10, author = {T.~Altenkirch and N.~A.~Danielsson and A.~L\"oh and N.~Oury}, title = {{PiSigma}: {D}ependent {T}ypes {W}ithout the {S}ugar}, diff -r ae860c95bf9f -r 69780ae147f5 Paper/document/root.tex --- a/Paper/document/root.tex Wed Oct 06 08:13:09 2010 +0100 +++ b/Paper/document/root.tex Wed Oct 06 21:32:44 2010 +0100 @@ -41,6 +41,7 @@ \newcommand{\isasymOF}{$\mathtt{of}$} \newcommand{\isasymAL}{\makebox[0mm][l]{$^\alpha$}} \newcommand{\isasymPRIME}{\makebox[0mm][l]{$'$}} +\newcommand{\isasymFRESH}{\#} \newcommand{\LET}{\;\mathtt{let}\;} \newcommand{\IN}{\;\mathtt{in}\;} \newcommand{\END}{\;\mathtt{end}\;} @@ -55,7 +56,7 @@ %%\newtheorem{lemma}[thm]{Lemma} %%\spnewtheorem{defn}[theorem]{Definition} %%\spnewtheorem{exmple}[theorem]{Example} - +\spnewtheorem{myproperty}{Property}{\bfseries}{\rmfamily} %-------------------- environment definitions ----------------- \newenvironment{proof-of}[1]{{\em Proof of #1:}}{}