From 68d9cf1274067725e5ec864b689fefc49f7daaa6 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 13 May 2024 18:57:15 -0700 Subject: [PATCH] Update 'evaluator for Dawn in Coq' article to new math delimiters Signed-off-by: Danila Fedorin --- content/blog/coq_dawn_eval/index.md | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/content/blog/coq_dawn_eval/index.md b/content/blog/coq_dawn_eval/index.md index 5e7a32e..678af28 100644 --- a/content/blog/coq_dawn_eval/index.md +++ b/content/blog/coq_dawn_eval/index.md @@ -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 [operational semantics](https://en.wikipedia.org/wiki/Operational_semantics) 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 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 >}} 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, 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 "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`) 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 -\\(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, +\(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, 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`. ### 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 -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 -\\(\\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: ```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, 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 -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? -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 `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. @@ -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 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 -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. #### 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`. 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 >}} @@ -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 pasting in the variable's definition. This is pretty much what the Dawn article seems to be doing. -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? +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? 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.