Don’t you need a theorem prover to go from commutativity of addition to f()+g()==g()+f()? I thought you were supposed to use only evaluations and source code comparisons on the code f()+g()==g()+f() directly...
Commutativity of addition is a correlation P1=P2, where P1(x,y)=x+y, and P2(x,y)=y+x. So, f()+g() = [using this correlation] = g()+f().
But you’re right. In order to use this, I have to be able to calculate evaluations and comparisons on arbitrary pieces of code, not just the ones existing in U()...
I think I can prove commutativity of addition using just evaluations and source code comparisons:
def P(m,n): P(m, 0) = m ; P(m, n+1) = P(m, n) + 1
Lemma: P(m+1, n) = P(m, n+1)
Proof:
Let A(m,n) = P(m+1, n),
Let B(m,n) = P(m, n+1)
Then:
A(m, 0) = P(m+1, 0) = m+1
A(m, n+1) = P(m+1, n+1) = P(m+1, n) + 1 = A(m, n) + 1
B(m, 0) = P(m, 0+1) = P(m) + 1 = m+1
B(m, n+1) = P(m, n+1+1) = P(m, n+1) + 1 = B(m, n) + 1
The source code for A and B are equivalent ⇒ A=B. QED
Theorem: P(m, n) = P(n, m)
Proof:
P(0, 0) = 0
P(m+1, 0) = P(m, 0) + 1
P(0, n+1) = P(0, n) + 1
P(m+1, n+1) = P(m+1, n) + 1 = P(m, n+1) + 1 = P(m, n) + 1 + 1
The code of P is symmetrical now, so P(m,n)=P(n,m). QED
Don’t you need a theorem prover to go from commutativity of addition to f()+g()==g()+f()? I thought you were supposed to use only evaluations and source code comparisons on the code f()+g()==g()+f() directly...
Commutativity of addition is a correlation P1=P2, where P1(x,y)=x+y, and P2(x,y)=y+x.
So, f()+g() = [using this correlation] = g()+f().
But you’re right. In order to use this, I have to be able to calculate evaluations and comparisons on arbitrary pieces of code, not just the ones existing in U()...