Matching problem for regular expressions with variables

Abstract

The notion of a backreference in practical regular expressions is formalised giving rise to a novel notion of a regular expression with variables. So far the state-of-the-art in formal languages theory of practical regular expressions with backreferences was represented by an operational matching semantics of trees of valid matches. Since explicit tree data structures are required only in procedural languages where functional list combinators are not available, this provides an opportunity for functional programming to step in with a computationally and proof-theoretically more tangible definition of backreferences and their matching semantics. An operational notion of (NP-complete) exhaustive pattern matching is provided that relies on a fundamental construction of partial derivatives of regular expressions. Matching is proved sound and complete. © 2013 Springer-Verlag.