5.2 Extended Syntax for Numbers

We first discuss two ways to provide a special syntax for numbers. This results in a proposal of how to extend the CASL-Syntax and how to translate this extension back into standard CASL. Finally we demonstrate that the proposed extension on numbers fits with our specifications of numbers in [RM99].

5.2.1 Two Different Approaches

There are basically two ways of providing a special syntax for natural numbers:

First approach:

Introduce a constant for each number, and axiomatize the successor operation by providing one axiom for each number.

The drawback of this approach is that the specification of natural numbers consists of an infinite signature and and infinite number of axioms. There is no difficulty in modifying the CASL semantics to allow such specifications. However, such infinite theories have to be hard-wired into theorem provers. This makes it more difficult to re-use existing theorem provers by building translations from CASL to tool-supported languages.

Second approach:

Translate a numeral into a sequence of digits. Just translating a sequence of digits d₁ d₂...d_n to d₁ d₂ ... d_n would require to introduce the digits as prefix or postfix operations. However, this leads to the peculiarity that 56 78 is the same as 5678. Thus, a better way is to insert operation symbols between the digits. That is, d₁ d₂...d_n is translated to d₁ :: d₂:: ...:: d_n.

The drawback of this approach is that it is not possible to pass a multi-digit number directly as an actual parameter to a generic specification. Instead, one has to introduce an extension of the natural numbers, where the number is named as a constant, and pass this constant to the generic specification⁸.

We propose to adopt the second approach.

5.2.2 Proposal for an Extended Syntax for Numbers

According to section C.4 of [CoF98] we suggest the following extended syntax for numbers:

 Digit	::=	0 | 1 | ... | 9
 Sign	::=	+ | -
 Number	::=	 Digit |  Number  Digit
 Fraction	::=	 Number |  Number .  Number
 Expo	::=	 Fraction E  Number |
		 Fraction E  Sign  Number

The syntax translation [ [ ] ] for this extension into CASL is defined inductively as

• [ [ 0 ] ]:= 0,
• [ [ 1 ] ]:= 1,
• ...
• [ [ 9 ] ]:= 9,
• [ [ + ] ]:= +,
• [ [ - ] ]:= -,
• [ [  Number  Digit ] ]:= [ [  Number ] ] :: [ [  Digit ] ],
• [ [  Number .  Number ] ]:= [ [  Number ] ] ::: [ [  Number ] ] , and
• [ [  Fraction E  Number ] ]:= [ [  Fraction ] ] ' ' E ' ' [ [  Number ] ], where ' ' denotes a space.
• [ [  Fraction E  Sign  Number ] ]:= [ [  Fraction ] ] ' ' E ' ' [ [  Sign ] ] [ [  Number ] ], where ' ' denotes a space.

• 0, 1, ..., 9,
• +__, -__,
• __ :: __, __ ::: __, and __ E __

5.2.3 Representation of Numbers in Notes M-6 and M-7

Natural numbers are represented in [RM99] as sequences of digits d₁ :: d₂:: ...:: d_n. This representation carries over to integers, where we add a sign to the numbers, and rational numbers, which are represented as a pair of an integer and a positive number. For finite decimal fractions we provide a special notion, which makes use of the operator __E__. Real numbers are defined in [MR99] as a supersort of rational numbers and need therefore no new representation. The same holds for the specification of complex numbers of [MR99].

Natural Numbers:

The representations of natural numbers is specified in [RM99] as follows:

spec

Nat =

GenerateNat with sorts Nat, Pos, ops 0, suc, pre

then

...

ops

1,2,3,4,5,6,7,8,9:	Nat;
__ :: __ :	Nat × Nat -> Nat %left assoc

%%

representing the natural numbers with digits:

.

1 = suc (0)

.

2 = suc (1)

.

3 = suc (2)

.

4 = suc (3)

.

5 = suc (4)

.

6 = suc (5)

.

7 = suc (6)

.

8 = suc (7)

.

9 = suc (8)

.

m :: n = (m * suc(9)) + n

end

Integers:

The syntax for integers is derived from the above syntax of natural numbers by introducing + (unary) and - (unary) as operation symbols:

spec

Int =

GenerateInt with sorts Nat, Pos, Neg, Int ops 0, suc, pre

then

...

ops

+__,
-__:	Int -> Int;

end

Rational Numbers:

The representation for rationals in [RM99] is obtained by operators +__ (unary), -__ (unary), and __/__ (binary):

spec

GenerateRat =

Int ...

then

free

{

type

Rat ::= sort Int | __ / __ (nom: Int ; denom: Pos)

...

}

end

spec

Rat =

GenerateRat ...

then

...

ops

+ __ ,
- __ :	Rat -> Rat;

end

For the representation of a subset of the rational numbers, the finite decimal fractions, we further introduce operations __:::__ and __E__ in [RM99]:

spec

Rat =

...

ops

__ ::: __ :	Nat × Nat -> Rat;
__ E __ :	Rat × Int -> Rat

vars

n,m: Nat; p: Pos

%%

represent the floating point number n.m as rational:

.

n:::m = n + (m/tenPower(m))

%%

introduce an exponent:

.

r E n = r* ((1::0) ^ n)

.

r E (-p) = r / ((1::0) ^ n)

end

Real Numbers:

The representation of the real numbers is the same as for rational numbers resp. finite decimal fractions: in [MR99] the sort Real is defined as supersort of Rat:

spec

DefineBasicReal =

ArchimedianField[DefineArchimedianField] with Elem ^_|-> Real and Rat

then

sort

Rat < Real

%%

The embedding is determined by overloading of 0,1,+,_,*,/

...

end

spec

BasicReal[DefineBasicReal] =

...

ops

pi,
e :	Real;

axioms

e = exp(1)

pi = 4*arcsin(sqrt(1/2))

...

end

Complex Numbers:

Complex numbers are specified in [MR99] as pairs of two real numbers. Thus again the representations for rational numbers resp. finite decimal fractions carry over and there is no need for further special syntax. The complex number i and the operator __ i, which denotes the imaginary part of a complex number, are obtained by overloading.

spec

BasicComplex =

BasicReal

then

free

type Complex ::= c(real,imag: Real)

sorts

Real < Complex

ops

i :	Complex;
__ i :	Real -> Complex;
...

axiom

i = c(0,1)

var

x: Real

.

x i = c(0,x)

...

end