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?
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) = {!!}