To prove that two given functions are the same involves proving infinitely many statements. I wonder how to implement so that a computer can check such a statement?

An easy example is the following: how to check

$$ \frac{1}{1-x}\frac{1}{1+x} = \frac{1}{1-x^2} $$

where three of them are expressed in terms of infinite sums?

More precisely, define three functions $f, g, h: \mathbb{N_{\geq 0}} \to \mathbb{C}$ with

$$ f(n) = 1 \mbox{, } g(n) = (-1)^n \mbox{, } h(2n) = 1 \mbox{, } h(2n+1) = 0.$$ Then

$$\frac{1}{1-x} = \Sigma_n f(n) x^n$$ $$\frac{1}{1+x} = \Sigma_n g(n) x^n$$ $$\frac{1}{1-x^2} = \Sigma_n h(n) x^n$$

Precise Question

How does a computer check if $h(n) = \Sigma_{k=0}^n f(k)g(n-k)$ for all $n$? Lets suppose we are not allowed to use theorems to transform the infinite sums back to their fractions form.


I am a mathematician (sort of) who knows little about logic, functional programming, and proof assistants. I know how to argue the proof with mathematician standard, but I am very curious about how a computer checks proofs that involve infinity.

  • 3
    $\begingroup$ If the functions are (multivariate) polynomials, the standard approach is probabilistic identity verification, based on the Schwartz–Zippel lemma: en.wikipedia.org/wiki/Polynomial_identity_testing $\endgroup$ – Gamow Nov 11 '19 at 17:46
  • 4
    $\begingroup$ To begin with, it depends on how your infinite functions are given to the computer in the first place. But for example, your identity seems to be simple enough to fall in the scope of the algorithms described in A=B. $\endgroup$ – Emil Jeřábek Nov 11 '19 at 17:53
  • 1
    $\begingroup$ "Lets suppose we are not allowed to use theorems to transform the infinite sums back to their fractions form." What does this mean? Formalizing that statement is quite tricky. As an extreme example, it's not (conceptually) hard to write a program that diagonalizes over all strings to find a ZF proofs of your statement (or if its negation), and outputs the first correct one. If a proof exists, this will find it. Can you put a finger on why this isn't what you're looking for? $\endgroup$ – Yonatan N Nov 11 '19 at 23:13
  • 3
    $\begingroup$ @Student: the general statement is due to Rice's Theorem. In short, if you could decide if two arbitrary functions are equal you would be able to decide the halting problem. Nevertheless, there are large classes of functions where equivalence is decidable. $\endgroup$ – lambda.xy.x Nov 12 '19 at 10:05
  • 4
    $\begingroup$ This is not a research-level question. It belongs on cs.stackexchange.com. $\endgroup$ – Andrej Bauer Nov 13 '19 at 12:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.