7 A Specification of Complex Numbers

The complex numbers are introduced as pairs  complex (t,u), where t,u are of sort Real. Thus again we call our specification BasicComplex. The mathematical background discussed in section 5 carries over to the specification BasicComplex.

The representations for rational numbers resp. finite decimal fractions as described in [RM99a][RM99b] carry over for complex numbers. Thus 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. Note that the operation complex is internal to the following specification as it is hided at its end. I.e. outside this specification a complex number c has to be written as c= a + b * i or in polar coordinates as c=r(c) * e^{i *phi(c)} .

spec

 BasicComplex =

BasicReal

then

free

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

sort

Real < Complex

ops

i :	Complex;
__i:	Real -> Complex;
r, phi :	Complex -> Real;
+__,-__ :	Complex -> Complex;
__+__,__-__,__*__ :	Complex × Complex -> Complex;
__/__,__^ __ :	Complex × Complex ->? Complex;
exp,sqrt :	Complex -> Complex;
ln :	Complex ->? Complex;
sin, cos, sinh, cosh :	Complex -> Complex;
tan, cot, tanh, coth :	Complex ->? Complex;

vars

t,u,v,w:Real; x,y: Complex

%%

Embedding of the reals:

.

t = complex(t,0)

%%

i:

.

i = complex(0,1)

.

t i = complex(0,t)

%%

Polar coordinates of a complex number:

.

r(complex(t,u)) = sqrt(t²+u²)

.

phi(complex(t,u)) = arctan(u/t) if ¬ t=0

.

phi(complex(t,u)) = sign(u)*pi/2 if t=0

%%

arithmetic functions:

.

+x = x

.

-complex(t,u) = complex(-t,-u)

.

complex(t,u)+complex(v,w) = complex(t+v,u+w)

.

complex(t,u)-complex(v,w) = complex(t-v,u-w)

.

complex(t,u)*complex(v,w) = complex(t*v-u*w,t*w+v*u)

.

def x/y <=> ¬ y=0

.

complex(t,u)/complex(v,w) =

complex( (t*v+u*w)/(v^ 2+w^ 2), (v*u-t*w)/(v^ 2+w^ 2))

%%

exponential function and logarithm (using Euler's formula):

.

exp(complex(t,u)) = exp(t) * complex(cos(u),sin(u))

.

def ln(x) <=> ¬ x=0

.

ln(x) = complex(ln(r(x)),phi(x)) if def ln(x)

%%

power and square root defined using exp and ln:

.

def x ^ y <=> ¬ x=0

.

x ^ y = exp(ln(x)*y)

.

sqrt(x) = x^ (1/2) if ¬ x=0

.

sqrt(0) = 0

%%

trigonometric functions:

.

sin(complex(t,u)) = complex(sin(t)*cosh(u),cos(t)*sinh(u))

.

cos(complex(t,u)) = complex(cos(t)*cosh(u),-sin(t)*sinh(u))

.

tan(complex(t,u)) =

complex( sin(2*t), sinh(2*u))/(cos(2*t)+cosh(2*u))

.

cot(complex(t,u)) =

complex( -sin(2*t), sinh(2*u))/(cos(2*t)-cosh(2*u))

%%

hyperbolic functions:

.

sinh(complex(t,u)) = complex(sinh(t)*cos(u),cosh(t)*sin(u))

.

cosh(complex(t,u)) = complex(cosh(t)*cos(u),sinh(t)*sin(u))

.

tanh(complex(t,u)) =

complex( sinh(2*t), sin(2*u))/(cosh(2*t)+cos(2*u))

.

coth(complex(t,u)) =

complex( sinh(2*t), -sin(2*u))/(cosh(2*t)-cos(2*u))

hide

op complex

end

---

CoFI Note: M-7 -- Version: 0.2 -- 13 April 1999.
Comments to till@informatik.uni-bremen.de