Go backward to C.6 Real Numbers Go up to C Logic Evaluator Definitions Go forward to C.8 More on Functions

C.7 Complex Numbers

// ----------------------------------------------------------------
// $Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp $
// the complex numbers
//
// (c) 1999, Wolfgang Schreiner, see file COPYRIGHT
// http://www.risc.uni-linz.ac.at/software/formal
// ----------------------------------------------------------------
read real;

// complex numbers are pairs of reals
pred C(x) <=> 
  and(Tuple(x), =(2, length(x)), R(.0(x)), R(.1(x)));

// complex constructors and
fun +i(x: R, y: R) = tuple(x, y);
fun real(r: R) = .0(r);
fun imaginary(r: R) = .1(r);

// constants
fun C0 = +i(R0, R0);
fun C1 = +i(R1, R0);
fun C2 = +i(R2, R0);
fun i  = +i(R0, R1);

// arithmetic
fun +C(x: C, y: C) = +i(+R(.0(x), .0(y)), +R(.1(x), .1(y)));
fun -C(x: C, y: C) = +i(-R(.0(x), .0(y)), -R(.1(x), .1(y)));
fun -(x: C) = -C(C0, x);
fun *C(x: C, y: C) = 
  +i(-R(*R(.0(x), .0(y)), *R(.1(x), .1(y))),
     +R(*R(.0(x), .1(y)), *R(.1(x), .0(y))));
fun /C(x: C, y: C) =
  let(d = +R(*R(.0(y), .0(y)), *R(.1(y), .1(y))):
    +i(/R(+R(*R(.0(x), .0(y)), *R(.1(x), .1(y))), d),
       /R(-R(*R(.1(x), .0(y)), *R(.0(x), .1(y))), d)));
fun ^-1C(x: C) = /C(C1, x);

// complex conjugate
fun conj(x: C) = +i(.0(x), -R(.1(x)));

// square of absolute value
fun ||^2(x: C) = +R(*R(.0(x), .0(x)), *R(.1(x), .1(x)));

// ----------------------------------------------------------------
// $Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp $
// ----------------------------------------------------------------