   Go backward to 5.1 Extended Syntax for Functions on Argument Lists
Go up to 5 Syntax Extensions
Go forward to 5.3 Extended Syntax for Characters and Strings

## 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 d1 d2...dn to d1 d2 ... dn 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, d1 d2...dn is translated to d1 :: d2:: ...:: dn.

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 specification8.

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,
• [ [ + ] ]:= +,
• [ [ - ] ]:= -,
• [ [ &nbsp;Number &nbsp;Digit ] ]:= [ [ &nbsp;Number ] ] :: [ [ &nbsp;Digit ] ],
• [ [ &nbsp;Number . &nbsp;Number ] ]:= [ [ &nbsp;Number ] ] ::: [ [ &nbsp;Number ] ] , and
• [ [ &nbsp;Fraction E &nbsp;Number ] ]:= [ [ &nbsp;Fraction ] ] ' ' E ' ' [ [ &nbsp;Number ] ], where ' ' denotes a space.
• [ [ &nbsp;Fraction E &nbsp;Sign &nbsp;Number ] ]:= [ [ &nbsp;Fraction ] ] ' ' E ' ' [ [ &nbsp;Sign ] ] [ [ &nbsp;Number ] ], where ' ' denotes a space.
Here we assume that there are operators
• 0, 1, ..., 9,
• +__, -__,
• __ :: __, __ ::: __, and __ E __
in some specifications concerning numbers. We deal with this subject in the next subsection.

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

Natural numbers are represented in [RM99] as sequences of digits d1 :: d2:: ...:: dn. 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
That allows to write the elements of the sort Nat as d_1 :: d_2 :: ...:: d_n, where n >1, di e {0,1, ...9} for 1 < i < n. Note that this representation without brackets is valid only if the annotation left assoc is taken into account

#### 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
I.e. we have as integers9 d_1 :: d_2 :: ...:: d_n, +d_1 :: d_2 :: ...:: d_n, and -d_1 :: d_2 :: ...:: d_n.

#### 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
To this end we have as rational numbers the integers and fraction (x/p), (-x/p) +(x/p), +(-x/p) -(x/p), and -(-x/p), where x is of sort Int and p is of sort Pos.

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
where the function tenPower is specified such that tenPower(n)= min { 10^k | k e N \{0}, 10^k > n }. Thus we have d_1 :: d_2 :: ...:: d_n ::: d'_1 :: d'_2 :: ...:: d'_m for the number d_1 d_2 ...d_n . d'_1 d'_2 ...d'_m and r E i for the number r * 10 ^ i, where r is of sort Rat and i of sort Int.

#### 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
%%
...
end
Constants like pi and e are defined later as operators:
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

CoFI Note: L-11 -- Version: 0.1 -- 11 March 1999.   