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

TL;DR

Dafny, a verification-aware programming language, is used to formally verify, for the first time, what has been previously established only through proofs-by-hand: the two semantics of regular expressions are well-behaved, in the sense that they are in fact one and the same, up to pointwise bisimilarity.

Abstract

Regular expressions are commonly 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 deterministic 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 deterministic finite automata. In this paper, we use Dafny, a verification-aware programming language, to formally verify, for the first time, what has been previously established only through proofs-by-hand: the two semantics of regular expressions are well-behaved, in the sense that they are in fact one and the same, up to pointwise bisimilarity. At each step of our formalisation, we propose an interpretation in the language of Coalgebra. We found that Dafny is particularly well suited for the task due to its inductive and coinductive features and hope our approach serves as a blueprint for future generalisations to other theories.

Figures (4)

• Figure 1: The triptych of regular expressions, deterministic finite automata, and regular languages.
• Figure 2: The compilation pipeline of Dafny.
• Figure 3: and as induced unique $\Sigma$-algebra and $B$-coalgebra homomorphisms, respectively.
• Figure 4: The and semantics of regular expressions are well-behaved.