Problemy z rozumieniem Coinduction Agdy

Question

Próbuję kodować semantykę funkcjonalną dla języka IMP z równoległym planowaniem zapobiegawczym, jak przedstawiono w sekcji 4 poniższej paper.

Używam Agdy 2.5.2 i biblioteki standardowej 0.13. Cały kod jest dostępny pod następującym numerem: gist.

Po pierwsze, zdefiniowałem składnię danego języka jako typy indukcyjne.

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 

Stan jest po prostu wektorem liczb naturalnych, a semantyka wypowiedzi jest prosta.

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

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

Następnie zdefiniowałem rodzaj wznowienia, który jest pewnego rodzaju opóźnionymi obliczeniami.

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 

Następnie po 1, zdefiniować sekwencyjnego i równoległego wykonywania sprawozdań

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 

Tak daleko, tak dobrze. Następnie potrzebuję zdefiniować funkcję oceny oświadczenia, aby operacja zamknięcia (wykonać zawieszone obliczenia) wznowiła.

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 za całość sprawdzania narzeka gdy próbuję wypełnić dziurę w eval równania dla atomic konstruktora z δ (♯ close (eval s st)) mówiąc, że sprawdzanie terminacji nie dla kilku punktów w obu eval i close funkcji.

Moje pytania dotyczące tego problemu są:

1) Dlaczego zakończenie Agda sprawdzanie narzeka tych definicji? Wydaje mi się, że wywołanie δ (♯ close (eval s st)) jest w porządku, ponieważ jest wykonywane na strukturalnie mniejszej instrukcji.

2) Current Agda's language documentation mówi, że ten rodzaj muzycznego zapisu opartego na notacji jest "starą" koindukcją w Agdzie. Zaleca stosowanie nagrań i protokołów o charakterze pomocniczym. Rozejrzałem się wokół, ale nie znalazłem przykładów copatternów poza strumieniami i monadą opóźnienia. Moje pytanie: czy można reprezentować wznowienia za pomocą rekordów i copywaterów?

Answer 1

Sposobem przekonania Agdy, że to się kończy, jest użycie typów o różnych rozmiarach. W ten sposób możesz pokazać, że close x jest co najmniej tak dobrze zdefiniowany, jak x.

Przede wszystkim o to definicja Res podstawie coinductive ewidencji i wielkości typy:

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 

Następnie można udowodnić, że evalSeq i przyjaciele zachować rozmiar:

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) 

i podobnie dla 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) 

A eval jest tak dobrze zdefiniowane do dowolnej wielkości:

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