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

…23)

[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).

---------

Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
Co-authored-by: Rustan Leino <leino@amazon.com>

Makefile

@@ -17,6 +17,7 @@ check:
 	assets/src/brittleness/verify.sh
 	assets/src/teaching-material/verify.sh
 	assets/src/standard-libraries/test.sh
+	assets/src/semantics-of-regular-expressions/verify.sh
 	(cd assets/src/clear-specification-and-implementation && ./verify.sh)
 
 generate:

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

@@ -0,0 +1,8 @@
+---
+layout: post
+title:  "Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny"
+author: Stefan Zetzsche and Wojciech Różowski
+date:   2024-01-12 18:00:00 +0100
+---
+
+{% include semantics-of-regular-expressions.html %}

assets/src/semantics-of-regular-expressions/Expressions.dfy

@@ -0,0 +1,28 @@
+module Expressions0 {
+  datatype Exp<A> = Zero | One | Char(A) | Plus(Exp, Exp) | Comp(Exp, Exp) | Star(Exp)
+}
+
+module Expressions1 {
+  import opened Expressions0
+
+  function Eps<A>(e: Exp): bool {
+    match e
+    case Zero => false
+    case One => true
+    case Char(a) => false
+    case Plus(e1, e2) => Eps(e1) || Eps(e2)
+    case Comp(e1, e2) => Eps(e1) && Eps(e2)
+    case Star(e1) => true
+  }
+
+  function Delta<A(==)>(e: Exp): A -> Exp {
+    (a: A) =>
+      match e
+      case Zero => Zero
+      case One => Zero
+      case Char(b) => if a == b then One else Zero
+      case Plus(e1, e2) => Plus(Delta(e1)(a), Delta(e2)(a))
+      case Comp(e1, e2) => Plus(Comp(Delta(e1)(a), e2), Comp(if Eps(e1) then One else Zero, Delta(e2)(a)))
+      case Star(e1) => Comp(Delta(e1)(a), Star(e1))
+  }
+}

assets/src/semantics-of-regular-expressions/Languages.dfy

