Brzozowski derivative

The Brzozowski derivative of a regular expression $r$ with respect to a character $a$ is a regular expression $\partial_{a} r$ that matches exactly the strings $w$ for which $a w$ matches $r$ . It is computed from the syntax of $r$ by rules that resemble those of calculus, so a string can be matched by taking one derivative per character and asking at the end whether the result matches the empty string^[1]. Up to a few algebraic identities, every regular expression has only finitely many derivatives, and they are the states of a deterministic finite automaton for it. Because the rules for intersection and complement are as simple as those for union, derivatives give matchers and automata for extended regular expressions with no extra machinery. Brzozowski introduced them in 1964^[1]; Owens, Reppy and Turon revived them in 2009 as a practical way to build lexers^[2].

§ 01

Definition

For a language $L$ over an alphabet $Σ$ and a character $a$ , the derivative is the set of suffixes left after removing a leading $a$ :

\partial_{a} L = {w; ∣; a w \in L}

A string $a_{1} a_{2} \dots a_{n}$ is in $L$ exactly when the empty string is in $\partial_{a_{n}} \dots \partial_{a_{2}} \partial_{a_{1}} L$ . Brzozowski showed that for a language given by a regular expression the derivative is again given by a regular expression, computed by structural rules. With $ν (r)$ true when $r$ matches the empty string^[1]:

