Khó hiểu Đồng bộ của Agda

Question

Tôi đang cố gắng viết mã ngữ nghĩa chức năng cho ngôn ngữ IMP với lập lịch dự phòng trước song song như được trình bày trong phần 4 của paper sau đây.

Tôi đang sử dụng Agda 2.5.2 và Thư viện chuẩn 0.13. Ngoài ra, toàn bộ mã có sẵn tại gist sau.

Trước hết, tôi đã xác định cú pháp của ngôn ngữ được đề cập là loại quy nạp.

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 

Trạng thái chỉ là vectơ số tự nhiên và ngữ nghĩa biểu thức đơn giả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 ⟧ 

Sau đó, tôi đã xác định loại tiếp tục, đó là một số loại tính toán chậm trễ.

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 

Tiếp theo, sau 1, tôi xác định thực hiện tuần tự và song song với báo cáo

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 

Cho đến nay, như vậy tốt. Tiếp theo, tôi cần xác định hàm đánh giá câu lệnh cùng với một thao tác để đóng (thực thi các tính toán bị treo) trong một lần nối lại.

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

kiểm tra tổng thể Agda của than phiền khi tôi cố gắng để lấp đầy lỗ trong eval phương trình cho atomic constructor với δ (♯ close (eval s st)) nói rằng kiểm tra chấm dứt không cho một số điểm trong cả hai eval và close chức năng.

Câu hỏi của tôi về vấn đề này như sau:

1) Tại sao Agda chấm dứt kiểm tra phàn nàn về những định nghĩa này? Dường như với tôi rằng cuộc gọi δ (♯ close (eval s st)) là tốt vì nó được thực hiện trên một tuyên bố có cấu trúc nhỏ hơn.

2) Current Agda's language documentation nói rằng ký hiệu dựa trên ký hiệu âm nhạc loại này là đồng nghĩa "cũ" trong Agda. Nó khuyến nghị sử dụng các bản ghi và copatterns đồng bộ. Tôi đã nhìn xung quanh nhưng tôi không thể tìm thấy ví dụ về copatterns ngoài suối và sự chậm trễ đơn nguyên. Câu hỏi của tôi: là nó có thể đại diện cho resumptions bằng cách sử dụng hồ sơ coinductive và copatterns?

Answer 1

Cách thuyết phục Agda rằng điều này chấm dứt là sử dụng các loại có kích thước. Bằng cách đó bạn có thể chỉ ra rằng close x ít nhất cũng được xác định là x.

Trước hết, đây là một định nghĩa của Res dựa trên hồ sơ coinductive và các loại kích thước:

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 

Sau đó, bạn có thể chứng minh rằng evalSeq và bạn bè giữ gìn kích thước:

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) 

Và tương tự cho 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) 

Và eval được cũng xác định lên đến bất kỳ kích thước:

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