Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Make some more progress on the UCC evaluator article

Browse Source
This commit is contained in:
Danila Fedorin 2021-11-28 01:48:01 -08:00
parent 6c1940f5d2
commit 4d24e7095b
1 changed files with 54 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

57
content/blog/coq_dawn_eval.md
View File

@ -265,10 +265,61 @@ eval_chain nil (e_comp (e_comp true false) or) (true :: nil)
This is the type of sequences (or chains) of steps corresponding to the
evaluation of the program \\(\\text{true}\\ \\text{false}\\ \\text{or}\\),
starting in an empty stack and evaluating to a stack with only true on top.
Thus to say that an expression evaluates to some final stack `vs'`, in
_some unknown number of steps_, it's sufficient to write:
starting in an empty stack and evaluating to a stack with only
\\(\\text{true}\\) on top. Thus to say that an expression evaluates to some
final stack `vs'`, in _some unknown number of steps_, it's sufficient to write:
```Coq
eval_chain vs e vs'
```
Evaluation chains have a couple of interesting properties. First and foremost,
they can be "concatenated". This is analagous to the `Sem_e_comp` rule
in our original semantics: if an expression `e1` starts in stack `vs`
and finishes in stack `vs'`, and another expression starts in stack `vs'`
and finishes in stack `vs''`, then we can compose these two expressions,
and the result will start in `vs` and finish in `vs''`.
{{< codelines "Coq" "dawn/DawnEval.v" 69 75 >}}
The proof is very short. We go
{{< sidenote "right" "concat-note" "by induction on the left evaluation" >}}
It's not a coincidence that defining something like <code>(++)</code>
(list concatenation) in Haskell typically starts by pattern matching
on the <em>left</em> list. In fact, proofs by <code>induction</code>
actually correspond to recursive functions! It's tough putting code blocks
in sidenotes, but if you're playing with the
<a href="https://dev.danilafe.com/Web-Projects/blog-static/src/branch/master/code/dawn/DawnEval.v"><code>DawnEval.v</code></a> file, try running
<code>Print eval_chain_ind</code>, and note the presence of <code>fix</code>,
the <a href="https://en.wikipedia.org/wiki/Fixed-point_combinator">fixed point
combinator</a> used to implement recursion.
{{< /sidenote >}}
chain (the one for `e1`). Coq takes care of most of the rest with `auto`.
The key to this proof is that whatever `P` is cotained within a "node"
in the left chain determines how `eval_step (e_comp e1 e2)` behaves. Whether
`e1` evaluates to `final` or `middle`, the composition evaluates to `middle`
(a composition of two expressions cannot be done in one step), so we always
{{< sidenote "left" "cons-note" "create a new \"cons\" node." >}}
This is <em>unlike</em> list concatenation, since we typically don't
create new nodes when appending to an empty list.
{{< /sidenote >}} via `chain_middle`. Then, the two cases are as follows:
* If the step was `final`, then
the rest of the steps use only `e2`, and good news, we already have a chain
for that!
* Otherwise, the step was `middle`, an we stll have a chain for some
intermediate program `ei` that starts in some stack `vsi` and ends in `vs'`.
By induction, we know that _this_ chain can be concatenated with the one
for `e2`, resulting in a chain for `e_comp ei e2`. All that remains is to
attach to this sub-chain the one step from `(vs, e1)` to `(vsi, ei)`, which
is handled by `chain_middle`.
{{< todo >}}A drawing would be nice here!{{< /todo >}}
The `merge` operation is reversible; chains can be split into two pieces,
one for each composed expression:
{{< codelines "Coq" "dawn/DawnEval.v" 77 78 >}}
While interesting, this particular fact isn't used anywhere else in this
post, and I will omit the proof here.