# HG changeset patch # User Christian Urban # Date 1277945580 -3600 # Node ID f296ef291ca9a974f5e646d89a8abbd4194253dd # Parent f659ce282610b62c785f6e05b510ced1a976c1f0 spell check diff -r f659ce282610 -r f296ef291ca9 Paper/Paper.thy --- a/Paper/Paper.thy Wed Jun 30 16:56:37 2010 +0100 +++ b/Paper/Paper.thy Thu Jul 01 01:53:00 2010 +0100 @@ -853,7 +853,7 @@ the definitions for $\alpha$-equivalence will help us in the next section. *} -section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *} +section {* Specifying General Binders\label{sec:spec} *} text {* Our choice of syntax for specifications is influenced by the existing @@ -945,7 +945,7 @@ of the specifications (the corresponding $\alpha$-equivalence will differ). We will show this later with an example. - There are some restrictions we need to impose on binding clasues: the main idea behind + There are 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 a bound variable cannot be free at the same time. First, a body can only occur in \emph{one} binding clause of a term constructor (this ensures @@ -1121,7 +1121,11 @@ \noindent The point of completion is that we can make definitions over the binding clauses and be sure to have captured all arguments of a term constructor. +*} +section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *} + +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 @@ -1185,7 +1189,7 @@ bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function that calculates those unbound atoms. - For atomic types we define the auxilary + For atomic types we define the auxiliary free variable functions: \begin{center} @@ -1285,7 +1289,7 @@ \noindent Since there are only (implicit) empty binding clauses for the term-constructors @{text ANil} and @{text "ACons"}, the corresponding free-variable function @{text - "fv\<^bsub>assn\<^esub>"} returns all atoms occuring in an assignment. The + "fv\<^bsub>assn\<^esub>"} returns all atoms occurring in an assignment. The binding only takes place in @{text Let} and @{text "Let_rec"}. In the @{text "Let"}-clause we want to bind all atoms given by @{text "set (bn as)"} in @{text t}. Therefore we have to subtract @{text "set (bn as)"} from @{text @@ -1915,7 +1919,7 @@ section {* Related Work *} text {* - To our knowledge, the earliest usage of general binders in a theorem prover + To our knowledge the earliest usage of general binders in a theorem prover is described in \cite{NaraschewskiNipkow99} about a formalisation of the algorithm W. This formalisation implements binding in type schemes using a de-Bruijn indices representation. Since type schemes of W contain only a single @@ -1926,7 +1930,7 @@ of two numbers, one referring to the place where a variable is bound and the other to which variable is bound. The reasoning infrastructure for both representations of bindings comes for free in theorem provers like Isabelle/HOL or - Coq, as the corresponding term-calculi can be implemented as ``normal'' + Coq, since the corresponding term-calculi can be implemented as ``normal'' 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 @@ -1937,7 +1941,7 @@ Another representation technique for binding is higher-order abstract syntax (HOAS), which for example is implemented in the Twelf system. This representation technique supports very elegantly many aspects of \emph{single} binding, and - impressive work is in progress that uses HOAS for mechanising the metatheory + impressive work has been done that uses HOAS for mechanising the metatheory of SML~\cite{LeeCraryHarper07}. We are, however, not aware how multiple binders of SML are represented in this work. Judging from the submitted Twelf-solution for the POPLmark challenge, HOAS cannot easily deal with @@ -1948,7 +1952,7 @@ all the unwanted consequences when reasoning about the resulting terms. Two formalisations involving general binders have also been performed in older - versions of Nominal Isabelle (one about Psi-calculi and one about alpgorithm W + versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W \cite{BengtsonParow09, UrbanNipkow09}). Both use the approach based on iterated single binders. Our experience with the latter formalisation has been disappointing. The major pain arose from @@ -2054,7 +2058,7 @@ $\alpha$-equivalence related to our binding mode \isacommand{bind\_res}. This definition is similar to the one by Pottier, except that it has a more operational flavour and calculates a partial (renaming) map. - In this way they can handle vacous binders. However, their notion of + In this way they can handle vacuous binders. However, their notion of equality between terms also includes rules for $\beta$ and to our knowledge no concrete mathematical result concerning their notion of equality has been proved. @@ -2115,14 +2119,12 @@ \medskip \noindent {\bf Acknowledgements:} We are very grateful to Andrew Pitts for - many discussions about Nominal Isabelle. We thank Peter Sewell for + many discussions about Nominal Isabelle. We also thank Peter Sewell for making the informal notes \cite{SewellBestiary} available to us and - also for patiently explaining some of the finer points of the work on the Ott-tool. We - also thank Stephanie Weirich for suggesting to separate the subgrammars + also for patiently explaining some of the finer points of the work on the Ott-tool. + Stephanie Weirich suggested to separate the subgrammars of kinds and types in our Core-Haskell example. - - * Conference of Altenkirch * *} (*<*) diff -r f659ce282610 -r f296ef291ca9 Paper/document/root.bib --- a/Paper/document/root.bib Wed Jun 30 16:56:37 2010 +0100 +++ b/Paper/document/root.bib Thu Jul 01 01:53:00 2010 +0100 @@ -1,6 +1,7 @@ @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}, + booktitle = "Proc.~of the 10th FLOPS Conference", year = 2010, series = "LNCS", pages = "40--55", diff -r f659ce282610 -r f296ef291ca9 Paper/document/root.tex --- a/Paper/document/root.tex Wed Jun 30 16:56:37 2010 +0100 +++ b/Paper/document/root.tex Thu Jul 01 01:53:00 2010 +0100 @@ -80,7 +80,7 @@ convention already built in. \end{abstract} -\category{CR-number}{subcategory}{third-level} +%\category{F.4.1}{subcategory}{third-level} \terms formal reasoning, programming language calculi