[Prev][Next][Index]

# The real numbers

• Subject: The real numbers
• From: leavens@cs.iastate.edu (Gary Leavens)
• Date: 17 Nov 95 00:16:46 GMT
• Keywords: reals, LSL, specification
• Newsgroups: comp.specification.larch
• Organization: Iowa State University, Ames, Iowa
• Summary: the real numbers specified as a real closed field

```This message presents a fairly snappy specification of the real numbers
in LSL.  Many thanks to Steve Garland for his ideas on how to specify
this, which I essentially only recorded here.  I am responsible for
any errors, and would appreciate corrections.  Also if you know any
implications that should be stated in the traits Real and RealClosedField,
please let me know, as I've had a hard time trying to think of any
(this being a bit far from my expretise!).

The traits (that are not in Guttag and Horning's handbook)
are structured as follows.

Polynomials     RingSugars
|              |
RealClosedField FieldSugars
\  /
Real
|
RealConversions

The Polynomial trait is the subject of an earlier message.
All the other traits (not in the Guttag and Horning handbook)
appear below.  The trait Real is the main one...

% @(#)\$Id: Real.lsl,v 1.2 1995/09/22 05:24:41 leavens Exp leavens \$

% The real numbers.

% Thanks to Steve Garland for pointing out how to do this,
% by noting that Tarski showed that the first-order theory of the
% reals is equivalent to the theory of real closed fields
% of characteristic zero.

Real: trait

includes RealClosedField, Natural(Nat for N),
MinMax(R), FieldSugars(R for T)

introduces
natToReal: Nat -> R

asserts
\forall n: Nat
natToReal(0) == 0;
natToReal(succ(n)) == natToReal(n) + 1;

implies
Field(R for T), TotalOrder(R for T)
\forall q,r,x,y,z: R
(x < y) => (\E z (x < z /\ z < y));
converts natToReal

% @(#)\$Id: RealClosedField.lsl,v 1.3 1995/09/22 22:38:43 leavens Exp leavens \$

% Thanks to Steve Garland for guidance on how to specify this.

RealClosedField: trait

includes Field(R for T), TotalOrder(R for T),
Polynomial(R,
zero_poly for 0: -> Poly[C],
unit_poly for 1: -> Poly[C])

asserts
\forall x,y,z: R, p: Poly[R]

(x < y) => (x + z) < (y + z);
(0 < x /\ 0 < y) => 0 < (x * y);

(0 < x) => (\E y (x = y * y));

(mod(degree(p), 2) = 1) => (\E y (evaluate(p, y) = 0));

% @(#)\$Id: FieldSugars.lsl,v 1.1 1995/11/16 19:57:26 leavens Exp leavens \$

FieldSugars: trait

assumes Field, TotalOrder

includes RingSugars

introduces
__ / __: T, T -> T

asserts
\forall x,y: T
x / y == x * (y\inv);

implies
\forall x,y: T
y > 0 => (y * (1/y) = 1);

% @(#)\$Id: RingSugars.lsl,v 1.1 1995/11/16 22:17:35 leavens Exp leavens \$

RingSugars: trait

assumes Ring

introduces
__ - __: T, T -> T

asserts
\forall x,y: T
x - y == x + (- y);

% @(#)\$Id: RealConversions.lsl,v 1.1 1995/11/16 23:25:49 leavens Exp leavens \$

% Conversions from other numeric sorts to the reals.

RealConversions: trait

includes Real, Rational

introduces
intToReal: Int -> R
posToReal: P -> R
ratToReal: Q -> R

asserts
\forall i: Int, p: P, q: Q
(intToReal(0:Int)) == 0;
intToReal(succ(i)) == intToReal(i) + 1;
intToReal(pred(i)) == intToReal(i) - 1;
posToReal(p) == intToReal(int(p));
ratToReal(i/p) == intToReal(i) / posToReal(p);

implies
\forall i, i1, i2: Int, p: P, q, q1, q2: Q
posToReal(0:P) == 0;
posToReal(succ(p)) == posToReal(p) + 1;
ratToReal(i/1) == intToReal(i);
ratToReal(i/p) == intToReal(i) * (posToReal(p)\inv);
(i1 <= i2) => intToReal(i1) <= intToReal(i2);
posToReal(p) > 0;
(q1 <= q2) => ratToReal(q1) <= ratToReal(q2);
converts intToReal, posToReal, ratToReal

%%%%%%%%%%%%%