Standard constructive definitions of integers, rationals, and reals?

Question

Natural numbers are defined inductively as (using Coq syntax as an example)

Inductive nat: Set :=
| O: nat
| S: nat -> nat.

Is there a standard way to define integers (and maybe other sets like rationals and reals) constructively?

Answer 1

There are multiple ways to define a mathematical structure, depending on what properties you consider to be the definition. Between equivalent characterizations, which one you take to be the definition and which one you take to be an alternative characterization is not important.

In constructive mathematics, it is preferable to pick a definition that makes constructive reasoning easy. For natural numbers, the basic form of reasoning is induction, which makes the traditional zero-or-successor definition very much suitable. Other sets of numbers don't have such a preference.

When reasoning on quotients, in non-constructive settings, it is common to say “pick a member of the equivalence class”. In a constructive setting, it is necessary to describe how to pick a member. This makes it easier to go with definitions that construct one object for each member of the type, rather than constructing equivalence classes.

For example, to define $\mathbb{Z}$, a mathematician might be happy with equating differences of natural numbers: $$\mathbb{Z} := \mathbb{N}^2 / \{((x,y),(x',y')) \mid x + y' = x' + y\}$$ While this has a tidy feeling to it (no “this or that”), for constructive reasoning, it's simpler if equality of objects coincides with equality of representations, so we might define the relative integers as either a natural number or the negative of a natural number minus one:

Inductive Z1 :=
  | Nonnegative : nat -> Z1   (* ⟦Nonnegative x⟧ = ⟦x⟧ *)
  | Negative : nat -> Z1.     (* ⟦Negative x⟧ = -⟦x⟧-1 *)

However, this definition is oddly asymmetric, which can make it preferable to admit two different representations for zero:

Inductive Z2 :=
  | Nonnegative : nat -> Z2   (* ⟦Nonnegative x⟧ = ⟦x⟧ *)
  | Nonpositive : nat -> Z2.  (* ⟦Nonpostitive x⟧ = -⟦x⟧ *)

Or we can build the relative integers without using the naturals as a building block:

Inductive Pos3 :=
  | I : Pos3                  (* ⟦I⟧ = 1 *)
  | S3 : Pos3 -> Pos3         (* ⟦S3 x⟧ = ⟦x⟧+1 *)
Inductive Z3 :=
  | N3 : Pos3 -> Z3           (* ⟦N3 x⟧ = -⟦x⟧ *)
  | O3 : Z3                   (* ⟦O3⟧ = 0 *)
  | P3 : Pos3 -> Z3           (* ⟦P3 x⟧ = ⟦x⟧ *)

The Coq standard library uses yet another definition: it constructs positive integers from their notation is base 2, as the digit 1 followed by a sequence of digits 0 or 1. It then constructs Z like Z3 from Pos3 above. This definition also has a unique representation for each integer. The choice of using binary notation is not for easier reasoning, but to produce more efficient code when programs are extracted from proofs.

Ease of reasoning is a motivation in picking a definition, but it is never an insurmountable factor. If some construction makes a particular proof easier, one can use that definition in that particular proof, and prove that the construction is equivalent to the other construction that was chosen as the definition originally.

For rational numbers, it's difficult to escape quotients, unless we start from a representation of integers as a product of factors (which makes some fundamental operations such as addition and the total ordering on $\mathbb{N}$ difficult to define). The Coq standard library defines Q as $\mathbb{N} \times \mathbb{N}^*$ (numerator and denominator), and defines an operator =?= to test the equivalence of two elements of Q. This definition is pretty common because that's as simple as it gets.

Real numbers are a whole different kettle of fish because they are not constructible. It is impossible to define the real numbers as an inductive type (all inductive types are denumerable). Instead, any definition of the real numbers has to be axiomatic, i.e. non-constructive. It is possible to construct denumerable subsets of the real numbers; the way to do that depends on what subset you want to construct.

Answer 2

Gilles answer is a good one, except for the paragraph on the real numbers, which is completely false, except for the fact that the real numbers are indeed a different kettle of fish. Because this sort of misinformation seems to be quite widespread, I would like to record here a detailed rebuttal.

It is not true that all inductive types are denumerable. For example, the inductive type

Inductive cow := 
   | nose : cow
   | horn : (nat -> cow) -> cow.

is not denumerable, for given any sequence c : nat -> cow we may form horn c which is not in the sequence by well-foundedness of cattle. If you want a correct statement of the form "all inductive types are countable" you have to severely limit the allowed constructions.

The real numbers cannot be easily constructed as an inductive type, except that in homotopy type theory they can be constructed as a higher inductive-inductive type, see Chapter 11 of the HoTT book. It could be argued that this is cheating.

There are a number of constructive definitions and constructions of the reals, contrary to Gilles claim. They can be broadly divided into two classes:

1. Cauchy-type constructions in which the reals as seen as a metric completion of the rational numbers. This sort of construction often requires quotients, although one may be able to get away with a coiunductive definition, dependig on how one treats equality. A naive construction typically requires countable choice as well, but Fred Richman gave a completion procedure which works constructively without choice, see his Real numbers and other completions.

2. Dedekind-type construction in which the reals are seen as (two-sided) cuts of rationals. This sort of construction usually requires powersets or a similar device, although it is possible to do it just with some basic $\lambda$-calculus and the axiomatization of the Sierpinski space $\Sigma$, see Dedekind reals in Abstract Stone Duality.

On the implementation side, we have various constructive formalizations of reals (but not the one in the Coq standard library which is just awful), for instance Robbert Krebbers's and Bas Spitters's Computer certified efficient exact reals in Coq.

For an actual implementation of exact real numbers I point you to Norbert Müller's iRRAM.

Lastly, Gilles remark about denumerable subsets of reals is off the mark. It is perfectly possible to construct or define uncountable sets, in whatever constructive setting you live. For example, the Baire space $\mathbb{N} \to \mathbb{N}$ of all sequences of numbers is alway uncountable, even if you think that every function is Turing-computable -- see my blog post for an explanation.