Trouble to understand Agda's Coinduction

Question

I'm trying to code a functional semantics for IMP language with parallel preemptive scheduling as presented in section 4 of the following paper.

I'm using Agda 2.5.2 and Standard library 0.13. Also, the whole code is available at the following gist.

First of all, I've defined the syntax of the language in question as inductive types.

  data Exp (n : ℕ) : Set where
    $_  : ℕ → Exp n
    Var : Fin n → Exp n
    _⊕_ : Exp n → Exp n → Exp n

  data Stmt (n : ℕ) : Set where
    skip : Stmt n
    _≔_ : Fin n → Exp n → Stmt n
    _▷_ : Stmt n → Stmt n → Stmt n
    iif_then_else_ : Exp n → Stmt n → Stmt n → Stmt n
    while_do_ : Exp n → Stmt n → Stmt n
    _∥_ : Stmt n → Stmt n → Stmt n
    atomic : Stmt n → Stmt n
    await_do_ : Exp n → Stmt n → Stmt n

The state is just a vector of natural numbers and expression semantics is straightforward.

  σ_ : ℕ → Set
  σ n = Vec ℕ n

  ⟦_,_⟧ : ∀ {n} → Exp n → σ n → ℕ
  ⟦ $ n , s ⟧ = n
  ⟦ Var v , s ⟧ = lookup v s
  ⟦ e ⊕ e' , s ⟧ = ⟦ e , s ⟧ + ⟦ e' , s ⟧

Then, I defined the type of resumptions, which are some sort of delayed computations.

  data Res (n : ℕ) : Set where
    ret : (st : σ n) → Res n
    δ   : (r : ∞ (Res n)) → Res n
    _∨_ : (l r : ∞ (Res n)) → Res n
    yield : (s : Stmt n)(st : σ n) → Res n

Next, following 1, I define sequential and parallel execution of statements

  evalSeq : ∀ {n} → Stmt n → Res n → Res n
  evalSeq s (ret st) = yield s st
  evalSeq s (δ r) = δ (♯ (evalSeq s (♭ r)))
  evalSeq s (l ∨ r) = ♯ evalSeq s (♭ l) ∨  ♯ evalSeq s (♭ r)
  evalSeq s (yield s' st) = yield (s ▷ s') st

  evalParL : ∀ {n} → Stmt n → Res n → Res n
  evalParL s (ret st) = yield s st
  evalParL s (δ r) = δ (♯ evalParL s (♭ r))
  evalParL s (l ∨ r) = ♯ evalParL s (♭ l) ∨ ♯ evalParL s (♭ r)
  evalParL s (yield s' st) = yield (s ∥ s') st

  evalParR : ∀ {n} → Stmt n → Res n → Res n
  evalParR s (ret st) = yield s st
  evalParR s (δ r) = δ (♯ evalParR s (♭ r))
  evalParR s (l ∨ r) = ♯ evalParR s (♭ l) ∨ ♯ evalParR s (♭ r)
  evalParR s (yield s' st) = yield (s' ∥ s) st

