我正在尝试为IMP语言编写功能语义,其中包括并行抢占调度,如以下论文第4节所述。
我正在使用Agda 2.5.2和标准库0.13。此外,整个代码可在以下gist中找到。
首先,我已定义了该语言的语法为归纳类型。
国家状态只是自然数的向量,表达语义很直观。
接下来,按照1所述,我定义了语句的顺序执行和并行执行。
到目前为止,一切都很好。接下来,我需要定义一个语句评估函数,并与恢复中的关闭操作(执行暂停计算)相互关联。
Agda的全面性检查器在我尝试用“δ(♯close(eval s st))”填充“atomic”构造函数的“eval”方程中的洞时发出警告,称终止检查失败于“eval”和“close”函数的多个点。关于这个问题,我的问题是:
1)为什么Agda终止检查会抱怨这些定义?在我看来,调用“δ(♯close(eval s st))”是可以的,因为它是在结构上更小的语句上完成的。
2)Current Agda's language documentation说,基于音乐符号的共归类是Agda中的“旧方式”共归类。它推荐使用共归记录和copatterns。我找了一下,但没有找到除流和延迟单子外的copatterns示例。我的问题是:是否可以使用共归记录和copatterns表示恢复?
我正在使用Agda 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说,基于音乐符号的共归类是Agda中的“旧方式”共归类。它推荐使用共归记录和copatterns。我找了一下,但没有找到除流和延迟单子外的copatterns示例。我的问题是:是否可以使用共归记录和copatterns表示恢复?
δ (♯ close (eval s st))
中调用 eval 时,其参数会逐渐变小。close 还会对结果调用 eval,而其参数大小是未知的。因此,无法使用归纳法证明 eval 的终止性。 - Twan van Laarhoven