[Prev][Next][Index]

The real numbers

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

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

Comments and corrections are welcome.

I have also revised the mathematical sequence stuff;
if anyone is interested I can send you that or make it available also.

	Gary
--
	229 Atanasoff Hall, Department of Computer Science
	Iowa State Univ., Ames, Iowa 50011-1040 USA / leavens@cs.iastate.edu
	phone: (515)294-1580 fax: (515)294-0258 ftp site: ftp.cs.iastate.edu
	URL: http://www.cs.iastate.edu/~leavens/homepage.html
Follow-Up(s):