Very often in this conversation, I think we’re using words to mean wildly different things; such as “proof.” Do you need to simulate bubble sort to prove that it takes quadratic time?
Very often in this conversation, I think we’re using words to mean wildly different things; such as “proof.”
Very possibly! “Simulate” is another word that we may not be using the same way.
Do you need to simulate bubble sort to prove that it takes quadratic time?
I would say ‘yes, if’, conditioned on what you mean by simulate. It doesn’t look like you can prove bubble sort takes quadratic time by running it a bunch of times, though you could certainly suggest that it does. But I also don’t see how to prove bubble sort takes quadratic time without intense understanding of the algorithm (and it may be that intense understanding requires simulation).
If you’re given the algorithm to begin with, this doesn’t seem like a big issue. But if I give you some code, which is an implementation of bubble sort but not labeled as such, then proving it takes quadratic time is more involved, and may (will?) require running the code. Right?
It is certainly true that some algorithms are easier to prove things about than others. Let’s set aside running time and just talk about correctness of sorting. There are algorithms that sort but are undecidable; or for which the proof is very long. But the proof that bubbling correctly sorts is short, even intercal bubbling. Finding a short proof quickly may be hard, but exhaustively searching for it is simple to implement and simple to prove things about. And once you’ve found it, you just verify it. You don’t have to simulate the code to verify the proof. You certainly don’t have an infinite regress.
If you like, you can say that by invoking exhaustive searching, we are assuming P=NP and assuming away the problem of AI. That is intentional. The question of decision theory is an independent problem and it is right to separate them this way. But exhaustive search is a concrete computable function, not “magic.” Also, sometimes you really are constrained by space, not time and so exhaustive search is a realistic option.
Putting in a proof generator makes it easy to make an algorithm undecidable. If we make these deterministic algorithms play Rock-Paper-Scissors, they will fail to terminate or otherwise break down. Many similar algorithms with resource constraints will be undecidable to other algorithms with the same resource constraints. But proofs are not particularly hard to reason about and do not force undecidability / infinite regress. In particular, when the game is PD and the algorithms are trying to cooperate to be understood and reach (C,C) rather than (D,D). Then (sometimes) there are short proofs of the relevant things and they do manage to cooperate.
And once you’ve found it, you just verify it. You don’t have to simulate the code to verify the proof. You certainly don’t have an infinite regress.
I still don’t see why this is the case, but I think I understand everything else about it, which suggests I should let this sit for a while and it’ll become clear when it’s relevant. (The proof verification is where it looked like magic was happening, not finding the interesting proofs.)
If you like, you can say that by invoking exhaustive searching, we are assuming P=NP and assuming away the problem of AI. That is intentional. The question of decision theory is an independent problem and it is right to separate them this way.
I think I disagree that it’s right to separate them this way, but this may just be a matter of taste / goals. I am far more interested in prescriptive decision theory than normative decision theory (bounded rationality vs. unbounded rationality).
I considered saying that proofs are verifiable by definition. I mean a proof in formal logic. The point of formal logic is that it is computable (even fast) to verify it. The point, which matches the common usage, is that it is convincing. You can’t prove anything about arbitrary code; these algorithms are not guaranteed to understand the opponent. But it’s interesting that sometimes they do succeed in proving things about their opponents.
If you’re given the algorithm to begin with, this doesn’t seem like a big issue. But if I give you some code, which is an implementation of bubble sort but not labeled as such, then proving it takes quadratic time is more involved, and may (will?) require running the code. Right?
I’d say it’s easier to prove that a naïve bubble sort runs in quadratic time, than it is to prove that when it terminates, the list is actually sorted. It’s obvious by inspection that it contains a nested loop over the same data structure.
Very often in this conversation, I think we’re using words to mean wildly different things; such as “proof.” Do you need to simulate bubble sort to prove that it takes quadratic time?
Very possibly! “Simulate” is another word that we may not be using the same way.
I would say ‘yes, if’, conditioned on what you mean by simulate. It doesn’t look like you can prove bubble sort takes quadratic time by running it a bunch of times, though you could certainly suggest that it does. But I also don’t see how to prove bubble sort takes quadratic time without intense understanding of the algorithm (and it may be that intense understanding requires simulation).
If you’re given the algorithm to begin with, this doesn’t seem like a big issue. But if I give you some code, which is an implementation of bubble sort but not labeled as such, then proving it takes quadratic time is more involved, and may (will?) require running the code. Right?
It is certainly true that some algorithms are easier to prove things about than others. Let’s set aside running time and just talk about correctness of sorting. There are algorithms that sort but are undecidable; or for which the proof is very long. But the proof that bubbling correctly sorts is short, even intercal bubbling. Finding a short proof quickly may be hard, but exhaustively searching for it is simple to implement and simple to prove things about. And once you’ve found it, you just verify it. You don’t have to simulate the code to verify the proof. You certainly don’t have an infinite regress.
If you like, you can say that by invoking exhaustive searching, we are assuming P=NP and assuming away the problem of AI. That is intentional. The question of decision theory is an independent problem and it is right to separate them this way. But exhaustive search is a concrete computable function, not “magic.” Also, sometimes you really are constrained by space, not time and so exhaustive search is a realistic option.
Putting in a proof generator makes it easy to make an algorithm undecidable. If we make these deterministic algorithms play Rock-Paper-Scissors, they will fail to terminate or otherwise break down. Many similar algorithms with resource constraints will be undecidable to other algorithms with the same resource constraints. But proofs are not particularly hard to reason about and do not force undecidability / infinite regress. In particular, when the game is PD and the algorithms are trying to cooperate to be understood and reach (C,C) rather than (D,D). Then (sometimes) there are short proofs of the relevant things and they do manage to cooperate.
I still don’t see why this is the case, but I think I understand everything else about it, which suggests I should let this sit for a while and it’ll become clear when it’s relevant. (The proof verification is where it looked like magic was happening, not finding the interesting proofs.)
I think I disagree that it’s right to separate them this way, but this may just be a matter of taste / goals. I am far more interested in prescriptive decision theory than normative decision theory (bounded rationality vs. unbounded rationality).
I considered saying that proofs are verifiable by definition. I mean a proof in formal logic. The point of formal logic is that it is computable (even fast) to verify it. The point, which matches the common usage, is that it is convincing. You can’t prove anything about arbitrary code; these algorithms are not guaranteed to understand the opponent. But it’s interesting that sometimes they do succeed in proving things about their opponents.
I’d say it’s easier to prove that a naïve bubble sort runs in quadratic time, than it is to prove that when it terminates, the list is actually sorted. It’s obvious by inspection that it contains a nested loop over the same data structure.