[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS] Re: [Hol-info] defining functions on equivalence classes
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
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
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.