<p>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?</p>

<p>An easy example is the following: how to check </p>

<p><span class="math-container">$$ \frac{1}{1-x}\frac{1}{1+x} = \frac{1}{1-x^2} $$</span></p>

<p>where three of them are expressed in terms of infinite sums?</p>

<hr>

<p>More precisely, define three functions <span class="math-container">$f, g, h: \mathbb{N_{\geq 0}} \to \mathbb{C}$</span> with </p>

<p><span class="math-container">$$ f(n) = 1 \mbox{, }   g(n) = (-1)^n  \mbox{, }  h(2n) = 1 \mbox{, } h(2n+1) = 0.$$</span> Then</p>

<p><span class="math-container">$$\frac{1}{1-x} = \Sigma_n f(n) x^n$$</span>
<span class="math-container">$$\frac{1}{1+x} = \Sigma_n g(n) x^n$$</span>
<span class="math-container">$$\frac{1}{1-x^2} = \Sigma_n h(n) x^n$$</span></p>

<h3>Precise Question</h3>

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

<h3>Disclaimer</h3>

<p>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.</p>

CC BY-SA 4.0
2019-11-11T17:46:39.840Z
If the functions are (multivariate) polynomials, the standard approach is probabilistic identity verification, based on the Schwartz–Zippel lemma:  https://en.wikipedia.org/wiki/Polynomial_identity_testing
Gamow
CC BY-SA 4.0
2019-11-11T17:53:06.253Z
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](https://www.math.upenn.edu/~wilf/AeqB.html).
Emil Jeřábek
CC BY-SA 4.0
2019-11-11T18:59:41.517Z
These are surprising. Do you guys mean there's no way to prove it unless we used some auxiliary theorem created by humans?! I have started to read `A=B` and it claims in the first chapter that no universal proof machine exists, even if all things we want is to check identities!!
Student
CC BY-SA 4.0
2019-11-11T19:09:14.187Z
If I want to check if $f(x)=x-x$ is the same as $g(x)=0$ as a function on $\mathbb{R}$, I need to invoke theorems like: `the set of real polynomials in one variable has canonical form`. Thus, checking such identities falls into a category that is higher than checking $1+1=2$, which can be done in finite time.
Student
CC BY-SA 4.0
2019-11-11T19:10:10.603Z
Is what concerns me above the difference between 1st-order logic and 0th-order logic?
Student
CC BY-SA 4.0
2019-11-11T23:13:47.150Z
"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?
Yonatan N
CC BY-SA 4.0
2019-11-12T10:05:16.077Z
@Student: the general statement is due to [Rice's Theorem](https://en.wikipedia.org/wiki/Rice%27s_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.
lambda.xy.x
CC BY-SA 4.0
2019-11-12T11:02:06.257Z
If the functions in question are semialgebraic, equality can (in principle) be decided using the first order theory of the reals.
mrp
CC BY-SA 4.0
2019-11-12T13:13:58.870Z
@mrp would you mind pointing out some reference for that?
Student
CC BY-SA 4.0
2019-11-12T13:19:55.887Z
@YonatanN Yeah, I too feel my statement is sloppy. I am no longer sure what a proof is. What concerns me is that the proofs I am used to in math-la-la-land seem to form a hierarchy system. For example, to prove $1+1=2$ is much easier than proving $x+x=2x$ (here x is viewed as a function, the identity function), because $1+1=2$ is a (to me) finite statement, whereas $x+x=2x$ is an infinite statement -- it boils down to say `for all real numbers r, r+r=2r`. How exactly does modern convention deal with the hierarchy above? Am I actually talking about 0th-order logic, 1st-order logic , 2nd-.. etc?
Student
CC BY-SA 4.0
2019-11-13T12:12:31.983Z
This is not a research-level question. It belongs on cs.stackexchange.com.
Andrej Bauer
CC BY-SA 4.0
2019-11-13T16:25:16.627Z
I'm sorry as I wasn't aware this is a place for research-level questions. Should I delete this post and post another one there?
Student
CC BY-SA 4.0
2019-11-14T15:14:29.467Z
Yes, please do so.
Andrej Bauer
<lo.logic><functional-programming><proof-assistants>
How do computers check if two functions are the same?
Student
# How do computers check if two functions are the same?

(Asked by: username_0 on 2019-11-11)

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.

### Disclaimer

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.

**Tags:** lo.logic, functional-programming, proof-assistants

> **Comments:**
> **username_1**: If the functions are (multivariate) polynomials, the standard approach is probabilistic identity verification, based on the Schwartz–Zippel lemma:  https://en.wikipedia.org/wiki/Polynomial_identity_testing  
> **username_2**: 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](https://www.math.upenn.edu/~wilf/AeqB.html).  
> **username_0**: These are surprising. Do you guys mean there's no way to prove it unless we used some auxiliary theorem created by humans?! I have started to read `A=B` and it claims in the first chapter that no universal proof machine exists, even if all things we want is to check identities!!  
> **username_0**: If I want to check if $f(x)=x-x$ is the same as $g(x)=0$ as a function on $\mathbb{R}$, I need to invoke theorems like: `the set of real polynomials in one variable has canonical form`. Thus, checking such identities falls into a category that is higher than checking $1+1=2$, which can be done in finite time.  
> **username_0**: Is what concerns me above the difference between 1st-order logic and 0th-order logic?  
> **username_3**: "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?  
> **username_4**: @username_0: the general statement is due to [Rice's Theorem](https://en.wikipedia.org/wiki/Rice%27s_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.  
> **username_5**: If the functions in question are semialgebraic, equality can (in principle) be decided using the first order theory of the reals.  
> **username_0**: @username_5 would you mind pointing out some reference for that?  
> **username_0**: @YonatanN Yeah, I too feel my statement is sloppy. I am no longer sure what a proof is. What concerns me is that the proofs I am used to in math-la-la-land seem to form a hierarchy system. For example, to prove $1+1=2$ is much easier than proving $x+x=2x$ (here x is viewed as a function, the identity function), because $1+1=2$ is a (to me) finite statement, whereas $x+x=2x$ is an infinite statement -- it boils down to say `for all real numbers r, r+r=2r`. How exactly does modern convention deal with the hierarchy above? Am I actually talking about 0th-order logic, 1st-order logic , 2nd-.. etc?  
> **username_6**: This is not a research-level question. It belongs on cs.stackexchange.com.  
> **username_0**: I'm sorry as I wasn't aware this is a place for research-level questions. Should I delete this post and post another one there?  
> **username_6**: Yes, please do so.  

---

## 0 answers

