Alexandra comment 2

_posts/2024-01-10-semantics-of-regular-expressions.markdown

@@ -7,7 +7,7 @@ author: Stefan Zetzsche and Wojciech Różowski
 
 ## Introduction
 
-[Regular expressions](https://en.wikipedia.org/wiki/Regular_expression) are one of the most ubiquitous formalisms of theoretical computer science. Commonly, they are understood in terms of their [*denotational* semantics](https://en.wikipedia.org/wiki/Denotational_semantics), that is, through formal languages — the [*regular* languages](https://en.wikipedia.org/wiki/Regular_language). 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](https://en.wikipedia.org/wiki/Operational_semantics), that is, through the [finite automata](https://en.wikipedia.org/wiki/Finite-state_machine) they induce. 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](http://www.dlsi.ua.es/~mlf/nnafmc/papers/kleene56representation.pdf) 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](https://homepages.inf.ed.ac.uk/gdp/publications/Math_Op_Sem.pdf)*, in the sense they are in fact one and the same, up to pointwise [bisimulation](https://en.wikipedia.org/wiki/Bisimulation). 
+[Regular expressions](https://en.wikipedia.org/wiki/Regular_expression) are one of the most ubiquitous formalisms of theoretical computer science. Commonly, they are understood in terms of their [*denotational* semantics](https://en.wikipedia.org/wiki/Denotational_semantics), that is, through formal languages — the [*regular* languages](https://en.wikipedia.org/wiki/Regular_language). 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](https://en.wikipedia.org/wiki/Operational_semantics), that is, through [finite automata](https://en.wikipedia.org/wiki/Finite-state_machine). 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](http://www.dlsi.ua.es/~mlf/nnafmc/papers/kleene56representation.pdf) 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](https://homepages.inf.ed.ac.uk/gdp/publications/Math_Op_Sem.pdf)*, in the sense they are in fact one and the same, up to pointwise [bisimulation](https://en.wikipedia.org/wiki/Bisimulation). 
 
 ## Denotational Semantics