Two degree-4 polynomials, one with real roots and one with complex roots, are evaluated at every point of a small grid of complex integers. EyeProlog keeps the points where the polynomial vanishes, then multiplies the roots back together to confirm they rebuild the original coefficients.
Run it in the playground · Source
A quartic is a polynomial of degree 4, so it has four roots counted with
multiplicity. Finding them in general takes numerical methods, but if we
suspect they are small Gaussian integers (complex numbers a + bi with
integer parts), we can simply search: evaluate the polynomial at each
candidate and keep the zeros. A second, independent computation then checks
the result by expanding (x − r₁)(x − r₂)(x − r₃)(x − r₄).
polynomial(real_quartic, [[1, 0], [-10, 0], [35, 0], [-50, 0], [24, 0]]).
polynomial(complex_quartic, [[1, 0], [-9, -5], [14, 33], [24, -44], [-26, 0]]).
real_domain(complex_quartic, 0, 5).
imag_domain(complex_quartic, 0, 2).
A complex number is a pair [Real, Imaginary], and a polynomial is its list
of coefficients from the highest power down. The real quartic is
x⁴ − 10x³ + 35x² − 50x + 24. The domain facts bound the search grid.
poly_eval([Coeff|Rest], X, Value) :-
poly_eval_acc(Rest, X, Coeff, Value).
poly_eval_acc([], _x, Acc, Acc).
poly_eval_acc([Coeff|Rest], X, Acc, Value) :-
c_mul(Acc, X, Product),
c_add(Product, Coeff, Next),
poly_eval_acc(Rest, X, Next, Value).
root(Case, Root) :-
polynomial(Case, Coeffs),
candidate(Case, Root),
poly_eval(Coeffs, Root, Value),
c_zero(Value).
poly_eval/3 is Horner’s rule: multiply the running value by x and add
the next coefficient. root/2 is generate-and-test: every grid point is a
candidate, and only exact zeros survive.
eyeprolog examples/polynomial.pl
root(real_quartic, [1, 0]).
root(real_quartic, [2, 0]).
root(real_quartic, [3, 0]).
root(real_quartic, [4, 0]).
root(complex_quartic, [0, 1]).
root(complex_quartic, [1, 1]).
root(complex_quartic, [3, 2]).
root(complex_quartic, [5, 1]).
reconstructedPolynomial(real_quartic, [[1, 0], [-10, 0], [35, 0], [-50, 0], [24, 0]]).
reconstructedPolynomial(complex_quartic, [[1, 0], [-9, -5], [14, 33], [24, -44], [-26, 0]]).
reconstructionMatches(real_quartic, true).
reconstructionMatches(complex_quartic, true).
allRootsVerified(real_quartic, true).
allRootsVerified(complex_quartic, true).
The real quartic has roots 1, 2, 3, 4; the complex one has i, 1 + i,
3 + 2i, and 5 + i. Expanding the four linear factors gives back exactly
the stated coefficients, so the search found all four roots of each.
eyeprolog --proof examples/polynomial.pl
step(root(complex_quartic, [3, 2]),
rule(20),
['Case' = complex_quartic,
'Root' = [3, 2],
'Coeffs' = [[1, 0], [-9, -5], [14, 33], [24, -44], [-26, 0]],
'Value' = [0, 0]],
[polynomial(complex_quartic, [[1, 0], [-9, -5], [14, 33], [24, -44], [-26, 0]]),
candidate(complex_quartic, [3, 2]),
poly_eval([[1, 0], [-9, -5], [14, 33], [24, -44], [-26, 0]], [3, 2], [0, 0]),
c_zero([0, 0])]).
3 + 2i is a root because it lies in the grid and Horner evaluation at that
point gives exactly [0, 0]. The poly_eval use has its own steps, one per
Horner iteration, down to the individual multiplications.
condition('C1', resolution, ok, 273).
condition('C5', re_decision, ok, 241).
condition('C7', relevance, ok, 528).
steps(514).
verified(273).
recomputed(241).
trusted(0).
verdict(checked).
The proof has 514 steps. The checker replays the 273 clause steps and
recomputes the 241 arithmetic steps (is/2, comparisons, between/3)
independently, so every complex multiplication in the argument is redone.
Nothing is taken on trust.
imag_domain(complex_quartic, 0, 2) to -2, 2. Do any new roots
appear, and why can’t there be more than four?x² + 1 as [[1, 0], [0, 0], [1, 0]],
with a grid that includes i and −i.complex_quartic by 1. How many roots survive,
and what does reconstructionMatches/2 report?Learn more in The Art of EyeProlog, Chapters 26 (witnesses) and 28 (representation).