Agdaのコイン導出を理解するのに苦労します

Question

私は、次のセクション4に示すように、並列プリエンプティブスケジューリングを使用してIMP言語の機能セマンティクスをコーディングしようとしています。paper。

私はAgda 2.5.2と標準ライブラリ0.13を使用しています。また、コード全体は、gistで利用可能です。

まず、問題の言語の構文を誘導型と定義しました。

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 

状態は単なる自然数のベクトルであり、式の意味は単純です。

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

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

次に、ある種の遅延計算である再開のタイプを定義しました。

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 

次に、1を次のように、私は、これまでのところは良い文

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 

のシーケンシャルおよび並列実行を定義します。次に、文章評価関数を、再開時に閉じる（中断した計算を実行する）操作で相互に定義する必要があります。私はδ (♯ close (eval s st))が終了チェックが両方evalとclose機能にいくつかの点で失敗したと言ってatomicコンストラクタのeval式の穴を埋めるためにしようとすると

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の全体チェッカーが文句を言います。この問題について

私の質問は以下のとおりです。

1）なぜAgdaの終了は、これらの定義について不満をチェックしていますか？構造的に小さい文の上に が実行されているので、δ (♯ close (eval s st))というコールは正常です。

2）Current Agda's language documentationは、この種類の音楽表記をベースにした共誘導はAgdaの「旧式」共導出であると言います。それは のコインシデンスレコードと共用体の使用を推奨しています。私は周りを見回しましたが、ストリームと遅延モナド以外のパターンの例は見つけられませんでした。私の質問：コインシデンス・レコードとコパタンを使って再開を表現することは可能でしょうか？

Answer 1

これが終了するとAgdaに伝える方法は、サイズの異なる型を使用することです。そうすれば、close xは少なくともxとして定義されていることがわかります。

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) 

と同様のために：あなたはevalSeqや友人のサイズを維持することを証明することができます次に

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 

：すべての

まず、ここcoinductive記録やサイズの種類に基づいてResの定義です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) 

そしてevalは、任意のサイズまで明確に定義されている：

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