「SF-LC」14 ImpCEvalFun
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.本文参与 腾讯云自媒体同步曝光计划，分享自作者个人站点/博客。
原始发表：2021-03-28，如有侵权请联系 cloudcommunity@tencent.com 删除
评论
登录后参与评论
推荐阅读
目录
腾讯云开发者
