# HG changeset patch # User Christian Urban # Date 1274767156 -7200 # Node ID 5054f170024e4842a9e9b98b5178c0e92fe6ed67 # Parent f11dd09fa3a74d60fc4ef409edd96d36fe0813e4 edits from the reviewers diff -r f11dd09fa3a7 -r 5054f170024e Paper/Paper.thy --- a/Paper/Paper.thy Mon May 24 22:47:06 2010 +0100 +++ b/Paper/Paper.thy Tue May 25 07:59:16 2010 +0200 @@ -85,7 +85,7 @@ also there one would like to bind multiple variables at once. Binding multiple variables has interesting properties that cannot be captured - easily by iterating single binders. For example in case of type-schemes we do not + easily by iterating single binders. For example in the case of type-schemes we do not want to make a distinction about the order of the bound variables. Therefore we would like to regard the following two type-schemes as alpha-equivalent % @@ -183,10 +183,10 @@ where the notation @{text "[_]._"} indicates that the list of @{text "x\<^isub>i"} becomes bound in @{text s}. In this representation the term \mbox{@{text "\ [x].s [t\<^isub>1, t\<^isub>2]"}} is a perfectly legal - instance, but the lengths of two lists do not agree. To exclude such terms, + instance, but the lengths of the two lists do not agree. To exclude such terms, additional predicates about well-formed terms are needed in order to ensure that the two lists are of equal - length. This can result into very messy reasoning (see for + length. This can result in very messy reasoning (see for example~\cite{BengtsonParow09}). To avoid this, we will allow type specifications for $\mathtt{let}$s as follows % @@ -220,7 +220,7 @@ inspired by the syntax of the Ott-tool \cite{ott-jfp}. However, we will not be able to cope with all specifications that are - allowed by Ott. One reason is that Ott lets the user to specify ``empty'' + allowed by Ott. One reason is that Ott lets the user specify ``empty'' types like \begin{center} @@ -704,7 +704,7 @@ $\not\approx_{\textit{set}}$ @{text "({x, y}, x)"} since there is no permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal (similarly for $\approx_{\textit{list}}$). It can also relatively easily be - shown that all tree notions of alpha-equivalence coincide, if we only + 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 @@ -1119,7 +1119,7 @@ term-constructors so that binders and their bodies are next to each other will result in inadequate representations. Therefore we will first extract datatype definitions from the specification and then define - expicitly an alpha-equivalence relation over them. + explicitly an alpha-equivalence relation over them. The datatype definition can be obtained by stripping off the @@ -1152,7 +1152,7 @@ @{text "p \ (C z\<^isub>1 \ z\<^isub>n) = C (p \ z\<^isub>1) \ (p \ z\<^isub>n)"} \end{equation} - The first non-trivial step we have to perform is the generation free-variable + The first non-trivial step we have to perform is the generation of free-variable functions from the specifications. For atomic types we define the auxilary free variable functions: @@ -1455,7 +1455,7 @@ \begin{proof} The proof is by mutual induction over the definitions. The non-trivial - cases involve premises build up by $\approx_{\textit{set}}$, + cases involve premises built up by $\approx_{\textit{set}}$, $\approx_{\textit{res}}$ and $\approx_{\textit{list}}$. They can be dealt with as in Lemma~\ref{alphaeq}. \end{proof} @@ -1526,7 +1526,7 @@ \end{center} \noindent - for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\\<^esub>\<^isub>i"} stand for properties + for all @{text "y\<^isub>i"} whereby the variables @{text "P\<^bsub>ty\\<^esub>\<^isub>i"} stand for properties defined over the types @{text "ty\\<^isub>1 \ ty\\<^isub>n"}. The premises of these induction principles look as follows @@ -1540,7 +1540,7 @@ Next we lift the permutation operations defined in \eqref{ceqvt} for the raw term-constructors @{text "C"}. These facts contain, in addition to the term-constructors, also permutation operations. In order to make the - lifting to go through, + lifting go through, we have to know that the permutation operations are respectful w.r.t.~alpha-equivalence. This amounts to showing that the alpha-equivalence relations are equivariant, which we already established @@ -1567,7 +1567,7 @@ \noindent which can be established by induction on @{text "\ty"}. Whereas the first - property is always true by the way how we defined the free-variable + property is always true by the way we defined the free-variable functions for types, the second and third do \emph{not} hold in general. There is, in principle, the possibility that the user defines @{text "bn\<^isub>k"} so that it returns an already bound variable. Then the third property is just not true. However, our @@ -1864,7 +1864,7 @@ \end{center} \noindent - So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \ Let p t\<^isub>1 t\<^isub>2)"}, we are can equally + So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \ Let p t\<^isub>1 t\<^isub>2)"}, we can equally establish \begin{center} @@ -1894,7 +1894,7 @@ 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 strong induction principle derives from the weak induction principle. For the moment we can derive the difficult cases of - the strong induction principles only by hand, but they are very schematically + the strong induction principles only by hand, but they are very schematic so that with little effort we can even derive them for Core-Haskell given in Figure~\ref{nominalcorehas}. *}