无法理解Agda的Coinduction

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)目前Agda的语言文档说,这种基于音乐符号的coinduction是Agda中的"老式"coinduction.它建议使用coinductive记录和copatterns.我环顾四周,但我无法找到除了溪流和延迟monad之外的copatterns的例子.我的问题:是否有可能使用共同记录和copatterns来表示恢复？

Answer 1

说服 Agda 终止的方法是使用大小类型。这样您就可以证明close x至少与 一样定义明确x。

\n\n

首先，这是Res基于共归纳记录和大小类型的定义：

\n\n

mutual\n  record Res (n : \xe2\x84\x95) {sz : Size} : Set where\n    coinductive\n    field resume : \xe2\x88\x80 {sz' : Size< sz} \xe2\x86\x92 ResCase n {sz'}\n  data ResCase (n : \xe2\x84\x95) {sz : Size} : Set where\n    ret : (st : \xcf\x83 n) \xe2\x86\x92 ResCase n\n    \xce\xb4   : (r : Res n {sz}) \xe2\x86\x92 ResCase n\n    _\xe2\x88\xa8_ : (l r : Res n {sz}) \xe2\x86\x92 ResCase n\n    yield : (s : Stmt n) (st : \xcf\x83 n) \xe2\x86\x92 ResCase n\nopen Res\n

\n\n

然后你可以证明这一点evalSeq并且朋友们可以保留大小：

\n\n

evalStmt : \xe2\x88\x80 {n sz} \xe2\x86\x92 (Stmt n \xe2\x86\x92 Stmt n \xe2\x86\x92 Stmt n) \xe2\x86\x92 Stmt n \xe2\x86\x92 Res n {sz} \xe2\x86\x92 Res n {sz}\nresume (evalStmt _\xe2\x8a\x97_ s res) with resume res\nresume (evalStmt _\xe2\x8a\x97_ s _) | ret st = yield s st\nresume (evalStmt _\xe2\x8a\x97_ s _) | \xce\xb4 x = \xce\xb4 (evalStmt _\xe2\x8a\x97_ s x)\nresume (evalStmt _\xe2\x8a\x97_ s _) | l \xe2\x88\xa8 r = evalStmt _\xe2\x8a\x97_ s l \xe2\x88\xa8 evalStmt _\xe2\x8a\x97_ s r\nresume (evalStmt _\xe2\x8a\x97_ s _) | yield s' st = yield (s \xe2\x8a\x97 s') st\n\nevalSeq : \xe2\x88\x80 {n sz} \xe2\x86\x92 Stmt n \xe2\x86\x92 Res n {sz} \xe2\x86\x92 Res n {sz}\nevalSeq = evalStmt (\\s s' \xe2\x86\x92 s \xe2\x96\xb7 s')\n\nevalParL : \xe2\x88\x80 {n sz} \xe2\x86\x92 Stmt n \xe2\x86\x92 Res n {sz} \xe2\x86\x92 Res n {sz}\nevalParL = evalStmt (\\s s' \xe2\x86\x92 s \xe2\x88\xa5 s')\n\nevalParR : \xe2\x88\x80 {n sz} \xe2\x86\x92 Stmt n \xe2\x86\x92 Res n {sz} \xe2\x86\x92 Res n {sz}\nevalParR = evalStmt (\\s s' \xe2\x86\x92 s' \xe2\x88\xa5 s)\n

\n\n

类似地close：

\n\n

mutual\n  close : \xe2\x88\x80 {n sz} \xe2\x86\x92 Res n {sz} \xe2\x86\x92 Res n {sz}\n  resume (close res) with resume res\n  ... | ret st = ret st\n  ... | \xce\xb4 r = \xce\xb4 (close r)\n  ... | l \xe2\x88\xa8 r = close l \xe2\x88\xa8 close r\n  ... | yield s st = \xce\xb4 (eval s st)\n

\n\n

并且eval对于任何大小都有明确的定义：

\n\n

  eval : \xe2\x88\x80 {n sz} \xe2\x86\x92 Stmt n \xe2\x86\x92 \xcf\x83 n \xe2\x86\x92 Res n {sz}\n  resume (eval skip st) = ret st\n  resume (eval (x \xe2\x89\x94 e) st) = ret (st [ x ]\xe2\x89\x94 \xe2\x9f\xa6 e , st \xe2\x9f\xa7 )\n  resume (eval (s \xe2\x96\xb7 s') st) = resume (evalSeq s (eval s' st))\n  resume (eval (iif e then s else s') st) with \xe2\x9f\xa6 e , st \xe2\x9f\xa7\n  ...| zero = yield s' st\n  ...| suc n = yield s st\n  resume (eval (while e do s) st) with \xe2\x9f\xa6 e , st \xe2\x9f\xa7\n  ...| zero = ret st\n  ...| suc n = yield (s \xe2\x96\xb7 while e do s) st\n  resume (eval (s \xe2\x88\xa5 s') st) = evalParR s' (eval s st) \xe2\x88\xa8 evalParL s (eval s' st)\n  resume (eval (atomic s) st) = resume (close (eval s st)) -- or \xce\xb4\n  resume (eval (await e do s) st) = {!!}\n

\n