From f00c69f02c15b85b6819f7db91870ccdabaedee4 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 3 Nov 2024 17:50:11 -0800 Subject: [PATCH] Edit and publish SPA part 5 --- content/blog/05_spa_agda_semantics/index.md | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/content/blog/05_spa_agda_semantics/index.md b/content/blog/05_spa_agda_semantics/index.md index 11e897e..9b86d3b 100644 --- a/content/blog/05_spa_agda_semantics/index.md +++ b/content/blog/05_spa_agda_semantics/index.md @@ -4,7 +4,6 @@ series: "Static Program Analysis in Agda" description: "In this post, I define the language that well serve as the object of our vartious analyses" date: 2024-08-10T17:37:43-07:00 tags: ["Agda", "Programming Languages"] -draft: true custom_js: ["parser.js"] bergamot: render_presets: @@ -269,7 +268,7 @@ thus be written as follows: {{< /latex >}} Now, on to the actual rules for how to evaluate expressions. Most simply, -integer literals `1` just evaluate to themselves. +integer literals like `1` just evaluate to themselves. {{< latex >}} \frac{n \in \text{Int}}{\rho, n \Downarrow n} @@ -336,7 +335,7 @@ I showed above. #### Simple Statements The main difference between formalizing (simple and "normal") statements is that they modify the environment. If `x` has one value, writing `x = x + 1` will -certainly change that value. On the other hands, statements don't produce values. +certainly change that value. On the other hand, statements don't produce values. So, we will be writing claims like \(\rho_1 , \textit{bs} \Rightarrow \rho_2\) to say that the basic statement \(\textit{bs}\), when starting in environment \(\rho_1\), will produce environment \(\rho_2\). Here's an example: @@ -472,13 +471,9 @@ final state, so that's what we use in the rule's conclusion. {{< /latex >}} And that's it! We have now seen every rule that defines the little object language -I've been using for my Agda work. As with all the other rules we've seen, the -mathematical notation above can be directly translated into Agda: - -{{< codelines "Agda" "agda-spa/Language/Semantics.agda" 47 64 >}} - -Below is a Bergamot widget that implements these rules. Try the following program, -which computes the `x`th power of two, and stores it in `y`: +I've been using for my Agda work. Below is a Bergamot widget that implements +these rules. Try the following program, which computes the `x`th power of two, +and stores it in `y`: ``` x = 5; y = 1; while (x) { y = y + y; x = x - 1 } @@ -520,6 +515,11 @@ hidden section "" { } {{< /bergamot_widget >}} +As with all the other rules we've seen, the mathematical notation above can +be directly translated into Agda: + +{{< codelines "Agda" "agda-spa/Language/Semantics.agda" 47 64 >}} + ### Semantics as Ground Truth Prior to this post, we had been talking about using lattices and monotone