more to the introduction of the qpaper
authorChristian Urban <urbanc@in.tum.de>
Fri, 11 Jun 2010 14:04:58 +0200
changeset 2220 2c4c0d93daa6
parent 2219 dff64b2e7ec3
child 2221 e749cefbf66c
more to the introduction of the qpaper
Quotient-Paper/Paper.thy
Quotient-Paper/document/root.bib
Quotient-Paper/document/root.tex
--- a/Quotient-Paper/Paper.thy	Thu Jun 10 13:37:32 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Fri Jun 11 14:04:58 2010 +0200
@@ -7,8 +7,6 @@
         "../Nominal/FSet"
 begin
 
-print_syntax
-
 notation (latex output)
   rel_conj ("_ OOO _" [53, 53] 52) and
   "op -->" (infix "\<rightarrow>" 100) and
@@ -18,7 +16,9 @@
   list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
   fempty ("\<emptyset>\<^isub>f") and
   funion ("_ \<union>\<^isub>f _") and
+  finsert ("{_} \<union>\<^isub>f _") and 
   Cons ("_::_") 
+ 
   
 
 ML {*
@@ -49,86 +49,101 @@
   \end{flushright}\smallskip
 
   \noindent
-  Isabelle is a generic theorem prover in which many logics can be
+  Isabelle is a popular generic theorem prover in which many logics can be
   implemented. The most widely used one, however, is Higher-Order Logic
   (HOL). This logic consists of a small number of axioms and inference rules
   over a simply-typed term-language. Safe reasoning in HOL is ensured by two
   very restricted mechanisms for extending the logic: one is the definition of
   new constants in terms of existing ones; the other is the introduction of
   new types by identifying non-empty subsets in existing types. It is well
-  understood how to use both mechanisms for dealing with quotient constructions in
-  HOL (see \cite{Homeier05,Paulson06}).  For example the integers
-  in Isabelle/HOL are constructed by a quotient construction over the type
-  @{typ "nat \<times> nat"} and the equivalence relation
+  understood how to use both mechanisms for dealing with quotient
+  constructions in HOL (see \cite{Homeier05,Paulson06}).  For example the
+  integers in Isabelle/HOL are constructed by a quotient construction over the
+  type @{typ "nat \<times> nat"} and the equivalence relation
 
   @{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + n\<^isub>2 = m\<^isub>1 + m\<^isub>2"}
 
   \noindent
   This constructions yields the new type @{typ int} and definitions for @{text
-  "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of 
-  natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations 
-  such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined 
-  in terms of operations on pairs of natural numbers (namely @{text "add\<^bsub>nat\<times>nat\<^esub>
-  (x\<^isub>1, y\<^isub>1) (x\<^isub>2, y\<^isub>2) \<equiv> (x\<^isub>1 +
-  x\<^isub>2, y\<^isub>1 + y\<^isub>2)"}).  Similarly one can construct the
-  type of finite sets by quotienting lists according to the equivalence
-  relation
+  "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of
+  natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations
+  such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in
+  terms of operations on pairs of natural numbers (namely @{text
+  "add\<^bsub>nat\<times>nat\<^esub> (x\<^isub>1, y\<^isub>1) (x\<^isub>2,
+  y\<^isub>2) \<equiv> (x\<^isub>1 + x\<^isub>2, y\<^isub>1 + y\<^isub>2)"}).
+  Similarly one can construct the type of finite sets by quotienting lists
+  according to the equivalence relation
 
   @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}
 
   \noindent
   which states that two lists are equivalent if every element in one list is also
   member in the other (@{text "\<in>"} stands here for membership in lists). The
-  empty finite set, written @{term "{||}"} can then be defined as the 
-  empty list and union of two finite sets, written @{text "\<union>\<^isub>f"}, as list append. 
+  empty finite set, written @{term "{||}"}, can then be defined as the 
+  empty list and the union of two finite sets, written @{text "\<union>\<^isub>f"}, 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
+
+  @{text [display, indent=10] "t ::= x | t t | \<lambda>x.t"}
 
-  Another important area of quotients is reasoning about programming language
-  calculi. A simple example are lambda-terms defined as
+  \noindent
+  The problem with this definition arises when one, for example, attempts to
+  prove formally the substitution lemma \cite{Barendregt81} by induction
+  ove 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
+  $\alpha$-equated lambda-terms, that means terms quotient according to
+  $\alpha$-equivalence, then the reasoning infrastructure provided by, 
+  for example, Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal 
+  proof of the substitution lemma almost trivial.
+
+  The difficulty is that in order to be able to reason about integers, finite
+  sets and $\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 \<times> 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.  The purpose of a
+  \emph{quotient package} is to ease the lifting and automate the reasoning as
+  much as possible. 
 
   \begin{center}
-  @{text "t ::= x | t t | \<lambda>x.t"}
-  \end{center}
+  \mbox{}\hspace{20mm}\begin{tikzpicture}
+  %%\draw[step=2mm] (-4,-1) grid (4,1);
+  
+  \draw[very thick] (0.7,0.3) circle (4.85mm);
+  \draw[rounded corners=1mm, very thick] ( 0.0,-0.9) rectangle ( 1.8, 0.9);
+  \draw[rounded corners=1mm, very thick] (-1.95,0.8) rectangle (-2.9,-0.195);
+  
+  \draw (-2.0, 0.8) --  (0.7,0.8);
+  \draw (-2.0,-0.195)  -- (0.7,-0.195);
 
-  \noindent
-  The difficulty with this definition of lambda-terms arises when, for 
-  example, proving formally the substitution lemma ...
-  On the other hand if we reason about alpha-equated lambda-terms, that means
-  terms quotient according to alpha-equivalence, then reasoning infrastructure
-  can be introduced that make the formal proof of the substitution lemma
-  almost trivial. 
+  \draw ( 0.7, 0.23) node {\begin{tabular}{@ {}c@ {}}equiv-\\[-1mm]clas.\end{tabular}};
+  \draw (-2.45, 0.35) node {\begin{tabular}{@ {}c@ {}}new\\[-1mm]type\end{tabular}};
+  \draw (1.8, 0.35) node[right=-0.1mm]
+    {\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};
+  \draw (0.9, -0.55) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
+  
+  \draw[->, very thick] (-1.8, 0.36) -- (-0.1,0.36);
+  \draw[<-, very thick] (-1.8, 0.16) -- (-0.1,0.16);
+  \draw (-0.95, 0.26) node[above=0.4mm] {Rep};
+  \draw (-0.95, 0.26) node[below=0.4mm] {Abs};
+
+  \end{tikzpicture}
+  \end{center}
 
 
-  The problem is that in order to be able to reason about integers, finite sets
-  and 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 \<times> nat"} to the quotient type @{typ int} (similarly for
-  @{text "\<alpha> list"} and finite sets of type @{text "\<alpha>"}, and also for raw lambda-terms
-  and alpha-equated lambda-terms). This lifting usually
-  requires a \emph{lot} of tedious reasoning effort.  The purpose of a \emph{quotient
-  package} is to ease the lifting and automate the reasoning as much as
-  possible. While for integers and finite sets teh tedious reasoning needs
-  to be done only once, Nominal Isabelle providing a reasoning infrastructure 
-  for binders and @{text "\<alpha>"}-equated terms it needs to be done over and over 
-  again.
-
-  Such a package is a central component of the new version of
-  Nominal Isabelle where representations of alpha-equated terms are
-  constructed according to specifications given by the user.
-
-  
   In the context of HOL, there have been several quotient packages (...). The
   most notable is the one by Homeier (...) implemented in HOL4. However, what is
   surprising, none of them can deal compositions of quotients, for example with 
   lifting theorems about @{text "concat"}:
 
-  @{thm [display] concat.simps(1)}
-  @{thm [display] concat.simps(2)[no_vars]}
+  @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]}
 
   \noindent
   One would like to lift this definition to the operation:
 
-  @{thm [display] fconcat_empty[no_vars]}
-  @{thm [display] fconcat_insert[no_vars]}
+  @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
 
   \noindent
   What is special about this operation is that we have as input
--- a/Quotient-Paper/document/root.bib	Thu Jun 10 13:37:32 2010 +0200
+++ b/Quotient-Paper/document/root.bib	Fri Jun 11 14:04:58 2010 +0200
@@ -128,4 +128,30 @@
         author          = "John Harrison",
         title           = "Theorem Proving with the Real Numbers",
         publisher       = "Springer-Verlag",
-        year            = 1998}
\ No newline at end of file
+        year            = 1998}
+
+@BOOK{Barendregt81,
+  AUTHOR = 	 "H.~Barendregt",
+  TITLE = 	 "{T}he {L}ambda {C}alculus: {I}ts {S}yntax and {S}emantics",
+  PUBLISHER = 	 "North-Holland",
+  YEAR = 	 1981,
+  VOLUME = 	 103,
+  SERIES = 	 "Studies in Logic and the Foundations of Mathematics"
+}
+
+@BOOK{CurryFeys58,
+  AUTHOR = 	 "H.~B.~Curry and R.~Feys",
+  TITLE = 	 "{C}ombinatory {L}ogic",
+  PUBLISHER =    "North-Holland",
+  YEAR = 	 "1958",
+  VOLUME =       1,
+  SERIES =       "Studies in Logic and the Foundations of Mathematics"
+}
+
+@Unpublished{UrbanKaliszyk11,
+  author = 	 {C.~Urban and C.~Kaliszyk},
+  title = 	 {{G}eneral {B}indings and {A}lpha-{E}quivalence in {N}ominal {I}sabelle},
+  note = 	 {submitted for publication},
+  month =	 {July},
+  year =	 {2010},
+}
\ No newline at end of file
--- a/Quotient-Paper/document/root.tex	Thu Jun 10 13:37:32 2010 +0200
+++ b/Quotient-Paper/document/root.tex	Fri Jun 11 14:04:58 2010 +0200
@@ -6,7 +6,8 @@
 \usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage{pdfsetup}
