Polynomial Normal Forms¶

Module: stdlib/polynomial.zph · Prerequisite: integer-arithmetic

Multivariate polynomial normal forms over ℤ, as pure forward-chaining rules. This is a data layer, like the arithmetic modules: it operates on normal forms and knows nothing about symbolic terms. The compiler that bridges the two is topoly.

Its reason for existing is one property: equality of polynomials is identity of nodes. Everything below serves that.

Representation¶

Recursive, dense, collapsed, variable-tagged.

A constant polynomial is a zint term: (pos zint N) / (neg zint N). This represents the layer’s intrinsic coefficient form: it keeps the sign tag even for nonnegative constants, and the layer calls z+ and zx directly, bypassing the façade that would otherwise lower a nonnegative result to the natural numeral N (Integers over ℤ). Every result of topoly is a value of this layer.
A non-constant polynomial with main variable V is (V poly L), where L is a cons list of canonical polynomials, least significant first: the V⁰ coefficient is the outermost cell.

The orientation is the numeral orientation, and deliberately so. A number in base b is a polynomial evaluated at b, and the rules below are the digit recursions of common-arithmetic with the carry removed.

zelph> .import math
zelph+> <x> ~ polyring
(:needsring <x>) ⇐ (<x> ~ polyring)
zelph+> ? :topoly $( 3*x^2 - 5 )
Answer: (:topoly $( &3 * x ^ &2 - &5 )) = (x poly <(neg zint &5) (pos zint &0) (pos zint &3)>)

The line <x> ~ polyring specifies x as an indeterminate and fixes the variable ORDER; absent this declaration, the query yields nothing whatsoever – refer to Variable order below.

⟨−5, 0, 3⟩ is −5 + 0·x + 3·x².

The invariants¶

Collapse. A polynomial that is constant in V is represented by its constant coefficient directly, never as (V poly (C cons nil)). Canonical coefficient lists therefore have length ≥ 2.

Nonzero leading coefficient. The last list element is never the zero polynomial. Inner zeros are value-relevant and kept.

Together: the zero polynomial at every nesting level is the single node (pos zint &0) — which is what turns the strip stage's zero test into a pattern match instead of a structural recursion. And it is what makes cancellation fall out:

zelph+> ? ((x poly <(pos zint &1) (pos zint &2)>) padd (x poly <(pos zint &3) (neg zint &2)>))
Answer: … = (pos zint &4)

(1 + 2x) + (3 − 2x): the x-coefficients cancel, the surviving list has one cell, and collapse turns it back into a bare constant.

The variable tag resolves an ambiguity an untagged collapsed representation would have across nesting levels: the list for y as a constant-in-x polynomial would be node-identical to the list for x. With the tag, every canonical polynomial is a unique hash-consed node.

Variable order¶

Composite coefficients inside (V poly L) have main variables strictly inner to V. The order is declared by the user as pouter facts — V pouter W reads "V is strictly outer" — and transitivity is provided by the module, so adjacent pairs suffice:

(A pouter B, B pouter C) => (A pouter C)

math.zph derives these from a <x y z> ~ polyring declaration, outermost first.

The ordering needs to constitute a strict total order across the variables involved. Asserting both V pouter W and W pouter V would break single-valuedness: the product of those two variables would end up with two distinct normal forms. Similar to a conflicting declared equation in symbolic-core, this case is reported as a contradiction that names both pouter facts, and it is reported only once:

(V pouter W, W pouter V, V != W) => !

A more extended cycle is closed into such pairings through transitivity. A variable declared as outer to itself (x pouter x) remains unreported. When two composites lack any declared ordering, they derive nothing – a manifestation of partiality by absence.

A different order is not wrong, only different; within one session the normal form is unique either way:

<x y> ~ polyring   →  (:topoly (y * x)) = (x poly <(pos zint &0) (y poly <…>)>)
<y x> ~ polyring   →  (:topoly (y * x)) = (y poly <(pos zint &0) (x poly <…>)>)

Operations¶

Request	Meaning
`(P padd Q) = R`	addition
`(:pneg P) = R`	negation
`(P psub Q) = R`	subtraction, via `pneg` + `padd`
`(P pmul Q) = R`	multiplication
`(P ppow N) = R`	exponentiation, `N` a natural numeral

zelph+> ? (:pneg (x poly <(pos zint &1) (pos zint &2)>))
Answer: … = (x poly <(neg zint &1) (neg zint &2)>)
zelph+> ? ((x poly <(pos zint &1) (pos zint &2)>) ppow &2)
Answer: … = (x poly <(pos zint &1) (pos zint &4) (pos zint &4)>)

(1 + 2x)² = 1 + 4x + 4x².

Addition is a flat case analysis on operand structures. A constant plus a constant delegates directly to z+ instead of to the ℤ façade, which would lower a nonnegative sum to a natural numeral. The same main variable means elementwise list addition – the digit recursion minus the carry – followed by a strip/collapse stage. Head adjustment (involving distinct main variables, or a constant into a composite) affects solely the V⁰ coefficient; the tail remains unaltered.

Multiplication needs no strip stage of its own: over ℤ, an integral domain, products of nonzero coefficients are nonzero, so elementwise scaling preserves canonicity, and the only accumulation — the schoolbook recursion — delegates to padd, which owns its canonicalisation.

Exponentiation arises when pmul is used in place of * inside a naive recursion. The exponent is not a polynomial; a zint, symbolic or composite exponent derives nothing, except a negative-signed zero such as (neg zint &0), which the façade compares as &0 and consequently interprets as the exponent zero; (pos zint &0) remains silent.

The zero test, positively¶

The strip rules must distinguish zero from nonzero coefficients. Zero is matched directly as the ground pattern (pos zint &0). Nonzero is derived as a positive marker from the three positive shapes: (neg zint N); (pos zint N) with N > &0 via an in-system cmp; and (W poly K) composites, which are never zero by the leading-coefficient invariant.

This keeps the module entirely inside the positive stratum — no negation, no != against structured nodes.

Canonicity¶

Every rule generates a canonical outcome when applied to canonical operands. Only addition involving the same main variable can yield a non-canonical raw list (cancellation, possibly of the leading coefficient); such outcomes proceed through the strip/collapse stage. Negation transforms each nonzero coefficient into another nonzero coefficient, one by one. An operand that is neither a zint nor a (V poly L) term derives nothing within padd, pneg, psub, or pmul. Outside of this, specifications apply solely to canonical operands: a non-canonical input – for instance, a signed zero like (neg zint &0), a magnitude that fails to be a numeral, or a coefficient list that is not canonical – might still receive a response, and that response need not be canonical.

Display note¶

The module excludes padd, psub, ladd and pmul from the self-fact display sugar: operand value coincidences like (P padd P) are ordinary facts about equal operands, not request markers, and must render verbosely. The genuine marker predicates (pneg, lneg, needsplcanon, plcanon, pzcheck, pnonzero) stay registered, because they are self-facts.

Testing¶

src/test/test_polynomial.cpp pins the representation, the invariants and every operation across all three arithmetic substrates.