Go backward to C.6 Real Numbers Go up to C Logic Evaluator Definitions Go forward to C.8 More on Functions |
// ---------------------------------------------------------------- // $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 $ // ----------------------------------------------------------------