Posts tagged "theory"
 P /= NP, Vinay Deolalikar August 9, 2010
 P and NP August 24, 2010
 David Berlinski, The Devil's Delusion: Turing machine and abacus September 18, 2010
 Some misconceptions about the CAP Theorem September 29, 2010
 Knights, knaves, and Program Construction November 11, 2010
 Measured Finger Trees December 11, 2010
 Speaking of Peano arithmetic... December 15, 2010
 Tony Morris on static types May 9, 2011
 Diagonalization and the Continuum Hypothesis May 27, 2011
 Link o' the Day: Markets are Efficient If and Only If P = NP August 24, 2011
 Link o' the day: Donald Knuth, Tony Hoare, and goto November 4, 2011
 Mad science, abstract data types, and objects December 12, 2011
 Link o' the day: Set Theory December 15, 2011
 Link o' the day: The halting poem March 14, 2012
 Link o' the day: Matt Might on parsing with derivatives March 31, 2012
 Logicomix May 28, 2012
 Quote o' the day: proofs and algorithms June 12, 2012
 Update to "Mad science, abstract data types, and objects" July 13, 2012
 On the definition of object oriented programming July 14, 2012
 The worst notational abuse October 17, 2013
 Link o' the day: static vs. dynamic typing battles January 14, 2014
 Typesafe C? August 8, 2014
 Turing machines vs. other models of computation October 30, 2014
 Quicksort February 14, 2016

A deep dive into regular expression derivatives for lexical analysis August 15, 2016
Although I (embarrassingly) never completed the project, I have written before on derivativebased parsing,^{1} the work of Matt Might and others. The recent appearance of On the Complexity and Performance of Parsing with Derivatives and a certain immediate interest in parsing reawakened my curiosity about the subject. (And no, it’s not because Might’s derivativeparsing tool is called Derp (but as an added bonus, the pure recognizer version is “herp” (and the accompanying regular expression package is “rerp”)).^{2}) In this particular post, I would like to demonstrate why I think the technique is cool, by demonstrating that derivativebased regular expressions are cool.
To that end, I’ll start with regular expression matching, then go on to the conversion to a deterministic finite automaton and finally discuss the minor extras needed to build a lexical analyzer, similar to lex or flex (but better).
Read more… 
Applied Formal Logic: Brute Force String Search June 19, 2017
Need is there, but tools are not.
– zzz95
Let’s play with FramaC.
Read more… 
Applied Formal Logic: The bug in Quick Search June 23, 2017
In my last post, I presented a brief introduction to FramaC and to the process of verifying properties about a very simple C function, a brute force string search. This time around, I intended to do roughly the same thing, using a slightly more complicated function, a faster string searching algorithm. Unfortunately, in doing so, I found a bug in the algorithm. Admittedly, the bug is rather minor and should not affect the actual behavior of an implementation in practice, but still, it is doing something it shouldn’t ought to be doing.
The string searching algorithm I am looking at this time is Quick Search, so named by Daniel M. Sunday in 1990 because it “is a simple, fast, practical algorithm [and] because it can be both coded and debugged quickly” (“A Very Fast Substring Search Algorithm” [PDF]. It is my personal favorite string search because it is, indeed, simple, fast, and practical. Let me quickly show why.
Read more…