Regular expression containment: coinductive axiomatization and computational interpretation
Research output: Contribution to journal › Conference article › Research › peer-review
Standard
Regular expression containment : coinductive axiomatization and computational interpretation. / Henglein, Fritz; Nielsen, Lasse.
In: A C M / S I G P L A N Notices, Vol. 46, No. 1, 2011, p. 385-398.Research output: Contribution to journal › Conference article › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
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 -
ID: 37560029