Step-Indexed Evaluator
…Copied from 12-imp.md:
Chapter
ImpCEvalFunprovide some workarounds to make functional evalution works:
- step-indexed evaluator, i.e. limit the recursion depth. (think about Depth-Limited Search).
- return
optionto tell if it’s a normal or abnormal termination.- use
LETOPT...IN...to reduce the “optional unwrapping” (basicaly Monadic binding>>=!) this approach oflet-bindingbecame so popular in ML family.
Notation "'LETOPT' x <== e1 'IN' e2"
:= (match e1 with
| Some x ⇒ e2
| None ⇒ None
end)
(right associativity, at level 60).
Open Scope imp_scope.
Fixpoint ceval_step (st : state) (c : com) (i : nat)
: option state :=
match i with
| O ⇒ None (* depth-limit hit! *)
| S i' ⇒
match c with
| SKIP ⇒
Some st
| l ::= a1 ⇒
Some (l !-> aeval st a1 ; st)
| c1 ;; c2 ⇒
LETOPT st' <== ceval_step st c1 i' IN (* option bind *)
ceval_step st' c2 i'
| TEST b THEN c1 ELSE c2 FI ⇒
if (beval st b)
then ceval_step st c1 i'
else ceval_step st c2 i'
| WHILE b1 DO c1 END ⇒
if (beval st b1)
then LETOPT st' <== ceval_step st c1 i' IN
ceval_step st' c i'
else Some st
end
end.
Close Scope imp_scope.
Relational vs. Step-Indexed Evaluation
Prove ceval_step is equiv to ceval
->
Theorem ceval_step__ceval: forall c st st',
(exists i, ceval_step st c i = Some st') ->
st =[ c ]=> st'.
The critical part of proof:
destructfor thei.induction i, generalize on allst st' c.i = 0case contradictioni = S i'case;destruct c.destruct (ceval_step ...)for theoptionNonecase contradictionSomecase, use induction hypothesis…
<-
Theorem ceval__ceval_step: forall c st st',
st =[ c ]=> st' ->
exists i, ceval_step st c i = Some st'.
Proof.
intros c st st' Hce.
induction Hce.
What readers say
先看读者反馈，再直接在当前页面继续讨论。公共留言需要 Waline 服务端；配置后访客只填昵称即可发布。
这类长文如果结构清楚，我会一路读到底。这里最好的地方是把概念、公式和代码示例放在同一篇里。
数据库和工程文档的风格很实用，截图、SQL 和说明都能直接拿去复盘项目。
强化学习相关文章密度很高，但排版如果更清楚，回看体验会更好。这个新版方向是对的。
我更喜欢能快速扫到标签、修改时间和文章重点的首页，现在这种卡片视图会比纯列表更容易选读。
代码块只要语言标识和层级做好，技术博客的专业感会立刻上来。
评论区不用社交账号强绑定会更愿意留言，尤其是这种偏学习记录的网站。
Quick Identity
Pick a preset and leave a note
留言方式：先选择一个预设身份，再在下方输入评论。当前若显示“需要配置 Waline”，说明站点还缺少可写评论后端。
当前未选择预设身份