Accueil     À propos     Téléchargement     Ressources     Contactez-nous

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Compiler feature - useful or not?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2007-11-16 (08:23) From: Andrej Bauer Subject: Re: [Caml-list] Compiler feature - useful or not?
```Christophe TROESTLER wrote:
> I believe Z is generally defined as a quotient of the disjoint union
> (borrowed as variants in programming languages) of N and N
> (identifying the two 0).  Of course you can also define it as a
> quotient of N×N by the smaller equivalent relation "~" s.t. (n,m) ~
> (n+1,m+1) and it is quite nice as addition is "inherited" from the one
> on N×N but I am not sure it is the way it is usually done.

As another mathematician, also prone to nitpicking, I beg to differ. It
is more natural to define Z as a quotient of N x N, because this is just
a special case of a general construction of a (commutative) ring out of
a (commutative) rig.

A rig is a structure with 0, + and * but no subtraction.

A ring is a structure with 0, +, - and *.

(Of course you need to imagine suitable axioms for 0, +, * such as
commutativity, associativity and distributivity, but I am not writing
them down here.)

From every rig M we can construct a ring R as a quotient (M x M)/~ of M
x M where we define

(a,b) ~ (c,d)  iff  a+d = b+c

Think of (a,b) as the "non-existent" difference a-b. This construction
is natural in the technical sense that it is left adjoint to the
forgetful functor(*) from rings to rigs. (In non-mathematician language:
if we already have + and *, there is a _best_ way of getting - as well.)

Caveat: (*) the use of "functor" here was as in mathematics, not as in
ocaml.

In what way is natural, or canonical, the construction of Z defined by
sticking together two copies of N?

To add some value to this post, other than mathematical willy waving,
let me pose a puzzle. Implement the above in Ocaml, i.e., start with:

module type RIG =
sig
type t
val zero : t
val add : t -> t -> t
val mul : t -> t -> t
end

module type RING =
sig
include RIG
val sub : t -> t -> t
end

The puzzle is this: write down the module type for the construction
taking a rig and returning the free ring over it. It is _not_ just

module type ConstructRing = functor (M : RIG) -> RING

because that would allow _any_ ring whatsoever as the result. It has to
be the ring that comes from M via above construction, so there has to be
extra stuff, such as an embedding of M into the resulting R. But what else?

Andrej

```