Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny
Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny
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, …