\partial_{a} \emptyset \partial_{a} (r s) \partial_{a} (r & s) = \emptyset = (\partial_{a} r) s; +; ν (r) \partial_{a} s = \partial_{a} r & \partial_{a} s \partial_{a} ε \partial_{a} (r + s) \partial_{a} (\neg r) = \emptyset = \partial_{a} r + \partial_{a} s = \neg \partial_{a} r \partial_{a} b \partial_{a} r^{*} = {ε \emptyset a = b a \neq = b = (\partial_{a} r) r^{*}

where $ν (r) s$ means $s$ if $r$ is nullable and $\emptyset$ otherwise. The rule for concatenation is a product rule: the first character is taken either from $r$ , or, if $r$ can be empty, from $s$ . Nullability is itself structural: $ε$ and $r^{*}$ are nullable, a character is not, a concatenation is nullable when both parts are, and a union when either is.

§ 02

Matching

Extended regular expressions with smart constructors, nullability and derivatives.

(* Regular expressions with intersection and complement. Alternation
   and intersection hold sorted lists without duplicates, so that
   associativity, commutativity and idempotence are built in. *)
type t =
  | Empty                   (* matches nothing *)
  | Eps                     (* matches the empty string *)
  | Chr of char
  | Seq of t * t
  | Alt of t list           (* r1 | r2 | ... *)
  | And of t list           (* r1 & r2 & ... *)
  | Star of t
  | Not of t
 
(* Smart constructors: the simplifications that keep derivatives finite. *)
let seq a b = match (a, b) with
  | Empty, _ | _, Empty -> Empty
  | Eps, r | r, Eps -> r
  | Seq (x, y), r -> Seq (x, Seq (y, r))
  | _ -> Seq (a, b)
 
let alt a b =
  let parts = function Alt l -> l | Empty -> [] | r -> [ r ] in
  match List.sort_uniq compare (parts a @ parts b) with
  | [] -> Empty
  | [ r ] -> r
  | l -> if List.mem (Not Empty) l then Not Empty else Alt l
 
let and_ a b =
  let parts = function And l -> l | r -> [ r ] in
  match List.sort_uniq compare (parts a @ parts b) with
  | l when List.mem Empty l -> Empty
  | [ r ] -> r
  | l -> (match List.filter (( <> ) (Not Empty)) l with [] -> Not Empty | [ r ] -> r | l -> And l)
 
let star = function Star _ as r -> r | Eps | Empty -> Eps | r -> Star r
let not_ = function Not r -> r | r -> Not r
 
(* nu(r) holds when r matches the empty string. *)
let rec nullable = function
  | Empty | Chr _ -> false
  | Eps | Star _ -> true
  | Seq (a, b) -> nullable a && nullable b
  | Alt l -> List.exists nullable l
  | And l -> List.for_all nullable l
  | Not r -> not (nullable r)
 
(* The derivative with respect to c: the strings w such that c w matches r. *)
let rec deriv c = function
  | Empty | Eps -> Empty
  | Chr d -> if c = d then Eps else Empty
  | Seq (a, b) -> let d = seq (deriv c a) b in if nullable a then alt d (deriv c b) else d
  | Alt l -> List.fold_left (fun acc r -> alt acc (deriv c r)) Empty l
  | And l -> List.fold_left (fun acc r -> and_ acc (deriv c r)) (Not Empty) l
  | Star r -> seq (deriv c r) (Star r)
  | Not r -> not_ (deriv c r)
 
let matches r s = nullable (String.fold_left (fun r c -> deriv c r) r s)
 
(* Helpers for writing expressions. *)
let str s = String.fold_right (fun c r -> seq (Chr c) r) s Eps
let any_of cs = List.fold_left (fun r c -> alt r (Chr c)) Empty cs
let alts = List.fold_left alt Empty

Matching identifiers, a language defined by intersection and complement, and a sequence of derivatives.

open Re
let letters = any_of (List.init 26 (fun i -> Char.chr (97 + i)))
let digits = any_of (List.init 10 (fun i -> Char.chr (48 + i)))
let sigma = star (any_of [ 'a'; 'b' ])

Running it.

identifier "x"        true
identifier "tail_rec2" true
identifier "2fast"    false
identifier ""         false
ab but not ba "ab"     true
ab but not ba "aabb"   true
ab but not ba "abba"   false
ab but not ba "ba"     false
ab but not ba "aaab"   true
d/da (ab)*    = b(ab)*
d/db b(ab)*   = (ab)*
d/da (ab)*    = b(ab)*
d/db b(ab)*   = (ab)*

The matcher needs no backtracking and no automaton: it keeps one expression, replaces it with its derivative at each character, and inspects nullability at the end. The derivatives of $(ab)^{*}$ alternate between two expressions, $b (ab)^{*}$ after an $a$ and $(ab)^{*}$ after a $b$ , which are the two states of its automaton. The language of strings containing $ab$ but not $ba$ is written directly with intersection and complement; classical constructions go through automata for each part and a product or subset construction.

§ 03

Automata from derivatives

Brzozowski proved that a regular expression has only finitely many derivatives up to similarity, the equivalence generated by associativity, commutativity and idempotence of union^[1]. Taking the distinct derivatives as states, with a transition on $a$ from $r$ to $\partial_{a} r$ and the nullable ones as accepting states, gives a deterministic finite automaton for the expression:

Building a DFA by exploring derivatives, for the language "the (n+1)-th symbol from the end is a".

(* A DFA from derivatives: the states are the distinct derivatives of r,
   found by exploring every character from every state. *)
open Re
 
let dfa alphabet r =
  let states = Hashtbl.create 64 and queue = Queue.create () and trans = ref [] in
  let id r = match Hashtbl.find_opt states r with Some i -> i | None ->
    let i = Hashtbl.length states in Hashtbl.add states r i; Queue.add r queue; i in
  ignore (id r);
  while not (Queue.is_empty queue) do
    let q = Queue.pop queue in
    List.iter (fun c -> trans := (id q, c, id (deriv c q)) :: !trans) alphabet
  done;
  (Hashtbl.length states, states, List.rev !trans)
 
(* (a|b)* a (a|b)^n: the (n+1)-th symbol from the end is an a. *)
let nth_from_end n =
  let ab = any_of [ 'a'; 'b' ] in
  let rec rep k = if k = 0 then Eps else seq ab (rep (k - 1)) in
  seq (star ab) (seq (Chr 'a') (rep n))

Running it.

(a|b)*a(a|b): 4 states
  0 --a--> 1
  0 --b--> 0
  1 --a--> 2
  1 --b--> 3
  2 --a--> 2
  2 --b--> 3
  3 --a--> 1
  3 --b--> 0
  accepting: 2, 3
n     DFA states regex size (symbols)
0              2                    3
1              4                    5
2              8                    7
3             16                    9
4             32                   11
5             64                   13
6            128                   15
7            256                   17

The expression $(a ∣ b)^{*} a (a ∣ b)^{n}$ has size linear in $n$ , and any deterministic automaton for it must remember the last $n + 1$ symbols, so it needs $2^{n + 1}$ states^[6]. The derivative automaton has exactly that many: here it is minimal. That is not guaranteed in general, but with the simplifications of the smart constructors derivative automata are usually close to minimal, and often much smaller than the DFAs produced by the subset construction from an NFA before minimization^[2].

Partial derivatives

Antimirov's partial derivatives split each derivative into a set of expressions, one per way the first character can be consumed, instead of a single union^[3]. The set of partial derivatives of an expression is at most one more than its number of character occurrences, and they form the states of a nondeterministic automaton of linear size, comparable to Thompson's construction^[5] and the position automaton of McNaughton and Yamada^[7].

§ 04

Uses

Owens, Reppy and Turon showed that lexer generators based on derivatives, with character classes as the alphabet, produce automata as small as traditional ones with simpler code, and implemented them in ML-ulex and a Scheme lexer generator^[2]. Derivatives are well suited to proof assistants, since the construction is purely syntactic: Traytel and Nipkow verified decision procedures for monadic second-order logic on words based on them^[8]. Z3 decides string constraints with extended regular expressions using symbolic derivatives^[9], and the .NET regular expression library has a non-backtracking engine built on derivatives that runs in time linear in the input^[10]. Might, Darais and Spiewak extended derivatives from regular expressions to context-free grammars, with laziness and memoization to handle recursion, giving a parser for any context-free grammar^[4]; see also parser combinators.

The derivative of a regular expression is unrelated, except in name and in the shape of the product rule, to the derivative of a data type that gives the zipper, though both remove one element from the front of, or inside, a structure.

§ 05

History

Brzozowski introduced derivatives of regular expressions in 1964, with the finiteness theorem and the automaton construction^[1]. The method was overshadowed for decades by Thompson's NFA construction of 1968^[5] and the subset construction, which suited the imperative implementations of the time. Antimirov's partial derivatives followed in 1996^[3], and Owens, Reppy and Turon's 2009 paper, "Regular-expression derivatives re-examined", brought the method back into practical use^[2].