[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: Lawrence Paulson <lp15@cam.ac.uk>, pvs@csl.sri.com, hol-info@lists.sourceforge.net, coq-club@pauillac.inria.fr, isabelle-users@cl.cam.ac.uk*Subject*: [PVS] Re: [Hol-info] defining functions on equivalence classes*From*: Rob Arthan <rda@lemma-one.com>*Date*: Sun, 28 Mar 2004 10:35:07 +0000*Cc*: John Harrison <johnh@ichips.intel.com>*In-Reply-To*: <16DA2C32-7BF2-11D8-B830-00039384D4B8@cam.ac.uk>*List-Help*: <mailto:pvs-request@csl.sri.com?subject=help>*List-Id*: PVS <pvs.csl.sri.com>*List-Post*: <mailto:pvs@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs>,<mailto:pvs-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs>,<mailto:pvs-request@csl.sri.com?subject=unsubscribe>*Organization*: Lemma 1 Ltd.*References*: <16DA2C32-7BF2-11D8-B830-00039384D4B8@cam.ac.uk>*Sender*: pvs-bounces+archive=csl.sri.com@csl.sri.com*User-Agent*: KMail/1.5

On Monday 22 Mar 2004 11:14 am, Lawrence Paulson wrote: > How frequently are quotient constructions used in formal proofs? I > think John Harrison used one to construct the rationals, and there are > a couple in Isabelle, but are there others? In ProofPower-HOL, at the moment, the only quotient constructions in building the theory library are to construct the integers (as equivalence classes of pairs of natural numbers) and the reals (as equivalence classes of Dedekind cuts). If you wanted to develop a theory of infinite cardinals in HOL, then it would be natural to define the infinite cardinals, in type 'a, to be the equivalence classes of sets of 'a modulo equinumerosity. On Thursday 25 Mar 2004 6:00 pm, John R Harrison wrote: >... > > In HOL Light, there are two quotient constructions involved in the > construction of the reals, one to factor the space of nearly-additive > functions N->N to yield the positive reals R+, the other to factor > R+^2 as usual to yield signed reals. > > The only other instance of a quotient construction I have is in a port > of Anthony Fox's ARM spec, where they're used to define a type of words, > as Konrad mentioned. > > So a survey of my proofs supports what I guess to be your hypothesis, that > quotient constructions are not used routinely. I think that's true in the HOL world, but isn't that because (a) much of the work on pure mathematics in the various implementations of HOL has concentrated on analysis, and (b), in practical applications, the data is typically sufficiently concrete to let you work with canonical representatives rather than equivalence classes? If you start trying to do much algebra or topology, you are much more likely to need quotient constructions. For example, I've been playing with the beginnings of a ProofPower-HOL theory of elementary algebraic topology recently. Quotient constructions (or more accurately subquotient constructions) are endemic in this. E.g., I can think of no way of defining the fundamental group of a topological space other than as a set of equivalence classes of continuous functions from a circle to the space. Similar thiings would apply if you wanted to develop group theory or ring theory - the three isomorphism theorems are amongst the most important basic tools in these theories and they all involve quotients. So, maybe Larry would get a very different answer if he asked this question in the Mizar world. Regards, Rob.

- Prev by Date:
**[PVS] Re: defining functions on equivalence classes** - Next by Date:
**[PVS] defining functions on equivalence classes** - Prev by thread:
**[PVS] Re: defining functions on equivalence classes** - Next by thread:
**[PVS] defining functions on equivalence classes** - Index(es):