Agda के Coinduction को समझने में समस्या

Question

मैं निम्नलिखित paper की धारा 4 में प्रस्तुत समानांतर प्रीपेप्टिव शेड्यूलिंग के साथ आईएमपी भाषा के लिए एक कार्यात्मक अर्थशास्त्र को कोड करने का प्रयास कर रहा हूं।

मैं एग्डा 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 

के अनुक्रमिक और समानांतर निष्पादन अब तक परिभाषित करते हैं, तो अच्छा। इसके बाद, मुझे एक रिजम्प्शन में बंद करने के लिए एक ऑपरेशन के साथ पारस्परिक रूप से स्टेटमेंट मूल्यांकन फ़ंक्शन को परिभाषित करने की आवश्यकता है (निलंबित कंप्यूटेशंस निष्पादित करें)।

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 की समग्रता चेकर की शिकायत जब मैं δ (♯ close (eval s st)) कह रही है कि समाप्ति की जाँच के साथ atomic निर्माता के लिए eval समीकरण में छेद को भरने के लिए कोशिश दोनों eval और close समारोह में कई बिंदुओं के लिए विफल रहता है।

इस समस्या के बारे में मेरे सवाल कर रहे हैं:

1) क्यों AGDA समाप्ति इन परिभाषाओं के बारे में शिकायत जाँच कर रहा है? मुझे लगता है कि δ (♯ close (eval s st)) पर कॉल ठीक है क्योंकि यह संरचनात्मक रूप से छोटे कथन पर किया गया है।

2) Current Agda's language documentation कहता है कि इस प्रकार की संगीत नोटेशन आधारित सिंडक्शन एग्डा में "पुरानी-रास्ता" संयम है। यह संवेदनात्मक रिकॉर्ड और copatterns के उपयोग की सिफारिश करता है। मैंने चारों ओर देखा है लेकिन मैं धाराओं और देरी monad से परे copatterns के उदाहरण नहीं मिल पाएगा। मेरा सवाल: क्या सहकारी रिकॉर्ड और copatterns का उपयोग कर बहाली का प्रतिनिधित्व करना संभव है?

Answer 1

आगाडा को मनाने का तरीका यह है कि यह समाप्ति आकार के प्रकारों का उपयोग करना है। इस तरह आप दिखा सकते हैं कि close x कम से कम x के रूप में परिभाषित किया गया है।

सबसे पहले, यहाँ Res की एक परिभाषा coinductive रिकॉर्ड और आकार प्रकार के आधार पर है:

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 

तो फिर तुम साबित कर सकते हैं कि evalSeq और दोस्तों के आकार को बनाए रखने:

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) 

और इसी के लिए 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 : ∀ {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) = {!!}