So far, so good. Next, I need to define statement evaluation function mutually with a operation to close (execute suspended computations) in a resumption.

  mutual
    close : ∀ {n} → Res n → Res n
    close (ret st) = ret st
    close (δ r) = δ (♯ close (♭ r))
    close (l ∨ r) = ♯ close (♭ l) ∨ ♯ close (♭ r)
    close (yield s st) = δ (♯ eval s st)

    eval : ∀ {n} → Stmt n → σ n → Res n
    eval skip st = ret st
    eval (x ≔ e) st = δ (♯ (ret (st [ x ]≔ ⟦ e , st ⟧ )))
    eval (s ▷ s') st = evalSeq s (eval s' st)
    eval (iif e then s else s') st with ⟦ e , st ⟧
    ...| zero = δ (♯ yield s' st)
    ...| suc n = δ (♯ yield s st)
    eval (while e do s) st with ⟦ e , st ⟧
    ...| zero = δ (♯ ret st)
    ...| suc n = δ (♯ yield (s ▷ while e do s) st )
    eval (s ∥ s') st = (♯ evalParR s' (eval s st)) ∨ (♯ evalParL s (eval s' st))
    eval (atomic s) st = {!!} -- δ (♯ close (eval s st))
    eval (await e do s) st = {!!}

Agda's totality checker complains when I try to fill the hole in eval equation for atomic constructor with δ (♯ close (eval s st)) saying that termination checking fails for several points in both eval and close function.

My questions about this problem are:

1) Why is Agda termination checking complaining about these definitions? It appears to me that the call δ (♯ close (eval s st)) is fine since it is done on a structurally smaller statement.

2) Current Agda's language documentation says that this kind musical notation based coinduction is the "old-way" coinduction in Agda. It recommends the use of coinductive records and copatterns. I've looked around but I'd not able to find examples of copatterns beyond streams and the delay monad. My question: is it possible to represent resumptions using coinductive records and copatterns?

Answer 1

The way to convince Agda that this terminates is to use sized types. That way you can show that close x is at least as well-defined as x.

First of all, here is a definition of Res based on coinductive records and sized types:

mutual
  record Res (n : ℕ) {sz : Size} : Set where
    coinductive
    field resume : ∀ {sz' : Size< sz} → ResCase n {sz'}
  data ResCase (n : ℕ) {sz : Size} : Set where
    ret : (st : σ n) → ResCase n
    δ   : (r : Res n {sz}) → ResCase n
    _∨_ : (l r : Res n {sz}) → ResCase n
    yield : (s : Stmt n) (st : σ n) → ResCase n
open Res

Then you can prove that evalSeq and friends preserve size:

evalStmt : ∀ {n sz} → (Stmt n → Stmt n → Stmt n) → Stmt n → Res n {sz} → Res n {sz}
resume (evalStmt _⊗_ s res) with resume res
resume (evalStmt _⊗_ s _) | ret st = yield s st
resume (evalStmt _⊗_ s _) | δ x = δ (evalStmt _⊗_ s x)
resume (evalStmt _⊗_ s _) | l ∨ r = evalStmt _⊗_ s l ∨ evalStmt _⊗_ s r
resume (evalStmt _⊗_ s _) | yield s' st = yield (s ⊗ s') st

evalSeq : ∀ {n sz} → Stmt n → Res n {sz} → Res n {sz}
evalSeq = evalStmt (\s s' → s ▷ s')

evalParL : ∀ {n sz} → Stmt n → Res n {sz} → Res n {sz}
evalParL = evalStmt (\s s' → s ∥ s')

evalParR : ∀ {n sz} → Stmt n → Res n {sz} → Res n {sz}
evalParR = evalStmt (\s s' → s' ∥ s)

And similarly for close:

mutual
  close : ∀ {n sz} → Res n {sz} → Res n {sz}
  resume (close res) with resume res
  ... | ret st = ret st
  ... | δ r = δ (close r)
  ... | l ∨ r = close l ∨ close r
  ... | yield s st = δ (eval s st)

And eval is as well-defined up to any size:

  eval : ∀ {n sz} → Stmt n → σ n → Res n {sz}
  resume (eval skip st) = ret st
  resume (eval (x ≔ e) st) = ret (st [ x ]≔ ⟦ e , st ⟧ )
  resume (eval (s ▷ s') st) = resume (evalSeq s (eval s' st))
  resume (eval (iif e then s else s') st) with ⟦ e , st ⟧
  ...| zero = yield s' st
  ...| suc n = yield s st
  resume (eval (while e do s) st) with ⟦ e , st ⟧
  ...| zero = ret st
  ...| suc n = yield (s ▷ while e do s) st
  resume (eval (s ∥ s') st) = evalParR s' (eval s st) ∨ evalParL s (eval s' st)
  resume (eval (atomic s) st) = resume (close (eval s st)) -- or δ
  resume (eval (await e do s) st) = {!!}