Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?


chronological Thread 
  • From: Milad Niqui <milad AT cs.kun.nl>
  • To: Thery Laurent <thery AT ns.di.univaq.it>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?
  • Date: Fri, 28 Nov 2003 12:59:16 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Thery Laurent wrote:
On Fri, 28 Nov 2003, Milad Niqui wrote:


Our canonical representation is essentialy like your original mkRat, we
 directly encode the unique proof of equlity (Zgcd m n)=1. So you can
consider our representation to be:

m/n -> (Zgcd m n)



Yes but yours does not extract in Ocaml is this true?

No they do.
To be more precise I should have written:

m/n -> (Zgcd m n) before iota-reduction

So we encode the compuatation tree of (Zgcd m n). This can be put in Set
and hence can be extracted to ocaml. That is what we did.

That means we rewrite the division-free Euclid's algorithm

let rec gcd m n =   if n == m then m
                    else if m>n then (gcd (m-n) n)
                         else (gcd m (n-m))

as

let rec gcd' m n = if n == m then ["end"]
else if m>n then ("subtract the denominator from the numerator"::gcd' (m-n) n)
else ("subtract the numerator from the denominator"::gcd' m (n-m))

So you see that we are more interested in how we get the gcd rather than
gcd itself:

# gcd' 9 6;;
- : string list =
["subtract the denominator from the numerator";
 "subtract the numerator from the denominator"; "end"]

#  gcd' 36 24 ;;
- : string list =
["subtract the denominator from the numerator";
 "subtract the numerator from the denominator"; "end"]

Note that although gcd(9,6)<>gcd(36,24) but the gcd' algorithm has the
same computation tree for both of them. From the point of view of gcd'
algorithm, only the ratio of two numbers is important.

Hence since in the computing the gcd' of any pair of numbers we only
perform two operations or halt , we can use a binary sequences to code
that pair of numbers. This gives us the idea to present the set of
positive fractions as this datatype:

Inductive Qpositive : Set :=
   nR: Qpositive ->  Qpositive
 | dL: Qpositive ->  Qpositive
 | One: Qpositive .

In terms of gcd' algorithm, nR stands for "subtract the denominator from
the numerator", dL stands for "subtract the numerator from the
denominator" and One stands for "end".

Alternatively, if we stay in Prop universe, all this can be seens as an
encoding of the unique proof of the equality of (Zgcd m n)=1 for any
irreducible fraction m/n, Because this proof is of the form (refl_equal
Z 1), in which 1 can be replaced by its iota-expansions according to
Zgcd algorithm.



--
Laurent Thery

.



--
Milad Niqui

Computing Science Department,                tel:+31 24 365 2631
University of Nijmegen,                      fax:+31 24 365 2525
P.O.B. 9010,                                 email: 
milad AT cs.kun.nl
6500 GL Nijmegen,                            http://www.cs.kun.nl/~milad
The Netherlands.
==============================================================================================
The University of Nijmegen will be named Radboud University Nijmegen as of September 1st, 2004





Archive powered by MhonArc 2.6.16.

Top of Page