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

Co-authored-by: Aaron Tomb <[email protected]>

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

@@ -31,7 +31,7 @@ We define the set of formal languages parametric in an alphabet `A` as an coindu
 codatatype Lang<!A> = Alpha(eps: bool, delta: A -> Lang<A>)
 ```
 
-To some, this choice might seem odd at first sight. If you are familiar with the topic, you likely have expected the set of formal languages to be defined more concretely as the set of all sets of finite sequences (sometimes called *words*), `iset<seq<A>>`. Rest assured, we agree — up to an appropriate notion of equality! Where as you characterise languages intrinsically, we treat them extrinsically, in terms of their universal property: [it is well known](https://ir.cwi.nl/pub/28550/rutten.pdf) that `iset<seq<A>>` forms the *greatest* [coalgebraic](https://en.wikipedia.org/wiki/F-coalgebra) structure (think of a deterministic automaton without initial state) `S` that is equipped with functions `eps: S -> bool` and `delta: S → (A → S)`. Indeed, for any set `U` of finite sequences, we can verify whether `U` contains the empty sequence, `U.eps == ([] in U)`, and for any `a: A`, we can transition to the set `U.delta(a) == (iset s | [a] + s in U)`. Here, we choose the more abstract perspective on formal languages at it hides irrelevant specifics and thus allows us to write more elegant proofs.
+To some, this choice might seem odd at first sight. If you are familiar with the topic, you likely have expected the set of formal languages to be defined more concretely as the set of all sets of finite sequences (sometimes called *words*), `iset<seq<A>>`. Rest assured, we agree — up to an appropriate notion of equality! Whereas you characterise languages intrinsically, we treat them extrinsically, in terms of their universal property: [it is well known](https://ir.cwi.nl/pub/28550/rutten.pdf) that `iset<seq<A>>` forms the *greatest* [coalgebraic](https://en.wikipedia.org/wiki/F-coalgebra) structure (think of a deterministic automaton without initial state) `S` that is equipped with functions `eps: S -> bool` and `delta: S → (A → S)`. Indeed, for any set `U` of finite sequences, we can verify whether `U` contains the empty sequence, `U.eps == ([] in U)`, and for any `a: A`, we can transition to the set `U.delta(a) == (iset s | [a] + s in U)`. Here, we choose the more abstract perspective on formal languages at it hides irrelevant specifics and thus allows us to write more elegant proofs.
 
 ### An Algebra of Formal Languages