Manuel Computer Proofs for Polynomial Identities in Arbitrary many Variables

Motivation

• Easy: Prove identities in one free variable like

A(n) = B(n)

• Routine: Prove identities in a fixed number of variables like A(m, n, x, y) = B(m, n, x, y)

• But we need a human to prove things of the form

A(x_{1}, …, x_{n}) = B(x_{1}, …, x_{n})

with arbitrary n, x_{1}, …, x_{n}.

• Do we?

• We will present an algorithm for doing it by the computer, for certain kinds of A and B.

Manuel Computer Proofs for Polynomial Identities in Arbitrary many Variables

Battle Plan

• Motivation

• Fundamentals I: Notions from Difference Algebra – Difference Rings, Difference Fields, and so on

– Comparison to Differential Algebra

• Fundamentals II: A new Algorithm for Proving Univariate Identities – Admissible Sequences

– Example Sequences

– Algebraization

– The Algorithm

– Note on Correctness and Termination

• Application to Arbitrary Many Variables – Admissible Sequences

– Modification of the Algorithm

– Examples

– Schoissengeier’s Problem

Fundamentals I: Notions from Difference Algebra

• R = (R, s) is called difference ring if R is a ring and s: R → R is an automorphism on R.

• A difference ring which is also a field, is called difference field.

• Let K be a difference field, m ∈ ℕ. The set K{t_{1}, …, t_{m}} of polynomials in s^{i}t_{j} (i ≥ 0, j = 1, …, m) is called m-fold polynomial difference ring

• The quotient field of K{t_{1}, …, t_{m}} is written K⟨t_{1}, …, t_{m}⟩.

• The order of a difference polynomial p ∈ K{t_{1}, …, t_{m}} in the maximum j such that s^{j}t_{i} appears in p for some i.

• K{t_{1}, …, t_{m}}_{k} := { p ∈ K{t_{1}, …, t_{m}} : order(p) ≤ k } is called restriction of K{t_{1}, …, t_{m}}.

• K⟨t_{1}, …, t_{m}⟩_{k} is the quotient field of K{t_{1}, …, t_{m}}_{k}.

• If S ⊆ K{t_{1}, …, t_{m}} =: R then ⟨S⟩ is the polynomial ideal generated by S in R, ⟨⟨S⟩⟩ is the difference ideal generated by S in R, ⟨S⟩_{k} = ⟨S⟩ ∩ R_{k}, ⟨⟨S⟩⟩_{k} = ⟨⟨S⟩⟩ ∩ R_{k}.

Fundamentals II: Proving Univariate Identities

• Admissible Sequences

• Example Sequences

• Algebraization

• The Algorithm

• Notes on Correctness and Termination

Admissible Sequences

• Define the class C of sequences as follows:

• If – f_{1}, …, f_{s} ∈ C (s ≥ 0)

– f is a sequence, r > 0

– p is a polynomial in

f_{1}(n), f_{1}(n + 1), …, f_{1}(n + r),
f_{2}(n), f_{2}(n + 1), …, f_{2}(n + r),
⋮
f_{s}(n), f_{s}(n + 1), …, f_{s}(n + r),
f(n), f(n + 1), …, f(n + r − 1)

– f obeys a recurrence of the form

f(n + r) = p or f(n + r) = 1/p

Then f ∈ C

• Note: induction base given for s = 0

Example Sequences in C

• rational functions in n

• n ↦ α^{n} (α ∈ ℚ)

• n ↦ α^{β^{n}} (α ∈ ℚ, β ∈ ℕ)

• n ↦ Fib(n)

• n ↦ 2^{Fib(n)}

• n ↦ Fib(2^{n})

• n ↦ Γ(αn + β) (α ∈ ℚ)

• n ↦ ∑_{k=1}^{n} H(k)\binom{n}{k}

Some Closure Properties

• Let f(n), g(n), h(n) ∈ C, h(n) ≠ 0 for all n.

• f + g, f · g, f − g, αf, f/h ∈ C

• n ↦ ∑_{k=1}^{n} f(n) ∈ C

