Complex numbers are written as two-item lists [Real, Imaginary], and a small
toolkit of rules computes powers, polar form, and inverse trigonometric
functions. The answers include Euler’s identity and the surprising fact that
i^i is a real number.
Run it in the playground · Source
What do four classic complex powers evaluate to, √−1, e^(iπ), i^i and e^(−π/2), and what are asin(2) and acos(2), which have no real value?
Each result row names the operation, gives its inputs, and carries the computed complex value, so the output reads like a table of identities.
complex_polar([X, Y], [R, Tp]) :-
(Z1 is X ** 2),
(Z2 is Y ** 2),
(Z3 is Z1 + Z2),
(R is Z3 ** 0.5),
(Z4 is abs(X)),
(Z5 is Z4 / R),
(T is acos(Z5)),
complex_dial(X, Y, T, Tp).
A complex number becomes a radius R and an angle. acos only gives an angle
in the first quadrant, so complex_dial/4 has one clause per quadrant to turn
it into the full angle, using pi/1.
complex_power(i_to_i, [0, 1], [0, 1], Result) :-
complex_exponentiation([0, 1], [0, 1], Result).
complex_exponentiation/3 computes z^w through the polar form: the radius is
raised to the real part of w, and the angle and logarithm of the radius
combine into a new angle, which cos and sin turn back into real and
imaginary parts. Every intermediate value is a named variable, so each one
appears in the proof.
eyeprolog examples/complex.pl
complex_power(sqrt_minus_one, [-1, 0], [0.5, 0], [6.123233995736766e-17, 1.0]).
complex_power(e_to_i_pi, [2.718281828459045, 0], [0, 3.141592653589793], [-1.0, 1.2246467991473532e-16]).
complex_power(i_to_i, [0, 1], [0, 1], [0.20787957635076193, 0.0]).
complex_power(e_to_minus_pi_over_two, [2.718281828459045, 0], [-1.57079632679, 0], [0.20787957635177984, 0.0]).
complex_function(asin, two, [2, 0], [1.5707963267948966, 1.3169578969248166]).
complex_function(acos, two, [2, 0], [0.0, -1.3169578969248166]).
√−1 is i, e^(iπ) is −1 (Euler’s identity), and i^i ≈ 0.2079 is real and
equal to e^(−π/2), as the fourth row confirms. Tiny values such as
6.123233995736766e-17 are floating-point rounding where the exact answer is 0.
eyeprolog --proof examples/complex.pl
step(complex_power(i_to_i, [0, 1], [0, 1], [0.20787957635076193, 0.0]),
rule(13),
['Result' = [0.20787957635076193, 0.0]],
[complex_exponentiation([0, 1], [0, 1], [0.20787957635076193, 0.0])]).
The named row holds by clause 13, which hands the computation to
complex_exponentiation/3. That step, in turn, lists every is/2 evaluation
it used, down to the polar form of i.
condition('C1', resolution, ok, 20).
condition('C5', re_decision, ok, 78).
verdict(checked).
The proof has 98 steps: 20 rule steps that the checker replays against the program, and 78 arithmetic steps that it recomputes independently and finds equal. Nothing is taken on trust.
--goal 'complex_exponentiation([1,1],[2,0],R)'. The
exact answer is 2i; how close does floating point get?complex_polar([0,-1], P). Which clause of
complex_dial/4 places its angle, and why is it 3π/2 rather than −π/2?Learn more in The Art of EyeProlog, Chapter 6 and Chapter 29.