   Go backward to 6 Towards a Datatype REAL
Go up to Top
Go forward to References

# 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) * ei *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(t2+u2)
.
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.   