• n ↦ ∏_{k=1}^{n} f(n) ∈ C

• n ↦ K_{k=1}^{n} h(n) = h(1) + \frac{1}{h(2) + \frac{1}{⋯ + \frac{1}{h(n)}}} ∈ C

RISC 2004 Computer Algebra Seminar

Manuel Computer Proofs for Polynomial Identities in Arbitrary many Variables

Algebraic Representation of Elements of C

• Consider difference ideals “generated” by the recurrences

• Let f_{1}, …, f_{m} ∈ C be such that the definition of f_{i} depends only on f_{j} with j < i, let f = f_{m}.

• Example: f(n) := ∑_{k=1}^{n} \frac{k! H(k)}{Fib(k)}

Component  Recurrence  Defining relation
f_{1}(n) = n  f_{1}(n + 1) = f_{1}(n) + 1  st_{1} − t_{1} − 1
f_{2}(n) = Fib(n)  f_{2}(n + 2) = f_{2}(n + 1) + f_{2}(n)  sst_{2} − st_{2} − t_{2}
f_{3}(n) = n!  f_{3}(n + 1) = (n + 1)f_{3}(n)  st_{3} − t_{3}st_{1}
f_{4}(n) = 1/n  f_{4}(n) = 1/n  t_{4}t_{1} − 1
f_{5}(n) = H(n) = ∑_{k=1}^{n} \frac{1}{k} f_{5}(n + 1) = f_{5}(n) + \frac{1}{n + 1}  st_{5} − t_{5} − st4
f_{6}(n) = \frac{1}{Fib(n)} f_{6}(n) = \frac{1}{Fib(n)} t_{6}t_{2} − 1
f_{7}(n) = f(n)  f_{7}(n + 1) = f_{7}(n) + \frac{(n + 1)! H(n + 1)}{Fib(n + 1)} st_{7} − t_{7} − st_{3}st_{5}st_{6}

RISC 2004 Computer Algebra Seminar

The Proving Algorithm

• Input: f ∈ C a polynomially recursive function

D defining relations of f and its “subexpressions”

Assumption: t_{m} corresponds to {f(n)}_{n};

The highest order in D is of order r.

Output:  “correct” or “incorrect” depending on whether f ≡ 0 or not

1 \underline{function} isZero(f, R) 2 k := r − 1

3  \underline{repeat}

4 k := k + 1 5 I_{k} := ⟨⟨D⟩⟩_{k} + ⟨t_{m}, st_{m}, …, s^{k−1}t_{m}⟩_{k} 6 \underline{until} s^{k}t_{m} ∈ RadI_{k} 7 // check initial conditions 8 \underline{if} f(1) = f(2) = ⋯ = f(k) = 0 \underline{then}

9  \underline{return} “correct”
10  \underline{else}
11  \underline{return} “incorrect”

Manuel Computer Proofs for Polynomial Identities in Arbitrary many Variables

Correctness and Termination

• Theorem The algorithm is correct and terminats.

Application to Arbitrary Many Variables

• Admissible Sequences

• Modification of the Algorithm

• Examples

• Schoissengeier’s Problem

Admissible Sequences

• Define the class C′ of formal sequences as follows:

•

Formal sequences u_{1}, u_{2}, u_{3}, … of indeterminates belong to C′.

• If, as before, – f_{1}, …, f_{s} ∈ C (s ≥ 0)

– f is a sequence, r > 0

– p is a polynomial in

f_{1}(n), f_{1}(n + 1), …, f_{1}(n + r),
f_{2}(n), f_{2}(n + 1), …, f_{2}(n + r),
⋮
f_{s}(n), f_{s}(n + 1), …, f_{s}(n + r),
f(n), f(n + 1), …, f(n + r − 1)

– f obeys a recurrence of the form

f(n + r) = p or f(n + r) = 1/p

Then f ∈ C

Modification of the Algorithm

• Represent sequences of indeterminates also by some t_{i}.

• Key idea I: Omit the defining relation for them.

