View source

From thelas.dk

You do not have permission to do that, for the following reason:

The action you have requested is limited to users in the group Sysops.

You can view and copy the source of this page:

== Abstract ==
<p>
We present a new sound and complete axiomatization of regular
expression containment.  It consists of the conventional
axiomatization of concatenation, alternation, empty set and (the
singleton set containing) the empty string as an idempotent semiring,
the fixed-point rule E*=1+EE* for Kleene-star, and a general
coinduction rule as the only additional rule.
</p>
<p>
Our axiomatization gives rise to a natural  
computational interpretation
of regular expressions as simple types that represent parse
trees, and of containment proofs as '''coercions'''.
This gives the axiomatization a Curry-Howard-style constructive 
interpretation: Containment proofs do not only certify a language-theoretic 
containment, but, under our computational interpretation,
constructively transform a membership proof of a string in one regular expression
into a membership proof of the same string in another regular expression.
</p>
<p>
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 axiomatization.
To ensure its soundness, we require that the computational interpretation of the 
coinduction rule be a hereditarily total function.
Hereditary totality can be considered the mother of syntactic 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.  
</p>
<p>
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 \emph{a priori} inapplicable.
</p>
<p>
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. 
</p>
<p>
This paper is joint work with Fritz Henglein, and was presented at POPL-2011.
</p>

Return to Regular Expression Containment.

Retrieved from "http://thelas.dk/index.php?title=Regular_Expression_Containment"

View source

From thelas.dk

Views

Personal tools