# HG changeset patch # User Christian Urban # Date 1276160031 -7200 # Node ID fc5bfd0cc1cda117bde99798b8418cee3e35c05c # Parent 1a9dbfe04f7d0f00f788ebdb809263c9a99ebd5e more on the qpaper diff -r 1a9dbfe04f7d -r fc5bfd0cc1cd Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Mon Jun 07 16:17:35 2010 +0200 +++ b/Quotient-Paper/Paper.thy Thu Jun 10 10:53:51 2010 +0200 @@ -10,17 +10,16 @@ print_syntax notation (latex output) - rel_conj ("_ OOO _" [53, 53] 52) -and - "op -->" (infix "\" 100) -and - "==>" (infix "\" 100) -and - fun_map (infix "\" 51) -and - fun_rel (infix "\" 51) -and - list_eq (infix "\" 50) (* Not sure if we want this notation...? *) + rel_conj ("_ OOO _" [53, 53] 52) and + "op -->" (infix "\" 100) and + "==>" (infix "\" 100) and + fun_map (infix "\" 51) and + fun_rel (infix "\" 51) and + list_eq (infix "\" 50) and (* Not sure if we want this notation...? *) + fempty ("\\<^isub>f") and + funion ("_ \\<^isub>f _") and + Cons ("_::_") + ML {* fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n; @@ -57,7 +56,7 @@ 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 to use both mechanisms for dealing with quotient constructions in + 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 \ nat"} and the equivalence relation @@ -65,11 +64,11 @@ @{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \ (m\<^isub>1, m\<^isub>2) \ n\<^isub>1 + n\<^isub>2 = m\<^isub>1 + m\<^isub>2"} \noindent - This constructions yields the type @{typ int} and definitions for @{text - "0::int"} and @{text "1::int"} in terms of pairs of natural numbers can be - given (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations such as - @{text "add"} with type @{typ "int \ int \ int"} can be defined in terms of operations on - pairs of natural numbers (namely @{text "add\<^bsub>nat\nat\<^esub> + 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 \ int \ int"} can be defined + in terms of operations on pairs of natural numbers (namely @{text "add\<^bsub>nat\nat\<^esub> (x\<^isub>1, y\<^isub>1) (x\<^isub>2, y\<^isub>2) \ (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 @@ -79,13 +78,32 @@ \noindent which states that two lists are equivalent if every element in one list is also - member in the other (@{text "\"} stands here for membership in lists). + member in the other (@{text "\"} 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 "\\<^isub>f"}, as list append. + + Another important area of quotients is reasoning about programming language + calculi. A simple example are lambda-terms defined as + + \begin{center} + @{text "t ::= x | t t | \x.t"} + \end{center} - The problem is that in order to be able to reason about integers and - finite sets, one needs to establish a reasoning infrastructure by + \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. + + + 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 \ nat"} to the quotient type @{typ int} (similarly for - @{text "\ list"} and finite sets of type @{text "\"}). This lifting usually + @{text "\ list"} and finite sets of type @{text "\"}, 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 diff -r 1a9dbfe04f7d -r fc5bfd0cc1cd Quotient-Paper/document/root.tex --- a/Quotient-Paper/document/root.tex Mon Jun 07 16:17:35 2010 +0200 +++ b/Quotient-Paper/document/root.tex Thu Jun 10 10:53:51 2010 +0200 @@ -33,7 +33,7 @@ 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 were able to specify completely the procedure of lifting theorems from +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.