Skip to content

Fix small typo in correctness and complexity #3

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
ftripier wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Fix small typo in correctness and complexity #3

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion posts/correctness-and-complexity.html
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -479,7 +479,7 @@ <h2 id="limiting-our-scope">Limiting our Scope</h2>
</code></pre>
</div>

<p>Yet mathematicians have failed to prove that this program never fails (i.e., reaches <code class="highlighter-rouge">crash()</code>) for 270 years. The program will crash iff Goldbach’s conjecture is false (of course, assuming we replace <code class="highlighter-rouge">int</code> 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?</p>
<p>Yet mathematicians have failed to prove that this program never fails (i.e., reaches <code class="highlighter-rouge">crash()</code>) for 270 years. The program will crash iff Goldbach’s conjecture is false (of course, assuming we replace <code class="highlighter-rouge">int</code> 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?</p>

<p>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 PTIME<sup id="fnref:BellantoniCook"><a href="#fn:BellantoniCook" class="footnote">20</a></sup>. Another model is <a href="https://en.wikipedia.org/wiki/Pushdown_automaton">pushdown-automata</a> (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).</p>

Expand Down