Update 'evaluator for Dawn in Coq' article to new math delimiters
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
5eb0d1548c
commit
68d9cf1274
|
@ -52,7 +52,7 @@ I replaced instances of `projT1` with instances of `value_to_expr`.
|
||||||
At the end of my previous article, we ended up with a Coq encoding of the big-step
|
At the end of my previous article, we ended up with a Coq encoding of the big-step
|
||||||
[operational semantics](https://en.wikipedia.org/wiki/Operational_semantics)
|
[operational semantics](https://en.wikipedia.org/wiki/Operational_semantics)
|
||||||
of UCC, as well as some proofs of correctness about the derived forms from
|
of UCC, as well as some proofs of correctness about the derived forms from
|
||||||
the article (like \\(\\text{quote}_3\\) and \\(\\text{rotate}_3\\)). The trouble
|
the article (like \(\text{quote}_3\) and \(\text{rotate}_3\)). The trouble
|
||||||
is, despite having our operational semantics, we can't make our Coq
|
is, despite having our operational semantics, we can't make our Coq
|
||||||
code run anything. This is for several reasons:
|
code run anything. This is for several reasons:
|
||||||
|
|
||||||
|
@ -97,10 +97,10 @@ We can now write a function that tries to execute a single step given an express
|
||||||
{{< codelines "Coq" "dawn/DawnEval.v" 11 27 >}}
|
{{< codelines "Coq" "dawn/DawnEval.v" 11 27 >}}
|
||||||
|
|
||||||
Most intrinsics, by themselves, complete after just one step. For instance, a program
|
Most intrinsics, by themselves, complete after just one step. For instance, a program
|
||||||
consisting solely of \\(\\text{swap}\\) will either fail (if the stack doesn't have enough
|
consisting solely of \(\text{swap}\) will either fail (if the stack doesn't have enough
|
||||||
values), or it will swap the top two values and be done. We list only "correct" cases,
|
values), or it will swap the top two values and be done. We list only "correct" cases,
|
||||||
and resort to a "catch-all" case on line 26 that returns an error. The one multi-step
|
and resort to a "catch-all" case on line 26 that returns an error. The one multi-step
|
||||||
intrinsic is \\(\\text{apply}\\), which can evaluate an arbitrary expression from the stack.
|
intrinsic is \(\text{apply}\), which can evaluate an arbitrary expression from the stack.
|
||||||
In this case, the "one step" consists of popping the quoted value from the stack; the
|
In this case, the "one step" consists of popping the quoted value from the stack; the
|
||||||
"remaining program" is precisely the expression that was popped.
|
"remaining program" is precisely the expression that was popped.
|
||||||
|
|
||||||
|
@ -109,10 +109,10 @@ expression on the stack). The really interesting case is composition. Expression
|
||||||
are evaluated left-to-right, so we first determine what kind of step the left expression (`e1`)
|
are evaluated left-to-right, so we first determine what kind of step the left expression (`e1`)
|
||||||
can take. We may need more than one step to finish up with `e1`, so there's a good chance it
|
can take. We may need more than one step to finish up with `e1`, so there's a good chance it
|
||||||
returns a "rest program" `e1'` and a stack `vs'`. If this happens, to complete evaluation of
|
returns a "rest program" `e1'` and a stack `vs'`. If this happens, to complete evaluation of
|
||||||
\\(e_1\\ e_2\\), we need to first finish evaluating \\(e_1'\\), and then evaluate \\(e_2\\).
|
\(e_1\ e_2\), we need to first finish evaluating \(e_1'\), and then evaluate \(e_2\).
|
||||||
Thus, the "rest of the program" is \\(e_1'\\ e_2\\), or `e_comp e1' e2`. On the other hand,
|
Thus, the "rest of the program" is \(e_1'\ e_2\), or `e_comp e1' e2`. On the other hand,
|
||||||
if `e1` finished evaluating, we still need to evaluate `e2`, so our "rest of the program"
|
if `e1` finished evaluating, we still need to evaluate `e2`, so our "rest of the program"
|
||||||
is \\(e_2\\), or `e2`. If evaluating `e1` led to an error, then so did evaluating `e_comp e1 e2`,
|
is \(e_2\), or `e2`. If evaluating `e1` led to an error, then so did evaluating `e_comp e1 e2`,
|
||||||
and we return `err`.
|
and we return `err`.
|
||||||
|
|
||||||
### Extracting Code
|
### Extracting Code
|
||||||
|
@ -280,9 +280,9 @@ 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
|
This is the type of sequences (or chains) of steps corresponding to the
|
||||||
evaluation of the program \\(\\text{true}\\ \\text{false}\\ \\text{or}\\),
|
evaluation of the program \(\text{true}\ \text{false}\ \text{or}\),
|
||||||
starting in an empty stack and evaluating to a stack with only
|
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
|
\(\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:
|
final stack `vs'`, in _some unknown number of steps_, it's sufficient to write:
|
||||||
|
|
||||||
```Coq
|
```Coq
|
||||||
|
@ -366,9 +366,9 @@ data types, `Sem_expr` and `Sem_int`, each of which contains the other.
|
||||||
Regular proofs by induction, which work on only one of the data types,
|
Regular proofs by induction, which work on only one of the data types,
|
||||||
break down because we can't make claims "by induction" about the _other_
|
break down because we can't make claims "by induction" about the _other_
|
||||||
type. For example, while going by induction on `Sem_expr`, we run into
|
type. For example, while going by induction on `Sem_expr`, we run into
|
||||||
issues in the `e_int` case while handling \\(\\text{apply}\\). We know
|
issues in the `e_int` case while handling \(\text{apply}\). We know
|
||||||
a single step -- popping the value being run from the stack. But what then?
|
a single step -- popping the value being run from the stack. But what then?
|
||||||
The rule for \\(\\text{apply}\\) in `Sem_int` contains another `Sem_expr`
|
The rule for \(\text{apply}\) in `Sem_int` contains another `Sem_expr`
|
||||||
which confirms that the quoted value properly evaluates. But this other
|
which confirms that the quoted value properly evaluates. But this other
|
||||||
`Sem_expr` isn't directly a child of the "bigger" `Sem_expr`, and so we
|
`Sem_expr` isn't directly a child of the "bigger" `Sem_expr`, and so we
|
||||||
don't get an inductive hypothesis about it. We know nothing about it; we're stuck.
|
don't get an inductive hypothesis about it. We know nothing about it; we're stuck.
|
||||||
|
@ -399,7 +399,7 @@ ways an intrinsic can be evaluated. Most intrinsics are quite boring;
|
||||||
in our evaluator, they only need a single step, and their semantics
|
in our evaluator, they only need a single step, and their semantics
|
||||||
rules guarantee that the stack has the exact kind of data that the evaluator
|
rules guarantee that the stack has the exact kind of data that the evaluator
|
||||||
expects. We dismiss such cases with `apply chain_final; auto`. The only
|
expects. We dismiss such cases with `apply chain_final; auto`. The only
|
||||||
time this doesn't work is when we encounter the \\(\\text{apply}\\) intrinsic;
|
time this doesn't work is when we encounter the \(\text{apply}\) intrinsic;
|
||||||
in that case, however, we can simply use the first theorem we proved.
|
in that case, however, we can simply use the first theorem we proved.
|
||||||
|
|
||||||
#### A Quick Aside: Automation Using `Ltac2`
|
#### A Quick Aside: Automation Using `Ltac2`
|
||||||
|
@ -498,7 +498,7 @@ is used to run code for each one of these goals. In the non-empty list case, we
|
||||||
apart its tail as necessary by recursively calling `destruct_n`.
|
apart its tail as necessary by recursively calling `destruct_n`.
|
||||||
|
|
||||||
That's pretty much it! We can now use our tactic from Coq like any other. Rewriting
|
That's pretty much it! We can now use our tactic from Coq like any other. Rewriting
|
||||||
our earlier proof about \\(\\text{swap}\\), we now only need to handle the valid case:
|
our earlier proof about \(\text{swap}\), we now only need to handle the valid case:
|
||||||
|
|
||||||
{{< codelines "Coq" "dawn/DawnEval.v" 248 254 >}}
|
{{< codelines "Coq" "dawn/DawnEval.v" 248 254 >}}
|
||||||
|
|
||||||
|
@ -625,8 +625,8 @@ We now have a verified UCC evaluator in Haskell. What next?
|
||||||
as syntax sugar in our parser. Using a variable would be the same as simply
|
as syntax sugar in our parser. Using a variable would be the same as simply
|
||||||
pasting in the variable's definition. This is pretty much what the Dawn article
|
pasting in the variable's definition. This is pretty much what the Dawn article
|
||||||
seems to be doing.
|
seems to be doing.
|
||||||
3. We could prove more things. Can we confirm, once and for all, the correctness of \\(\\text{quote}_n\\),
|
3. We could prove more things. Can we confirm, once and for all, the correctness of \(\text{quote}_n\),
|
||||||
for _any_ \\(n\\)? Is there is a generalized way of converting inductive data types into a UCC encoding?
|
for _any_ \(n\)? Is there is a generalized way of converting inductive data types into a UCC encoding?
|
||||||
Or could we perhaps formally verify the following comment from Lobsters:
|
Or could we perhaps formally verify the following comment from Lobsters:
|
||||||
|
|
||||||
> with the encoding of natural numbers given, n+1 contains the definition of n duplicated two times.
|
> with the encoding of natural numbers given, n+1 contains the definition of n duplicated two times.
|
||||||
|
|
Loading…
Reference in New Issue
Block a user