# 「SF-LC」14 ImpCEvalFun

## Logical Foundations - An Evaluation Function For Imp

Posted by Hux on January 14, 2019

## Step-Indexed Evaluator

…Copied from 12-imp.md:

Chapter ImpCEvalFun provide some workarounds to make functional evalution works:

1. step-indexed evaluator, i.e. limit the recursion depth. (think about Depth-Limited Search).
2. return option to tell if it’s a normal or abnormal termination.
3. use LETOPT...IN... to reduce the “optional unwrapping” (basicaly Monadic binding >>=!) this approach of let-binding became so popular in ML family.
 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 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

### ->

 1 2 3 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:

• destruct for the i.
• induction i, generalize on all st st' c.
1. i = 0 case contradiction
2. i = S i' case; destruct c.
• destruct (ceval_step ...) for the option