@@ -0,0 +1,266 @@
+module Languages0 {
+  codatatype Lang<!A> = Alpha(eps: bool, delta: A -> Lang<A>)
+}
+
+module Languages1 {
+  import opened Languages0
+
+  function Zero<A>(): Lang {
+    Alpha(false, (a: A) => Zero())
+  }
+}
+
+module Languages2 {
+  import opened Languages0
+  import opened Languages1
+
+  function One<A>(): Lang {
+    Alpha(true, (a: A) => Zero())
+  }
+
+  function Singleton<A(==)>(a: A): Lang {
+    Alpha(false, (b: A) => if a == b then One() else Zero())
+  }
+
+  function {:abstemious} Plus<A>(L1: Lang, L2: Lang): Lang {
+    Alpha(L1.eps || L2.eps, (a: A) => Plus(L1.delta(a), L2.delta(a)))
+  }
+
+  function {:abstemious} Comp<A>(L1: Lang, L2: Lang): Lang {
+    Alpha(
+      L1.eps && L2.eps,
+      (a: A) => Plus(Comp(L1.delta(a), L2), Comp(if L1.eps then One() else Zero(), L2.delta(a)))
+    )
+  }
+
+  function Star<A>(L: Lang): Lang {
+    Alpha(true, (a: A) => Comp(L.delta(a), Star(L)))
+  }
+}
+
+module Languages3 {
+  import opened Languages0
+  import opened Languages1
+  import opened Languages2
+
+  greatest predicate Bisimilar<A(!new)>[nat](L1: Lang, L2: Lang) {
+    && (L1.eps == L2.eps)
+    && (forall a :: Bisimilar(L1.delta(a), L2.delta(a)))
+  }
+}
+
+module Languages4 {
+  import opened Languages0
+  import opened Languages1
+  import opened Languages2
+  import opened Languages3
+
+  greatest lemma BisimilarityIsReflexive<A(!new)>[nat](L: Lang)
+    ensures Bisimilar(L, L)
+  {}
+}
+
+module Languages5 {
+  import opened Languages0
+  import opened Languages1
+  import opened Languages2
+  import opened Languages3
+  import opened Languages4
+
+  greatest lemma PlusCongruence<A(!new)>[nat](L1a: Lang, L1b: Lang, L2a: Lang, L2b: Lang)
+    requires Bisimilar(L1a, L1b)
+    requires Bisimilar(L2a, L2b)
+    ensures Bisimilar(Plus(L1a, L2a), Plus(L1b, L2b))
+  {}
+
+  lemma CompCongruence<A(!new)>(L1a: Lang, L1b: Lang, L2a: Lang, L2b: Lang)
+    requires Bisimilar(L1a, L1b)
+    requires Bisimilar(L2a, L2b)
+    ensures Bisimilar(Comp(L1a, L2a), Comp(L1b, L2b))
+}
+
+module Languages5WithProof refines Languages5 {
+  lemma CompCongruence<A(!new)>(L1a: Lang<A>, L1b: Lang<A>, L2a: Lang<A>, L2b: Lang<A>)
+    ensures Bisimilar(Comp(L1a, L2a), Comp(L1b, L2b))
+  {
+    forall k: nat
+      ensures Bisimilar#[k](Comp(L1a, L2a), Comp(L1b, L2b))
+    {
+      if k != 0 {
+        var k' :| k' + 1 == k;
+        CompCongruenceHelper(k', L1a, L1b, L2a, L2b);
+      }
+    }
+  }
+
+  lemma CompCongruenceHelper<A(!new)>(k: nat, L1a: Lang, L1b: Lang, L2a: Lang, L2b: Lang)
+    requires forall n : nat :: n <= k + 1 ==> Bisimilar#[n](L1a, L1b)
+    requires forall n : nat :: n <= k + 1 ==> Bisimilar#[n](L2a, L2b)
+    ensures Bisimilar#[k+1](Comp(L1a, L2a), Comp(L1b, L2b))
+  {
+    var lhs := Comp(L1a, L2a);
+    var rhs := Comp(L1b, L2b);
+
+    assert Bisimilar#[1](L1a, L1b);
+    assert Bisimilar#[1](L2a, L2b);
+    assert lhs.eps == rhs.eps;
+
+    forall a
+      ensures (Bisimilar#[k](lhs.delta(a), rhs.delta(a)))
+    {
+      var x1 := Comp(L1a.delta(a), L2a);
+      var x2 := Comp(L1b.delta(a), L2b);
+      assert Bisimilar#[k](x1, x2) by {
+        if k != 0 {
+          BisimilarCuttingPrefixesPointwise(k, a, L1a, L1b);
+          var k' :| k == k' + 1;
+          CompCongruenceHelper(k', L1a.delta(a), L1b.delta(a), L2a, L2b);
+        }
+      }
+      var y1 := Comp(if L1a.eps then One() else Zero(), L2a.delta(a));
+      var y2 := Comp(if L1b.eps then One() else Zero(), L2b.delta(a));
+      assert Bisimilar#[k](y1, y2) by {
+        assert L1a.eps == L1b.eps;
+        if k != 0 {
+          if L1a.eps {
+            BisimilarityIsReflexive<A>(One());
+            BisimilarCuttingPrefixesPointwise(k, a, L2a, L2b);
+            var k' :| k == k' + 1;
+            CompCongruenceHelper(k', One<A>(), One<A>(), L2a.delta(a), L2b.delta(a));
+          } else {
+            BisimilarityIsReflexive<A>(Zero());
+            BisimilarCuttingPrefixesPointwise(k, a, L2a, L2b);
+            var k' :| k == k' + 1;
+            CompCongruenceHelper(k', Zero<A>(), Zero<A>(), L2a.delta(a), L2b.delta(a));
+          }
+        }
+      }
+      PlusCongruenceAlternative(k, x1, x2, y1, y2);
+    }
+  }
+
+  lemma PlusCongruenceAlternative<A>(k: nat, L1a: Lang, L1b: Lang, L2a: Lang, L2b: Lang)
+    requires Bisimilar#[k](L1a, L1b)
+    requires Bisimilar#[k](L2a, L2b)
+    ensures Bisimilar#[k](Plus(L1a, L2a), Plus(L1b, L2b))
+  {}
+
+
+  lemma BisimilarCuttingPrefixesPointwise<A(!new)>(k: nat, a: A, L1a: Lang, L1b: Lang)
+    requires k != 0
+    requires forall n: nat :: n <= k + 1 ==> Bisimilar#[n](L1a, L1b)
+    ensures forall n: nat :: n <= k ==> Bisimilar#[n](L1a.delta(a), L1b.delta(a))
+  {
+    forall n: nat
+      ensures n <= k ==> Bisimilar#[n](L1a.delta(a), L1b.delta(a))
+    {
+      if n <= k {
+        BisimilarCuttingPrefixes(n, L1a, L1b);
+      }
+    }
+  }
+
+  lemma BisimilarCuttingPrefixes<A(!new)>(k: nat, L1: Lang, L2: Lang)
+    requires forall n: nat :: n <= k + 1 ==> Bisimilar#[n](L1, L2)
+    ensures forall a :: Bisimilar#[k](L1.delta(a), L2.delta(a))
+  {
+    forall a
+      ensures Bisimilar#[k](L1.delta(a), L2.delta(a))
+    {
+      if k != 0 {
+        assert Bisimilar#[k + 1](L1, L2);
+      }
+    }
+  }
+}
+
+module Languages6 {
+  import opened Languages0
+  import opened Languages1
+  import opened Languages2
+  import opened Languages3
+  import opened Languages4
+  import opened Languages5WithProof
+
+  greatest lemma BisimilarityIsTransitive<A>[nat](L1: Lang, L2: Lang, L3: Lang)
+    requires Bisimilar(L1, L2) && Bisimilar(L2, L3)
+    ensures Bisimilar(L1, L3)
+  {}
+}
+
+module Languages7 {
+  import opened Languages0
+  import opened Languages1
+  import opened Languages2
+  import opened Languages3
+  import opened Languages4
+  import opened Languages5WithProof
+  import opened Languages6
+  greatest lemma BisimilarityIsSymmetric<A(!new)>[nat](L1: Lang, L2: Lang)
+    ensures Bisimilar(L1, L2) ==> Bisimilar(L2, L1)
+    ensures Bisimilar(L1, L2) <== Bisimilar(L2, L1)
+  {}
+
+  lemma StarCongruence<A(!new)>(L1: Lang, L2: Lang)
+    requires Bisimilar(L1, L2)
+    ensures Bisimilar(Star(L1), Star(L2))
+}
+
+module Languages7WithProof refines Languages7 {
+  lemma StarCongruence<A(!new)>(L1: Lang<A>, L2: Lang<A>)
+    ensures Bisimilar(Star(L1), Star(L2))
+  {
+    forall k: nat
+      ensures Bisimilar#[k](Star(L1), Star(L2))
+    {
+      if k != 0 {
+        var k' :| k' + 1 == k;
+        StarCongruenceHelper(k', L1, L2);
+      }
+    }
+  }
+
+  lemma StarCongruenceHelper<A(!new)>(k: nat, L1: Lang, L2: Lang)
+    requires forall n: nat :: n <= k + 1 ==> Bisimilar#[n](L1, L2)
+    ensures Bisimilar#[k+1](Star(L1), Star(L2))
+  {
+    forall a
+      ensures Bisimilar#[k](Star(L1).delta(a), Star(L2).delta(a))
+    {
+      if k != 0 {
+        BisimilarCuttingPrefixesPointwise(k, a, L1, L2);
+        var k' :| k == k' + 1;
+        forall n: nat
+          ensures n <= k' + 1 ==> Bisimilar#[n](Star(L1), Star(L2))
+        {
+          if 0 < n <= k' + 1 {
+            var n' :| n == n' + 1;
+            StarCongruenceHelper(n', L1, L2);
+          }
+        }
+        CompCongruenceHelper(k', L1.delta(a), L2.delta(a), Star(L1), Star(L2));
+      }
+    }
+  }
+}
+
+module Languages8 {
+  import opened Languages0
+  import opened Languages1
+  import opened Languages2
+  import opened Languages3
+  import opened Languages4
+  import opened Languages5WithProof
+  import opened Languages6
+  import opened Languages7WithProof
+
+  lemma BisimilarityIsTransitiveAlternative<A(!new)>(L1: Lang, L2: Lang, L3: Lang)
+    ensures Bisimilar(L1, L2) && Bisimilar(L2, L3) ==> Bisimilar(L1, L3)
+  {
+    if Bisimilar(L1,L2) && Bisimilar(L2, L3) {
+      assert Bisimilar(L1, L3) by {
+        BisimilarityIsTransitive(L1, L2, L3);
+      }
+    }
+  }
+}