TY - GEN

T1 - Regular expression containment

T2 - 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

AU - Henglein, Fritz

AU - Nielsen, Lasse

N1 - Conference code: 38

PY - 2011

Y1 - 2011

N2 - We present a new sound and complete axiomatization of regular expression containment. It consists of the conventional axiomatiza- tion of concatenation, alternation, empty set and (the singleton set containing) the empty string as an idempotent semiring, the fixed- point rule E* = 1 + E × E* for Kleene-star, and a general coin- duction rule as the only additional rule.Our axiomatization gives rise to a natural computational inter- pretation of regular expressions as simple types that represent parse trees, and of containment proofs as coercions. This gives the axiom- atization a Curry-Howard-style constructive interpretation: Con- tainment proofs do not only certify a language-theoretic contain- ment, but, under our computational interpretation, constructively transform a membership proof of a string in one regular expres- sion into a membership proof of the same string in another regular expression.We show how to encode regular expression equivalence proofs in Salomaa’s, Kozen’s and Grabmayer’s axiomatizations into our containment system, which equips their axiomatizations with a computational interpretation and implies completeness of our ax- iomatization. To ensure its soundness, we require that the compu- tational interpretation of the coinduction rule be a hereditarily total function. Hereditary totality can be considered the mother of syn- tactic side conditions: it “explains” their soundness, yet cannot be used as a conventional side condition in its own right since it turns out to be undecidable.We discuss application of regular expressions as types to bit coding of strings and hint at other applications to the wide-spread use of regular expressions for substring matching, where classical automata-theoretic techniques are a priori inapplicable.Neither regular expressions as types nor subtyping interpreted coercively are novel per se. Somewhat surprisingly, this seems to be the first investigation of a general proof-theoretic framework for the latter in the context of the former, however.

AB - We present a new sound and complete axiomatization of regular expression containment. It consists of the conventional axiomatiza- tion of concatenation, alternation, empty set and (the singleton set containing) the empty string as an idempotent semiring, the fixed- point rule E* = 1 + E × E* for Kleene-star, and a general coin- duction rule as the only additional rule.Our axiomatization gives rise to a natural computational inter- pretation of regular expressions as simple types that represent parse trees, and of containment proofs as coercions. This gives the axiom- atization a Curry-Howard-style constructive interpretation: Con- tainment proofs do not only certify a language-theoretic contain- ment, but, under our computational interpretation, constructively transform a membership proof of a string in one regular expres- sion into a membership proof of the same string in another regular expression.We show how to encode regular expression equivalence proofs in Salomaa’s, Kozen’s and Grabmayer’s axiomatizations into our containment system, which equips their axiomatizations with a computational interpretation and implies completeness of our ax- iomatization. To ensure its soundness, we require that the compu- tational interpretation of the coinduction rule be a hereditarily total function. Hereditary totality can be considered the mother of syn- tactic side conditions: it “explains” their soundness, yet cannot be used as a conventional side condition in its own right since it turns out to be undecidable.We discuss application of regular expressions as types to bit coding of strings and hint at other applications to the wide-spread use of regular expressions for substring matching, where classical automata-theoretic techniques are a priori inapplicable.Neither regular expressions as types nor subtyping interpreted coercively are novel per se. Somewhat surprisingly, this seems to be the first investigation of a general proof-theoretic framework for the latter in the context of the former, however.

U2 - 10.1145/1925844.1926429

DO - 10.1145/1925844.1926429

M3 - Conference article

VL - 46

SP - 385

EP - 398

JO - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)

JF - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)

SN - 1523-2867

IS - 1

Y2 - 26 January 2011 through 28 January 2011

ER -