From 4eabd3998565a0402e81e65d203fe7a1d7bc7874 Mon Sep 17 00:00:00 2001 From: Felix Tripier Date: Sat, 20 Jan 2018 15:26:26 -0800 Subject: [PATCH] Fix small typo in correctness and complexity --- posts/correctness-and-complexity.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/posts/correctness-and-complexity.html b/posts/correctness-and-complexity.html index 2b34109..1894598 100644 --- a/posts/correctness-and-complexity.html +++ b/posts/correctness-and-complexity.html @@ -479,7 +479,7 @@

Limiting our Scope

-

Yet mathematicians have failed to prove that this program never fails (i.e., reaches crash()) for 270 years. The program will crash iff Goldbach’s conjecture is false (of course, assuming we replace int with some larger integer type; we know it holds for 32-bit integers, but we’re not sure about 64-bit integers). At this point, some of you may say, “well of course proving the behavior of programs that encode hard number theory problems would be hard!” but that would be misunderstands the problem. Noticing that this program encodes a well-known hard problem in number theory is just a way of convincing ourselves that verifying this particular program is indeed hard. But it doesn’t tell us that this program is any harder to verify than programs we encounter regularly. If we didn’t know that the program corresponds to Goldbach’s conjecture (or if Goldbach never made the conjecture), would we be able to tell that the program would be so hard to verify by looking at it?

+

Yet mathematicians have failed to prove that this program never fails (i.e., reaches crash()) for 270 years. The program will crash iff Goldbach’s conjecture is false (of course, assuming we replace int with some larger integer type; we know it holds for 32-bit integers, but we’re not sure about 64-bit integers). At this point, some of you may say, “well of course proving the behavior of programs that encode hard number theory problems would be hard!” but that would be misunderstanding the problem. Noticing that this program encodes a well-known hard problem in number theory is just a way of convincing ourselves that verifying this particular program is indeed hard. But it doesn’t tell us that this program is any harder to verify than programs we encounter regularly. If we didn’t know that the program corresponds to Goldbach’s conjecture (or if Goldbach never made the conjecture), would we be able to tell that the program would be so hard to verify by looking at it?

Now, there are various other ways we can restrict our computational model. For example, Stephen Bellantoni and Stephen Cook invented a language where every program is computable in PTIME20. Another model is pushdown-automata (PDA). That one is interesting and tricky – as many PDA properties can be verified even though the model admits an infinite number of states, but languages based on it can become Turing complete with a slight breeze (e.g. two PDAs communicating are Turing complete).