From 5eb0d1548c98f04b98b1bd88654f4ab4ab5dc9e1 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 13 May 2024 18:55:59 -0700 Subject: [PATCH] Update dawn-in-coq to new math delimiters Signed-off-by: Danila Fedorin --- content/blog/coq_dawn.md | 94 ++++++++++++++++++++-------------------- 1 file changed, 47 insertions(+), 47 deletions(-) diff --git a/content/blog/coq_dawn.md b/content/blog/coq_dawn.md index 79bd2e8..b168df0 100644 --- a/content/blog/coq_dawn.md +++ b/content/blog/coq_dawn.md @@ -17,13 +17,13 @@ and that's what I reached for when making this attempt. #### Expressions and Intrinsics This is mostly the easy part. A UCC expression is one of three things: -* An "intrinsic", written \\(i\\), which is akin to a built-in function or command. -* A "quote", written \\([e]\\), which takes a UCC expression \\(e\\) and moves it onto the stack (UCC is stack-based). -* A composition of several expressions, written \\(e_1\\ e_2\\ \\ldots\\ e_n\\), which effectively evaluates them in order. +* An "intrinsic", written \(i\), which is akin to a built-in function or command. +* A "quote", written \([e]\), which takes a UCC expression \(e\) and moves it onto the stack (UCC is stack-based). +* A composition of several expressions, written \(e_1\ e_2\ \ldots\ e_n\), which effectively evaluates them in order. This is straightforward to define in Coq, but I'm going to make a little simplifying change. -Instead of making "composition of \\(n\\) expressions" a core language feature, I'll only -allow "composition of \\(e_1\\) and \\(e_2\\)", written \\(e_1\\ e_2\\). This change does not +Instead of making "composition of \(n\) expressions" a core language feature, I'll only +allow "composition of \(e_1\) and \(e_2\)", written \(e_1\ e_2\). This change does not in any way reduce the power of the language; we can still {{< sidenote "right" "assoc-note" "write \(e_1\ e_2\ \ldots\ e_n\) as \((e_1\ e_2)\ \ldots\ e_n\)." >}} The same expression can, of course, be written as \(e_1\ \ldots\ (e_{n-1}\ e_n)\). @@ -42,10 +42,10 @@ of an inductive data type in Coq. {{< codelines "Coq" "dawn/Dawn.v" 12 15 >}} -Why do we need `e_int`? We do because a token like \\(\\text{swap}\\) can be viewed -as belonging to the set of intrinsics \\(i\\), or the set of expressions, \\(e\\). While writing +Why do we need `e_int`? We do because a token like \(\text{swap}\) can be viewed +as belonging to the set of intrinsics \(i\), or the set of expressions, \(e\). While writing down the rules in mathematical notation, what exactly the token means is inferred from context - clearly -\\(\\text{swap}\\ \\text{drop}\\) is an expression built from two other expressions. In statically-typed +\(\text{swap}\ \text{drop}\) is an expression built from two other expressions. In statically-typed functional languages like Coq or Haskell, however, the same expression can't belong to two different, arbitrary types. Thus, to turn an intrinsic into an expression, we need to wrap it up in a constructor, which we called `e_int` here. Other than that, `e_quote` accepts as argument another expression, `e` (the @@ -69,12 +69,12 @@ Inductive value := | v_quot (e : expr). ``` -Then, `v_quot (e_int swap)` would be the Coq translation of the expression \\([\\text{swap}]\\). +Then, `v_quot (e_int swap)` would be the Coq translation of the expression \([\text{swap}]\). However, I didn't decide on this approach for two reasons: * There are now two ways to write a quoted expression: either `v_quote e` to represent a quoted expression that is a value, or `e_quote e` to represent a quoted expression - that is just an expression. In the extreme case, the value \\([[e]]\\) would + that is just an expression. In the extreme case, the value \([[e]]\) would be represented by `v_quote (e_quote e)` - two different constructors for the same concept, in the same expression! * When formalizing the lambda calculus, @@ -88,9 +88,9 @@ but also such that here is no way to prove `IsValue (e_int swap)`, since _that_ a value. But what does "provable" mean, here? By the [Curry-Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence), -a predicate is just a function that takes _something_ and returns a type. Thus, if \\(\\text{Even}\\) -is a predicate, then \\(\\text{Even}\\ 3\\) is actually a type. Since \\(\\text{Even}\\) takes -numbers in, it is a predicate on numbers. Our \\(\\text{IsValue}\\) predicate will be a predicate +a predicate is just a function that takes _something_ and returns a type. Thus, if \(\text{Even}\) +is a predicate, then \(\text{Even}\ 3\) is actually a type. Since \(\text{Even}\) takes +numbers in, it is a predicate on numbers. Our \(\text{IsValue}\) predicate will be a predicate on expressions, instead. In Coq, we can write this as: {{< codelines "Coq" "dawn/Dawn.v" 19 19 >}} @@ -178,8 +178,8 @@ Although the stacks are written in reverse order (which is just a consequence of I hope that the correspondence is fairly clear. If it's not, try reading this rule out loud: > The rule `Sem_swap` says that for every two values `v` and `v'`, and for any stack `vs`, - evaluating `swap` in the original stack `v' :: v :: vs`, aka \\(\\langle V, v, v'\\rangle\\), - results in a final stack `v :: v' :: vs`, aka \\(\\langle V, v', v\\rangle\\). + evaluating `swap` in the original stack `v' :: v :: vs`, aka \(\langle V, v, v'\rangle\), + results in a final stack `v :: v' :: vs`, aka \(\langle V, v', v\rangle\). With that in mind, here's a definition of a predicate `Sem_int`, the evaluation predicate for intrinsics: @@ -189,8 +189,8 @@ for intrinsics: Hey, what's all this with `v_quote` and `projT1`? It's just a little bit of bookkeeping. Given a value -- a pair of an expression `e` and a proof `IsValue e` -- the function `projT1` just returns the expression `e`. That is, it's basically a way of converting a value back into -an expression. The function `v_quote` takes us in the other direction: given an expression \\(e\\), -it constructs a quoted expression \\([e]\\), and combines it with a proof that the newly constructed +an expression. The function `v_quote` takes us in the other direction: given an expression \(e\), +it constructs a quoted expression \([e]\), and combines it with a proof that the newly constructed quote is a value. The above two function in combination help us define the `quote` intrinsic, which @@ -222,8 +222,8 @@ true and false. Why don't we do the same thing? {{< foldtable >}} |UCC Spec| Coq encoding | |---|----| -|\\(\\text{false}\\)=\\([\\text{drop}]\\)| {{< codelines "Coq" "dawn/Dawn.v" 41 42 >}} -|\\(\\text{true}\\)=\\([\\text{swap} \\ \\text{drop}]\\)| {{< codelines "Coq" "dawn/Dawn.v" 44 45 >}} +|\(\text{false}\)=\([\text{drop}]\)| {{< codelines "Coq" "dawn/Dawn.v" 41 42 >}} +|\(\text{true}\)=\([\text{swap} \ \text{drop}]\)| {{< codelines "Coq" "dawn/Dawn.v" 44 45 >}} Let's try prove that these two work as intended. @@ -234,38 +234,38 @@ I invite you to take a look at the "shape" of the proof: * After the initial use of `intros`, which brings the variables `v`, `v`, and `vs` into scope, we start by applying `Sem_e_comp`. Intuitively, this makes sense - at the top level, - our expression, \\(\\text{false}\\ \\text{apply}\\), - is a composition of two other expressions, \\(\\text{false}\\) and \\(\\text{apply}\\). + our expression, \(\text{false}\ \text{apply}\), + is a composition of two other expressions, \(\text{false}\) and \(\text{apply}\). Because of this, we need to use the rule from our semantics that corresponds to composition. * The composition rule requires that we describe the individual effects on the stack of the two constituent expressions (recall that the first expression takes us from the initial stack `v1` to some intermediate stack `v2`, and the second expression takes us from that stack `v2` to the final stack `v3`). Thus, we have two "bullet points": - * The first expression, \\(\\text{false}\\), is just a quoted expression. Thus, the rule + * The first expression, \(\text{false}\), is just a quoted expression. Thus, the rule `Sem_e_quote` applies, and the contents of the quote are puhsed onto the stack. - * The second expression, \\(\\text{apply}\\), is an intrinsic, so we need to use the rule + * The second expression, \(\text{apply}\), is an intrinsic, so we need to use the rule `Sem_e_int`, which handles the intrinsic case. This, in turn, requires that we show the effect of the intrinsic itself; the `apply` intrinsic evaluates the quoted expression on the stack. - The quoted expression contains the body of false, or \\(\\text{drop}\\). This is - once again an intrinsic, so we use `Sem_e_int`; the intrinsic in question is \\(\\text{drop}\\), + The quoted expression contains the body of false, or \(\text{drop}\). This is + once again an intrinsic, so we use `Sem_e_int`; the intrinsic in question is \(\text{drop}\), so the `Sem_drop` rule takes care of that. Following these steps, we arrive at the fact that evaluating `false` on the stack simply drops the top -element, as specified. The proof for \\(\\text{true}\\) is very similar in spirit: +element, as specified. The proof for \(\text{true}\) is very similar in spirit: {{< codelines "Coq" "dawn/Dawn.v" 55 63 >}} -We can also formalize the \\(\\text{or}\\) operator: +We can also formalize the \(\text{or}\) operator: {{< foldtable >}} |UCC Spec| Coq encoding | |---|----| -|\\(\\text{or}\\)=\\(\\text{clone}\\ \\text{apply}\\)| {{< codelines "Coq" "dawn/Dawn.v" 65 65 >}} +|\(\text{or}\)=\(\text{clone}\ \text{apply}\)| {{< codelines "Coq" "dawn/Dawn.v" 65 65 >}} -We can write two top-level proofs about how this works: the first says that \\(\\text{or}\\), -when the first argument is \\(\\text{false}\\), just returns the second argument (this is in agreement -with the truth table, since \\(\\text{false}\\) is the identity element of \\(\\text{or}\\)). +We can write two top-level proofs about how this works: the first says that \(\text{or}\), +when the first argument is \(\text{false}\), just returns the second argument (this is in agreement +with the truth table, since \(\text{false}\) is the identity element of \(\text{or}\)). The proof proceeds much like before: {{< codelines "Coq" "dawn/Dawn.v" 67 73 >}} @@ -276,19 +276,19 @@ Because of this, in this proof writing `apply Sem_apply...` is the same as `apply Sem_apply. apply Sem_e_int`. Since the `Sem_e_int` rule is used a lot, this makes for a very convenient shorthand. -Similarly, we prove that \\(\\text{or}\\) applied to \\(\\text{true}\\) always returns \\(\\text{true}\\). +Similarly, we prove that \(\text{or}\) applied to \(\text{true}\) always returns \(\text{true}\). {{< codelines "Coq" "dawn/Dawn.v" 75 83 >}} -Finally, the specific facts (like \\(\\text{false}\\ \\text{or}\\ \\text{false}\\) evaluating to \\(\\text{false}\\)) +Finally, the specific facts (like \(\text{false}\ \text{or}\ \text{false}\) evaluating to \(\text{false}\)) can be expressed using our two new proofs, `or_false_v` and `or_true`. {{< codelines "Coq" "dawn/Dawn.v" 85 88 >}} ### Derived Expressions #### Quotes -The UCC specification defines \\(\\text{quote}_n\\) to make it more convenient to quote -multiple terms. For example, \\(\\text{quote}_2\\) composes and quotes the first two values +The UCC specification defines \(\text{quote}_n\) to make it more convenient to quote +multiple terms. For example, \(\text{quote}_2\) composes and quotes the first two values on the stack. This is defined in terms of other UCC expressions as follows: {{< latex >}} @@ -300,11 +300,11 @@ We can write this in Coq as follows: {{< codelines "Coq" "dawn/Dawn.v" 90 94 >}} This definition diverges slightly from the one given in the UCC specification; particularly, -UCC's spec mentions that \\(\\text{quote}_n\\) is only defined for \\(n \\geq 1\\).However, +UCC's spec mentions that \(\text{quote}_n\) is only defined for \(n \geq 1\).However, this means that in our code, we'd have to somehow handle the error that would arise if the -term \\(\\text{quote}\_0\\) is used. Instead, I defined `quote_n n` to simply mean -\\(\\text{quote}\_{n+1}\\); thus, in Coq, no matter what `n` we use, we will have a valid -expression, since `quote_n 0` will simply correspond to \\(\\text{quote}_1 = \\text{quote}\\). +term \(\text{quote}_0\) is used. Instead, I defined `quote_n n` to simply mean +\(\text{quote}_{n+1}\); thus, in Coq, no matter what `n` we use, we will have a valid +expression, since `quote_n 0` will simply correspond to \(\text{quote}_1 = \text{quote}\). We can now attempt to prove that this definition is correct by ensuring that the examples given in the specification are valid. We may thus write, @@ -315,7 +315,7 @@ We used a new tactic here, `repeat`, but overall, the structure of the proof is the definition of `quote_n` consists of many intrinsics, and we apply the corresponding rules one-by-one until we arrive at the final stack. Writing this proof was kind of boring, since I just had to see which intrinsic is being used in each step, and then write a line of `apply` -code to handle that intrinsic. This gets worse for \\(\\text{quote}_3\\): +code to handle that intrinsic. This gets worse for \(\text{quote}_3\): {{< codelines "Coq" "dawn/Dawn.v" 108 122 >}} @@ -325,10 +325,10 @@ to write proofs like this itself. Here's what I came up with: {{< codelines "Coq" "dawn/Dawn.v" 124 136 >}} You don't have to understand the details, but in brief, this checks what kind of proof -we're asking Coq to do (for instance, if we're trying to prove that a \\(\\text{swap}\\) +we're asking Coq to do (for instance, if we're trying to prove that a \(\text{swap}\) instruction has a particular effect), and tries to apply a corresponding semantic rule. -Thus, it will try `Sem_swap` if the expression is \\(\\text{swap}\\), -`Sem_clone` if the expression is \\(\\text{clone}\\), and so on. Then, the two proofs become: +Thus, it will try `Sem_swap` if the expression is \(\text{swap}\), +`Sem_clone` if the expression is \(\text{clone}\), and so on. Then, the two proofs become: {{< codelines "Coq" "dawn/Dawn.v" 138 144 >}} @@ -345,7 +345,7 @@ Or, in Coq, {{< codelines "Coq" "dawn/Dawn.v" 148 149 >}} -This is the trick to how \\(\\text{rotate}_n\\) works: it creates a quote of \\(n\\) reordered and composed +This is the trick to how \(\text{rotate}_n\) works: it creates a quote of \(n\) reordered and composed values on the stack, and then evaluates that quote. Since evaluating each value just places it on the stack, these values end up back on the stack, in the same order that they were in the quote. When writing the proof, `solve_basic ()` gets us almost all the way to the @@ -357,7 +357,7 @@ placed back on the stack. ### `e_comp` is Associative When composing three expressions, which way of inserting parentheses is correct? -Is it \\((e_1\\ e_2)\\ e_3\\)? Or is it \\(e_1\\ (e_2\\ e_3)\\)? Well, both! +Is it \((e_1\ e_2)\ e_3\)? Or is it \(e_1\ (e_2\ e_3)\)? Well, both! Expression composition is associative, which means that the order of the parentheses doesn't matter. We state this in the following theorem, which says that the two ways of writing the composition, if they evaluate to anything, evaluate to the same thing. @@ -372,8 +372,8 @@ says: I think that UCC is definitely getting there: formally defining the semantics outlined on the page was quite straightforward. We can now have complete confidence in the behavior -of \\(\\text{true}\\), \\(\\text{false}\\), \\(\\text{or}\\), \\(\\text{quote}_n\\) and -\\(\\text{rotate}_n\\). The proof of associativity is also enough to possibly argue for simplifying +of \(\text{true}\), \(\text{false}\), \(\text{or}\), \(\text{quote}_n\) and +\(\text{rotate}_n\). The proof of associativity is also enough to possibly argue for simplifying the core calculus' syntax even more. All of this we got from an official source, with only a little bit of tweaking to get from the written description of the language to code! I'm looking forward to reading the next post about the _multistack_ concatenative calculus.