Number Systems

Number Systems: Concepts, Issues, and Designs

Number Systems: Index

Natural Numbers
Integers
Rationals
Reals
Natural Numbers
Note: NAT is a primeval (or: built-in) spec: you can refer to the sort Nat and the various operations, but you cannot refer to the NAT spec itself.

Constructors are: zero and succ
Other operations are: one, two,nonzero?, pred, lt, leq, gt, geq, plus, times, and minus
Spec for natural numbers
is in: nat.re
Higher-order iteration on nats
foldl for nats and booleans (with "early-stop" versions). Also, universal and existential quantifiers on ranges of nats. Spec is in : nat-ho.re
Also, see higher-order-specs
Integers
Integers in algebraic form
The integers are presented as the cannonical ordered integral-domain. The integer spec is in: integer.re
integral-domain
  • Commutative ring with unit (one)
  • Nontrivial: (not (zero = one))
  • Cancellation for times
  • Spec is in: abstract-algebra.re
ordering
There are at least two possibilities:
  • Axiomatize pos?
  • Use STRICT-SIMPLE-ORDER and use the following axioms to relate the order to plus and times:
    • (implies (lt x y) (lt (plus x z)(plus y z)))
    • (implies (and (lt x y)(lt zero z)) (lt (times x z)(items y z)))
  • The current version uses ordering axioms and defines pos?
Integers as quotient of NAT, NAT wrt Subtraction equivalence
The equivalence relation is:
(iff (subtract-equiv? n2 m2>) (equal (minus n1 m1) (minus n2 m2)))
Integers are then interpreted as equivalence classes of subtract-equiv pairs. Spec is in : integer-to-nat.re
Rationals
Rationals as quotient on Nat, Nonzero-Nat
See Interpreting sorts: subsort of product vs product of subsorts.
Spec is in: rational-spec.re
Reals
Spec for reals
The Reals are specified via the canonical presentation as a complete ordered field. Completeness can be expressed in a variety of ways. The simplest in abstract terms is the existence of least upper bounds (greatest lower bounds) for sets of rationals bounded above (below) (which actually requires a more sophisticated version of sets than is available in the current library). The current version uses greatest lower bounds. Spec is in: real-spec.re
Interpretation of Reals as equivalence classes of Cauchy sequences.
Basic idea is that Cauchy seqs are equivalent if they converge to the same limit.
Cauchy Seqs
Spec is in: cauchy-seq.re
Ordered-field to Cauchy Seqs
Spec is in: ordered-field-to-cauchy-seq.re
Complete-Order to Cauchy Seqs
Spec is planned.
Computable Reals, Floating Point Numbers, etc
Is: Future...
SpecWeb Index Specs