= 27d567bc2d48d9f40e9ccc20ea370b15)
gRR comments on Difference between CDT and ADT/UDT as constant programs - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (10)
Yes, all computations that it has no resources to directly simulate. Which necessarily include any copies of itself, no matter how much resources it has.
What do you think of the other idea - that all ways of recognizing correlations can be reduced to series of evaluations and source code comparisons? I don't immediately see any other way to prove that two source codes return the same thing... must check a textbook on lambda calculus.
No, that idea looks wrong, unless I misunderstand it. Imagine you have two functions f() and g() that you're too weak to evaluate. You need to be able to prove that f()+g()==g()+f(), but I don't see any way to do that using only evaluations and source code comparisons. The general way is to use a theorem prover that has axioms like the commutativity of addition.
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()...