# HG changeset patch # User Christian Urban # Date 1276335156 -7200 # Node ID 36c9d9e658c756dc0c9a2f5658b8acd9f85e9c05 # Parent cbffed7d81bdf53024ab1c8cbe11a2ca3a43cf8e some slight tuning of the intro diff -r cbffed7d81bd -r 36c9d9e658c7 Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Sat Jun 12 06:35:27 2010 +0200 +++ b/Quotient-Paper/Paper.thy Sat Jun 12 11:32:36 2010 +0200 @@ -85,7 +85,7 @@ @{text "\"}, as list append. An area where quotients are ubiquitous is reasoning about programming language - calculi. A simple example is the lambda-calculus, whose ``raw'' terms are defined as + calculi. A simple example is the lambda-calculus, whose raw terms are defined as @{text [display, indent=10] "t ::= x | t t | \x.t"} @@ -94,7 +94,7 @@ prove formally, for example, the substitution lemma \cite{Barendregt81} by induction over the structure of terms. This can be fiendishly complicated (see \cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof - about ``raw'' lambda-terms). In contrast, if we reason about + about raw lambda-terms). In contrast, if we reason about $\alpha$-equated lambda-terms, that means terms quotient according to $\alpha$-equivalence, then the reasoning infrastructure provided, for example, by Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal @@ -103,7 +103,7 @@ The difficulty is that in order to be able to reason about integers, finite sets or $\alpha$-equated lambda-terms one needs to establish a reasoning infrastructure by transferring, or \emph{lifting}, definitions and theorems - from the ``raw'' type @{typ "nat \ nat"} to the quotient type @{typ int} + from the raw type @{typ "nat \ nat"} to the quotient type @{typ int} (similarly for finite sets and $\alpha$-equated lambda-terms). This lifting usually requires a \emph{lot} of tedious reasoning effort \cite{Paulson06}. It is feasible to to this work manually, if one has only a few quotient @@ -143,13 +143,16 @@ \end{center} \noindent - The starting point is an existing type over which an equivalence relation - given by the user is defined. With this input the package introduces a new - type that comes with associated \emph{abstraction} and \emph{representation} - functions, written @{text Abs} and @{text Rep}. These functions relate - elements in the existing type to ones in the new type and vice versa; they - can be uniquely identified by their type. For example for the integer - quotient construction the types of @{text Abs} and @{text Rep} are + The starting point is an existing type, often referred to as the + \emph{raw level}, over which an equivalence relation given by the user is + defined. With this input the package introduces a new type, to which we + refer as the \emph{quotient level}. This type comes with an + \emph{abstraction} and a \emph{representation} function, written @{text Abs} + and @{text Rep}. These functions relate elements in the existing type to + ones in the new type and vice versa; they can be uniquely identified by + their type. For example for the integer quotient construction the types of + @{text Abs} and @{text Rep} are + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @{text "Abs::nat \ nat \ int"}\hspace{10mm}@{text "Rep::int \ nat \ nat"} @@ -157,7 +160,7 @@ \noindent However we often leave this typing information implicit for better - readability. Every abstraction and representation function represents an + readability. Every abstraction and representation function stands for an isomorphism between the non-empty subset and elements in the new type. They are necessary for making definitions involving the new type. For example @{text "0"} and @{text "1"} of type @{typ int} can be defined as @@ -175,13 +178,13 @@ \noindent where we take the representation of the arguments @{text n} and @{text m}, - add them according to @{text "add_pair"} and then take the + add them according to the function @{text "add_pair"} and then take the abstraction of the result. This is all straightforward and the existing quotient packages can deal with such definitions. But what is surprising that none of them can deal with slightly more complicated definitions involving \emph{compositions} of quotients. Such compositions are needed for example - in case of quotienting lists and the operator that flattens lists of lists, defined - as follows + in case of quotienting lists to obtain finite sets and the operator that + flattens lists of lists, defined as follows @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]} @@ -195,7 +198,7 @@ The quotient package should provide us with a definition for @{text "\"} in terms of @{text flat}, @{text Rep} and @{text Abs} (the latter two having the type @{text "\ fset \ \ list"} and @{text "\ list \ \ fset"}, - respectively). The problem is that the method is used in the existing quotient + respectively). The problem is that the method used in the existing quotient packages of just taking the representation of the arguments and then take the abstraction of the result is \emph{not} enough. The reason is that case in case of @{text "\"} we obtain the incorrect definition @@ -205,7 +208,7 @@ \noindent where the right-hand side is not even typable! This problem can be remedied in the existing quotient packages by introducing an intermediate step and reasoning - about faltening of lists of finite sets. However, this remedy is rather + about flattening of lists of finite sets. However, this remedy is rather cumbersome and inelegant in light of our work, which can deal with such definitions directly. The solution is that we need to build aggregate representation and abstraction functions, which in case of @{text "\"} @@ -218,14 +221,14 @@ will present a formal definition of our aggregate abstraction and representation functions (this definition was omitted in \cite{Homeier05}). They generate definitions, like the one above for @{text "\"}, - according to the type of the ``raw'' constant and the type + according to the type of the raw constant and the type of the quotient constant. This means we also have to extend the notions of \emph{respectfulness} and \emph{preservation} from Homeier \cite{Homeier05}. We will also address the criticism by Paulson \cite{Paulson06} cited at the beginning of this section about having to collect theorems that are lifted from the raw - level to the quotient level. Our quotient package is modular so that it + level to the quotient level. Our quotient package id the first one that is modular so that it allows to lift single theorems separately. This has the advantage for the user to develop a formal theory interactively an a natural progression. A pleasing result of the modularity is also that we are able to clearly diff -r cbffed7d81bd -r 36c9d9e658c7 Quotient-Paper/document/root.bib --- a/Quotient-Paper/document/root.bib Sat Jun 12 06:35:27 2010 +0200 +++ b/Quotient-Paper/document/root.bib Sat Jun 12 11:32:36 2010 +0200 @@ -37,7 +37,7 @@ author = {Laurent Chicli and Loic Pottier and Carlos Simpson}, - title = {Mathematical Quotients and Quotient Types in Coq}, + title = {{M}athematical {Q}uotients and {Q}uotient {T}ypes in {C}oq}, booktitle = {TYPES}, year = {2002}, pages = {95-107}, diff -r cbffed7d81bd -r 36c9d9e658c7 Quotient-Paper/document/root.tex --- a/Quotient-Paper/document/root.tex Sat Jun 12 06:35:27 2010 +0200 +++ b/Quotient-Paper/document/root.tex Sat Jun 12 11:32:36 2010 +0200 @@ -37,7 +37,7 @@ the procedure of lifting theorems from the raw level to the quotient level. The importance for programming language research is that many properties of programming language calculi are easier to verify over $\alpha$-equated, or -$\alpha$-quotient, terms, than over ``raw'' terms. +$\alpha$-quotient, terms, than over raw terms. \end{abstract} % generated text of all theories