Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny

[stefan-aws]

Regular expressions are one of the most ubiquitous formalisms of theoretical computer science. Commonly, they are understood in terms of their denotational semantics, that is, through formal languages — the regular languages. This view is inductive in nature: two primitives are equivalent if they are constructed in the same way. Alternatively, regular expressions can be understood in terms of their operational semantics, that is, through finite automata. This view is coinductive in nature: two primitives are equivalent if they are deconstructed in the same way. It is implied by Kleene’s famous theorem that both views are equivalent: regular languages are precisely the formal languages accepted by finite automata. In this blogpost, we utilise Dafny’s built-in inductive and coinductive reasoning capabilities to show that the two semantics of regular expressions are well-behaved, in the sense they are in fact one and the same, up to pointwise bisimulation.

[atomb]

This is a very nice post! I just have a few suggestions for improved wording here and there. It also might be nice to use the syntax highlighting that some other recent posts used, though that's not essential.

[RustanLeino]

This is an interesting and very clear blog post. Well done!

[atomb]

I saw a couple of tiny things to fix, but otherwise think this looks great.

[stefan-aws]

Content is ready for review. However, turning this temporarily into a draft to implement the changes needed for @jtristan's tool that automatically verifies code snippets.

Content previously approved. Only changed the stylesheet. Agreed offline