Problème de compréhension de la Coinduction d'Agda

Question

J'essaie de coder une sémantique fonctionnelle pour le langage IMP avec une planification préemptive parallèle comme présenté dans la section 4 du paper suivant. J'utilise Agda 2.5.2 et la bibliothèque standard 0.13. En outre, le code entier est disponible à l'adresse suivante gist. En premier lieu, j'ai défini la syntaxe du langage en question comme des types inductifs. L'état est juste un vecteur de nombres naturels et la sémantique d'expression est directe. Ensuite, j'ai défini le type de reprises, qui sont une sorte de calculs retardé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 

Ensuite, suivant 1, je définir l'exécution séquentielle et parallèle des états

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 

Jusqu'à présent, si bon. Ensuite, j'ai besoin de définir la fonction d'évaluation d'une instruction avec une opération de fermeture (exécution de calculs suspendus) dans une reprise.

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

le vérificateur de la totalité de Agda se plaint lorsque je tente de combler le trou dans eval équation pour atomic constructeur avec δ (♯ close (eval s st)) en disant que la vérification de terminaison échoue pour plusieurs points dans les deux fonctions eval et close.

Mes questions sur ce problème sont:

1) Pourquoi la fin Agda vérifier se plaindre de ces définitions? Il me semble que l'appel δ (♯ close (eval s st)) est bien car il est fait sur une déclaration structurellement plus petit. 2) Current Agda's language documentation 2) Current Agda's language documentation dit que cette sorte de coinduction basée sur la notation musicale est la coinduction "à l'ancienne" dans Agda. Il recommande l'utilisation des enregistrements coindatifs et des copatterns. J'ai regardé autour de moi mais je ne pouvais pas trouver des exemples de personnages au-delà des flux et de la monade de retard. Ma question: est-il possible de représenter des reprises en utilisant des enregistrements coinductifs et des copatterns?

Answer 1

La façon de convaincre Agda que cela se termine est d'utiliser des types de taille. De cette façon, vous pouvez montrer que close x est au moins aussi bien défini que x.

Tout d'abord, voici une définition de Res basée sur les dossiers CoInductive et types de taille:

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 

Ensuite, vous pouvez prouver que evalSeq et les amis conserver la taille:

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) 

Et même pour 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) 

Et eval est aussi bien définie jusqu'à une taille:

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