Add illustrations about evaluation chains

This commit is contained in:
Danila Fedorin 2021-12-02 17:41:36 -08:00
parent 1c93d28441
commit b8f9f93537
8 changed files with 31 additions and 12 deletions

Binary file not shown.

After

Width:  |  Height:  |  Size: 114 KiB

Binary file not shown.

After

Width:  |  Height:  |  Size: 190 KiB

Binary file not shown.

After

Width:  |  Height:  |  Size: 132 KiB

Binary file not shown.

After

Width:  |  Height:  |  Size: 46 KiB

Binary file not shown.

After

Width:  |  Height:  |  Size: 193 KiB

Binary file not shown.

After

Width:  |  Height:  |  Size: 54 KiB

Binary file not shown.

After

Width:  |  Height:  |  Size: 87 KiB

View File

@ -217,6 +217,11 @@ step-by-step to final stack `vs'`"? For one step, we can say:
eval_step vs e = final vs' eval_step vs e = final vs'
``` ```
Here's a picture so you can start visualizing what it looks like. The black line represents
a single "step".
{{< figure src="coq_eval_empty.png" caption="Visual representation of a single-step evaluation." class="small" alt="Two dots connected by a line. One dot is labeled \"vs\", and the other \"vs1\"." >}}
For two steps, we'd have to assert the existence of an intermediate For two steps, we'd have to assert the existence of an intermediate
expression (the "rest of the program" after the first step): expression (the "rest of the program" after the first step):
@ -226,6 +231,10 @@ exists ei vsi,
eval_step vsi ei = final vs' (* Second step to final state. *) eval_step vsi ei = final vs' (* Second step to final state. *)
``` ```
Once again, here's a picture. I've highlighted the intermediate state, `vsi`, in
a brighter color.
{{< figure src="coq_eval_one.png" caption="Visual representation of a two-step evaluation." class="small" alt="Three dots connected by lines. The first dot is labeled \"vs\", the next \"vsi\", and the last \"vs1\". The second dot is highlighted." >}}
For three steps: For three steps:
```Coq ```Coq
@ -235,6 +244,9 @@ exists ei1 ei2 vsi1 vsi2,
eval_step vsi2 ei2 = final vs' (* Second step to final state. *) eval_step vsi2 ei2 = final vs' (* Second step to final state. *)
``` ```
I can imagine that you're getting the idea, but here's one last picture:
{{< figure src="coq_eval_two.png" caption="Visual representation of a three-step evaluation." class="small" alt="Four dots connected by lines. The first dot is labeled \"vs\", the next \"vsi1\", the one after \"vsi2\", and the last \"vs1\". The second and third dots are highlighted." >}}
This is awful! Not only is this a lot of writing, but it also makes various This is awful! Not only is this a lot of writing, but it also makes various
sequences of steps have a different "shape". This way, we can't make sequences of steps have a different "shape". This way, we can't make
proofs about evaluations of an _arbitrary_ number of steps. Not all is lost, though: if we squint proofs about evaluations of an _arbitrary_ number of steps. Not all is lost, though: if we squint
@ -251,7 +263,11 @@ If you squint at this, it kind of looks like a list! The "empty"
part of a list is the final step, while the "cons" part is a middle step. The part of a list is the final step, while the "cons" part is a middle step. The
analogy holds up for another reason: an "empty" sequence has zero intermediate analogy holds up for another reason: an "empty" sequence has zero intermediate
expressions, while each "cons" introduces a single new intermediate expressions, while each "cons" introduces a single new intermediate
program. Perhaps we can define a new data type that matches this? Indeed program.
{{< figure src="coq_eval_lists.png" caption="Evaluation sequences as lists." class="large" alt="The three previous figures are drawn together, each next to its list representation." >}}
Perhaps we can define a new data type that matches this? Indeed
we can! we can!
{{< codelines "Coq" "dawn/DawnEval.v" 64 67 >}} {{< codelines "Coq" "dawn/DawnEval.v" 64 67 >}}
@ -283,6 +299,8 @@ and the result will start in `vs` and finish in `vs''`.
{{< codelines "Coq" "dawn/DawnEval.v" 69 75 >}} {{< codelines "Coq" "dawn/DawnEval.v" 69 75 >}}
{{< figure src="coq_eval_chain_merge.png" caption="Merging evaluation chains." class="large" alt="Two evaluation chains, one starting in \"vs\" and ending in \"vs'\", and one starting in \"vs'\" and ending in \"vs''\", are combined into one. The new chain starts in \"vs\", ends in \"vs''\", and has \"vs'\" in the middle. " >}}
The proof is very short. We go The proof is very short. We go
{{< sidenote "right" "concat-note" "by induction on the left evaluation chain" >}} {{< sidenote "right" "concat-note" "by induction on the left evaluation chain" >}}
It's not a coincidence that defining something like <code>(++)</code> It's not a coincidence that defining something like <code>(++)</code>
@ -303,19 +321,20 @@ in the left chain determines how `eval_step (e_comp e1 e2)` behaves. Whether
{{< sidenote "left" "cons-note" "create a new \"cons\" node." >}} {{< sidenote "left" "cons-note" "create a new \"cons\" node." >}}
This is <em>unlike</em> list concatenation, since we typically don't This is <em>unlike</em> list concatenation, since we typically don't
create new nodes when appending to an empty list. create new nodes when appending to an empty list.
{{< /sidenote >}} via `chain_middle`. Then, the two cases are as follows: {{< /sidenote >}} via `chain_middle`. Then, the two cases are as follows.
* If the step was `final`, then If the step was `final`, then
the rest of the steps use only `e2`, and good news, we already have a chain the rest of the steps use only `e2`, and good news, we already have a chain
for that! for that!
* Otherwise, the step was `middle`, an we still have a chain for some {{< figure src="coq_eval_chain_base.png" caption="Merging evaluation chains when the first chain only has one step." class="large" alt="A single-step chain connected to another by a line labeled \"chain_middle\"." >}}
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 >}} Otherwise, the step was `middle`, an we still 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`.
{{< figure src="coq_eval_chain_inductive.png" caption="Merging evaluation chains when the first chain has a middle step and others." class="large" alt="Visualization of the inductive case of merging chains." >}}
The `merge` operation is reversible; chains can be split into two pieces, The `merge` operation is reversible; chains can be split into two pieces,
one for each composed expression: one for each composed expression: