Memoized Derivatives for Fast Filtering and Schema Validation of Semi-Structured Data

We present a high-performance filtering and schema-validation algorithm based on Brzozowski’s derivatives, extended to regular hedge grammars for semi-structured data. Our algorithm inherits the expressiveness of regular hedge grammars to support a wide range of schema languages and serialization formats, such as JSON Schema, RELAX NG for XML, and Protocol Buffers. High performance is achieved by refactoring the derivative algorithm to make it more amenable to memoization of hedges. We verify in Lean that our memoization technique is correct: our memoized filtering and validation algorithm is equivalent to the denotational semantics of regular hedge grammars. This is the first proof of correctness in an interactive theorem prover of a derivative algorithm for regular hedge grammars or schema languages. We combine the memoization technique with the fusion of the parsing and derivative algorithms to avoid creating intermediate parsing data structures. Benchmarking is done on an implementation in Go against several other JSON Schema implementations. We end up with the fastest library in the filtering use case when considering median latency, providing evidence that derivatives are a competitive approach for validation, even for semi-structured data.