Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Edit and publish SPA part 5

Browse Source
This commit is contained in:
Danila Fedorin 2024-11-03 17:50:11 -08:00
parent 4fc1191d13
commit f00c69f02c
1 changed files with 10 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
content/blog/05_spa_agda_semantics/index.md
View File

@ -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" 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 date: 2024-08-10T17:37:43-07:00
tags: ["Agda", "Programming Languages"] tags: ["Agda", "Programming Languages"]
draft: true
custom_js: ["parser.js"] custom_js: ["parser.js"]
bergamot: bergamot:
render_presets: render_presets:
@ -269,7 +268,7 @@ thus be written as follows:
{{< /latex >}} {{< /latex >}}
Now, on to the actual rules for how to evaluate expressions. Most simply, 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 >}} {{< latex >}}
\frac{n \in \text{Int}}{\rho, n \Downarrow n} \frac{n \in \text{Int}}{\rho, n \Downarrow n}
@ -336,7 +335,7 @@ I showed above.
#### Simple Statements #### Simple Statements
The main difference between formalizing (simple and "normal") statements is 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 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\) 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 to say that the basic statement \(\textit{bs}\), when starting in environment
\(\rho_1\), will produce environment \(\rho_2\). Here's an example: \(\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 >}} {{< /latex >}}
And that's it! We have now seen every rule that defines the little object language 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 I've been using for my Agda work. Below is a Bergamot widget that implements
mathematical notation above can be directly translated into Agda: these rules. Try the following program, which computes the `x`th power of two,
and stores it in `y`:
{{< 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`:
``` ```
x = 5; y = 1; while (x) { y = y + y; x = x - 1 } x = 5; y = 1; while (x) { y = y + y; x = x - 1 }
@ -520,6 +515,11 @@ hidden section "" {
} }
{{< /bergamot_widget >}} {{< /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 ### Semantics as Ground Truth
Prior to this post, we had been talking about using lattices and monotone Prior to this post, we had been talking about using lattices and monotone