Lean4
/-- In order to extract a compositional semantics from the sequential execution behavior of
configurations, we observe that continuations have a monoid structure, with `Cont.halt` as the unit
and `Cont.then` as the multiplication. `Cont.then k₁ k₂` runs `k₁` until it halts, and then takes
the result of `k₁` and passes it to `k₂`.
We will not prove it is associative (although it is), but we are instead interested in the
associativity law `k₂ (eval c k₁) = eval c (k₁.then k₂)`. This holds at both the sequential and
compositional levels, and allows us to express running a machine without the ambient continuation
and relate it to the original machine's evaluation steps. In the literature this is usually
where one uses Turing machines embedded inside other Turing machines, but this approach allows us
to avoid changing the ambient type `Cfg` in the middle of the recursion.
-/
def «then» : Cont → Cont → Cont
| Cont.halt => fun k' => k'
| Cont.cons₁ fs as k => fun k' => Cont.cons₁ fs as (k.then k')
| Cont.cons₂ ns k => fun k' => Cont.cons₂ ns (k.then k')
| Cont.comp f k => fun k' => Cont.comp f (k.then k')
| Cont.fix f k => fun k' => Cont.fix f (k.then k')