• Given f_{1}, …, f_{m} ∈ C′ where – f_{1}, …, f_{i} are sequences of indeterminates and

– f_{i+1}, …, f_{m} are given by recurrences, each f_{j} depending only on f_{j′} with j′ < j

• The original algorithm is applicable, but does not (always) terminate.

• Key idea II: Put indeterminates into the ground field, compute in K⟨t_{1}, …, t_{i}⟩{t_{i+1}, …, t_{m}} • The original algorithm is applicable and the termination proof goes through.

Manuel Computer Proofs for Polynomial Identities in Arbitrary many Variables

Examples

• Any family of orthogonal polynomials, defined by

P_{n}(x) = (x − c_{n})P_{n−1}(x) − λ_{n}P_{n−2}(x),  P_{−1}(x) = 0, P_{0}(x) = 1

for arbitrary c_{1}, c_{2}, … and λ_{1}, λ_{2}, … satisfies the Christoffel-Darboux-formula

∑_{k=0}^{n} \frac{P_{k}(x)P_{k}(u)}{∏_{i=1}^{k+1} λ_{i}} = \frac{P_{n+1}(x)P_{n}(u) − P_{n}(x)P_{n+1}(u)}{(x − u) ∏_{i=1}^{n+1} λ_{i}}

• Proof: less than a second

• Continued fraction identity: Write

C_{n} := x_{0} + \frac{y_{1}}{x_{1} + \frac{y_{2}}{... + \frac{y_{n}}{x_{n}}}} = \frac{K(y_{1}, …, y_{n}; x_{0}, …, x_{n})}{K(y_{2}, …, y_{n}; x_{1}, …, x_{n})}

for arbitrary x_{1}, …, x_{n}, y_{1}, …, y_{n} and n, and prove, in less than a second,

C_{n} = \frac{K(y_{1}, …, y_{n}; x_{0}, …, x_{n})}{K(y_{2}, …, y_{n}; x_{1}, …, x_{n})} = x_{0} + ∑_{k=1}^{n}(−1)^{k+1} \frac{∏_{i=1}^{k} y_{i}}{K(y_{2}, …, y_{k−1}; x_{1}, …, x_{k−1})K(y_{2}, …, y_{k}; x_{1}, …, x_{k})}

RISC 2004 Computer Algebra Seminar

Manuel Computer Proofs for Polynomial Identities in Arbitrary many Variables

Examples II

• Also easy (less than one second):

∑_{k=1}^{n} \frac{∏_{i=1}^{k−1}(x_{i} + α)}{∏_{i=1}^{k} x_{k}} = \frac{1}{α}( ∏_{k=1}^{n} \frac{x_{k} + α}{x_{k}} − 1)
∑_{k=1}^{n} H(k) ∑_{i=1}^{k} x_{i} = (−n + (1 + n) H(n)) ∑_{i=1}^{n} x_{i} − ∑_{k=1}^{n}(H(k) − 1)kx_{k}
∑_{r=1}^{n} \frac{∑_{l=1}^{r} ∏_{k=1}^{l} \frac{x_{k}}{1+x_{k}}}{1 + x_{r}} = ∑_{k=1}^{n} \frac{∏_{i=1}^{k} \frac{x_{i}}{1+x_{i}}}{1 + x_{k}} + ∑_{i=1}^{n} \frac{1}{1 + x_{i}} ∑_{i=1}^{n} ∏_{k=1}^{i} \frac{x_{k}}{1 + x_{k}} − ∑_{k=1}^{n} ( ∏_{i=1}^{k} \frac{x_{i}}{1 + x_{i}})( ∑_{i=1}^{k} \frac{1}{1 + x_{i}})

RISC 2004 Computer Algebra Seminar

Schoissengeier’s Problem

• Appears in number theoretic context

• An identitity with 27 summation signs, two sequences of indeterminates.

• Not of the appropriate form.

• but can be converted to an appropriate form.

• At the cost of expression blow up: The result contains 2000 summation signs.

• Elementary simplification gives 100 summation signs.

• Compute a Gröbner basis of 250 polynomials in 350 variables. Game over.