Problem zu verstehen, Agda Coinduction

Question

Ich versuche, eine funktionale Semantik für IMP Sprache mit parallelen präventiven Planung wie in Abschnitt 4 der folgenden paper vorgestellt.

Ich benutze Agda 2.5.2 und Standard-Bibliothek 0.13. Der gesamte Code ist auch unter folgender Nummer verfügbar: gist.

Zuerst habe ich die Syntax der betreffenden Sprache als induktive Typen definiert.

Der Zustand ist nur ein Vektor der natürlichen Zahlen und Ausdruck Semantik ist einfach.

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

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

Dann habe ich die Art der Wiederaufnahmen definiert, die eine Art von verzögerten Berechnungen sind.

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 

Als nächstes folgt 1 definiere ich sequentielle und parallele Ausführung von Anweisungen

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 weit, so gut. Als nächstes muss ich die Anweisungsbewertungsfunktion wechselseitig definieren mit einer Operation zum Schließen (Ausführen von suspendierten Berechnungen) in einer Wiederaufnahme.

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 der Gesamtheit checker beschwert, wenn ich versuche für atomic Konstruktor das Loch in eval Gleichung zu füllen mit δ (♯ close (eval s st)) sagen, dass die Abschlussprüfung für mehrere Punkte nicht in beiden eval und close Funktion.

Meine Fragen zu diesem Problem sind:

1) Warum ist Agda Kündigung über diese Definitionen Überprüfung beschweren? Es scheint mir, dass der Anruf δ (♯ close (eval s st)) in Ordnung ist, da es auf eine strukturell kleinere Aussage gemacht wird.

2) Current Agda's language documentation sagt, dass diese Art Musiknotation basierte Coinduction ist die "alten Weg" Coinduction in Agda. Es empfiehlt die Verwendung von coinductive records und copatterns. Ich habe mich umgesehen, aber ich konnte keine Beispiele für Copatterns jenseits von Streams und der Verzögerungs-Monade finden. Meine Frage: Ist es möglich, Wiederaufnahmen mit Koinduktiven Akten und Copattern darzustellen?

Answer 1

Der Weg, Agda zu überzeugen, dass dies endet, ist die Verwendung von Größen. Auf diese Weise können Sie zeigen, dass close x mindestens so gut definiert ist wie x.

Zunächst einmal ist hier eine Definition von Res basierend auf coinductive Aufzeichnungen und Größe Typen:

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 

Dann können Sie beweisen, dass evalSeq und Freunde Größe erhalten:

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) 

Und in ähnlicher Weise für 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) 

Und eval als gut definiert bis zu jeder Größe:

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