Quick disclaimer: The ideas in this blog post are not my original work. I am paraphrasing from lectures given by both Nate Foster and Dexter Kozen at Cornell University, and adding some of my own intuition and insights where I think it is helpful. My intent is to increase awareness of a cool thing that I am excited about, not to pass any of this work off as my own.
Regular expressions come up a lot in computer science. From a theory perspective, they are a compact and intuitive way to understand regular languages. In practice, they allow programmers to recognize phone numbers, search for files, and even parse HTML.1 Up until about a month ago, I thought I knew everything I wanted to know about regular expressions, and then I discovered Brzozowski derivatives.
Before I start, let’s take a step back and define exactly what we mean by regular expressions. Here’s a nice inductive definition:
Note that this definition is minimal—I don’t include things like or because they can be written in terms of the other operators. One bit of common notation that I will use is to instead of ; both are the regular expression denoting the empty string.
At this point, I’ll assume you have a general understanding of how to interpret regular expressions; so if I write , you should know that it denotes any string that is either zero or more ’s followed zero or more ’s, or just .
The Brzozowski Derivative
With notation out of the way, we can start to look at what a Brzozowski derivative is.2 Intuitively, it is a way of partially interpreting a regular expression. The derivative of with respect to a character , , is a new regular expression that matches all strings from that started with an , but without the . We “take off the front of ”. For example,
Since doesn’t start with a , we dropped that part of the expression altogether. For each of the other pieces, we just took a off of the front.
Now that we understand what we’re going for, let’s actually define a way to compute . We’ll do it inductively, step by step.
This one should be pretty obvious. If you take off of every string in … well there were no strings to begin with.
The idea here is that if you try to take off of the string , you get an empty string back, and if you try to take off of the string (where is some character that isn’t ), you just can’t do it.
If you want to take an off the front of an alternation, you can either take it off of the first expression, or off of the second.
Uh oh. What does mean? It’s actually totally straightforward, and I’ll define it in detail soon. For now, just know that if can denote the empty string, and otherwise. With that in mind, this statement says that taking off of a concatenation either means taking off of the first expression, or if the first expression can be empty taking off of the second expression.
Finally, we can say that taking an off of a sequence of ’s means taking off of the first , and leaving a sequence of ’s after that. This looks a little silly, but if you play around with it for a bit, it should make sense.3
Let’s go back and define , which we’ll call the observation function. Remember that it “observes” whether can denote the empty string, and returns or accordingly. Here’s the definition:
The only tricky thing here is convincing yourself that the and cases work. These facts might help:4
It turns out that will be more important than just helping us define the derivative. We can actually use the observation function to tell us about which strings match a given expression.
We’re finally ready to implement a regular expression matcher. Let’s can extend our derivative function from earlier to handle entire strings:
You can think of this as taking a derivative with respect to each character of the string, in order, and accumulating the result. I now claim that matches a string if and only if
So how does this work? Well, goes character-by-character in , taking each character off of . This means that by the end, we will have a regular expression that matches everything left in after taking the string off the front.
If we take off of the strings in and that set contains the empty string, then it must be the case that was in to start with! Conversely, if we know that matched to start with, then removing from would leave us with .
Practically, this means that we can use Brzozowski derivatives to write regular expression matchers in code! I have a Haskell implementation as a gist on GitHub that you can check out, and I am also currently writing a verified version in Coq.
Why I’m Excited
When I first learned about regular expressions formally, we were given a process for implementing them:
- Transform the regular expression into an -NFA, using a Thompson construction.
- Turn that -NFA into a normal NFA.
- Determinize the NFA to get a DFA.
- Run the DFA on the input string.
There are things that I love about this algorithm too. It relies on the amazing result that regular expressions, NFAs, and DFAs are all the same, and the Thompson construction itself is really brilliant. But there’s just something that feels so nice and PL-ey about the derivative approach. Rather than deal with intermediate representations and stateful algorithms, we can just define our desired result by induction, and write pure functions that capture our intent. The Brzozowski derivatives are also totally symbolic. The whole process is just replacing symbols with other symbols, which obviates the need for any complex reasoning.
Ultimately, this algorithm captures the reason that I study programming languages. For me, doing computer science isn’t about just solving the problem.5 It’s about seeing the structure of the problem that you are working with, and letting that structure guide you to an answer. It’s about avoiding complex decision procedures in favor of symbolic manipulations that simplify and transform your goal. At the end of the day, Brzozowski derivatives are just a different way of looking at regular expressions—but I think they’re a really freaking cool way of looking at regular expressions, so I wrote a blog post.
Technically, this is the Brzozowski Syntactic Derivative. There is also a Semantic Derivative that deals with DFAs and their denotations. ↩
If you reeeeally squint at these last two definitions you might see something familiar. The concatenation and star rules here are similar in structure to the product and power rules for derivatives in calculus. I doubt this is just a coincidence. If I find a satisfying reason why, I’ll probably write another post about it. ↩
I’m being sort of sloppy with my notation around equality. What I really mean is that , etc., so might not actually be equal to or , but it will always be denotationally equal to one or the other. ↩
To be clear, there’s nothing wrong with “just solving the problem”—in fact, that’s usually a far more effective approach. ↩