Трудно понять коиндукцию Агды

Question

Я пытаюсь кодировать функциональную семантику для языка IMP с параллельным упреждающим планированием, как представлено в разделе 4 следующей статьи.

Я использую Agda 2.5.2 и стандартную библиотеку 0.13. Кроме того, весь код доступен в следующем разделе.

Прежде всего, я определил синтаксис рассматриваемого языка как индуктивные типы.

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

Проверка целостности Агды жалуется, когда я пытаюсь заполнить дыру в eval уравнение для atomic конструктор с δ (♯ close (eval s st)) говоря, что проверка завершения не удается для нескольких точек в обоих eval а также close функция.

Мои вопросы по этой проблеме:

1) Почему проверка завершения Agda жалуется на эти определения? Мне кажется, что вызов δ (♯ close (eval s st)) хорошо, так как это сделано на структурно меньшем утверждении.

2) В текущей языковой документации Агды говорится, что подобная музыкальная нотация, основанная на коиндукции, является "старой" коиндукцией в Агде. Он рекомендует использовать коиндуктивные записи и копаттерны. Я осмотрелся вокруг, но я не смог найти примеров copatterns за пределами потоков и монады задержки. Мой вопрос: возможно ли представить резюме с использованием коиндуктивных записей и копаттернов?

Answer 1

Способ убедить Agda в том, что это заканчивается, - использовать размерные типы. Таким образом, вы можете показать, что close x по крайней мере так же четко, как x,

Прежде всего, вот определение Res на основе коиндуктивных записей и типоразмеров:

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 так же хорошо определен до любого размера:

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