-
+\usepackage{tikz}
+\usepackage{pgf}
 
 \urlstyle{rm}
 \isabellestyle{it}
@@ -24,19 +25,18 @@
 \maketitle
 
 \begin{abstract}
-Higher-order logic (HOL), used in a number of theorem provers, is based on a small
-logic kernel, whose only mechanism for extension is the introduction of safe
-definitions and non-empty types. Both extensions are often performed by
-quotient constructions; for example finite sets are constructed by quotienting
-lists, or integers by quotienting pairs of natural numbers. To ease the work
-involved with quotient constructions, we re-implemented in Isabelle/HOL the
-quotient package by Homeier. In doing so we extended his work in order to deal
-with compositions of quotients. Also, we designed our quotient package so that
-every step in a quotient construction can be performed separately and as a
-result we were able to specify completely the procedure of lifting theorems from
-the raw level to the quotient level.  The importance to programming language
-research is that many properties of programming languages are more convenient
-to verify over $\alpha$-quotient terms, than over raw terms.
+Higher-Order Logic (HOL) is based on a small logic kernel, whose only
+mechanism for extension is the introduction of safe definitions and of
+non-empty types. Both extensions are often performed in quotient
+constructions. To ease the work involved with such quotient constructions, we
+re-implemented in Isabelle/HOL the quotient package by Homeier. In doing so we
+extended his work in order to deal with compositions of quotients. Also, we
+designed our quotient package so that every step in a quotient construction
+can be performed separately and as a result we were able to specify completely
+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.
 \end{abstract}
 
 % generated text of all theories