diff --git a/assets/sass/_content.scss b/assets/sass/_content.scss index 140f285..d45b547 100644 --- a/assets/sass/_content.scss +++ b/assets/sass/_content.scss @@ -124,6 +124,7 @@ a code { } pre > code { + color: $text-color; display: block; padding: 5px; overflow-x: auto; @@ -156,7 +157,56 @@ table.table { } } -.post-content { +.post-container { + display: flex; + + @media screen and (max-width: 520px) { + flex-direction: column; + .toc-drawer { display: block; } + .toc-list { display: none; } + } + + @media screen and (min-width: 520px) { + flex-direction: row; + align-items: flex-start; + gap: 12px; + + .toc-drawer { display: none; } + .toc-list { + top: 0; + display: block; + position: sticky; + min-width: 160px; + } + } + + .post-content { + min-width: 1px; + } + + .toc-draw #TableOfContents, .toc-list #TableOfContents { + ul { + list-style-type: "\22A2 "; + padding-left: 1rem; + + li { + margin-bottom: 0.5rem; + } + } + + li ul { + margin-top: 0.5rem; + } + } +} + +.division .post-content, .post-content { + .heading { + a { + color: $heading-color; + } + } + > p { line-height: 1.5; } diff --git a/assets/sass/main.scss b/assets/sass/main.scss index 743ecab..ebe40de 100644 --- a/assets/sass/main.scss +++ b/assets/sass/main.scss @@ -4,7 +4,8 @@ @font-face { font-family: 'PragmataPro Mono Liga'; - src: url('/fonts/PragmataPro_Mono_R_liga_0829.woff2') format('woff2'); + src: url("/fonts/PragmataPro_Mono_R_liga_0829.woff2") format("woff2"), + url(https://mzhang.io/fonts/PragmataPro_Mono_R_liga_0829.woff2) format("woff2"); } $sansfont: "Helvetica", "Arial", "Liberation Sans", sans-serif; @@ -26,7 +27,7 @@ $monofont: "PragmataPro Mono Liga", "Roboto Mono", "Roboto Mono for Powerline", } @media (prefers-color-scheme: dark) { - $background-color: #15202B; + $background-color: #151520; $faded-background-color: lighten($background-color, 10%); $heading-color: #E4E4E4; $text-color: #BCBCBC; diff --git a/config.toml b/config.toml index b91dc7e..b381f39 100644 --- a/config.toml +++ b/config.toml @@ -9,7 +9,7 @@ language = "languages" [markup.tableOfContents] endLevel = 4 -ordered = true +ordered = false startLevel = 2 [markup.goldmark.renderer] diff --git a/content/posts/2022-02-02-formal-cek-machine-in-agda/_index.md b/content/posts/2022-02-02-formal-cek-machine-in-agda/_index.md new file mode 100644 index 0000000..38e9f6d --- /dev/null +++ b/content/posts/2022-02-02-formal-cek-machine-in-agda/_index.md @@ -0,0 +1,96 @@ ++++ +title = "a formal cek machine in agda" +draft = true +date = 2022-02-02 +tags = ["computer-science", "programming-languages", "formal-verification", "lambda-calculus"] +languages = ["agda"] +layout = "single" +toc = true ++++ + + + +Last semester, I took a course on reasoning about programming languages using +Agda, a dependently typed meta-language. For the term project, we were to +implement a simply-typed lambda calculus with several extensions, along with +proofs of certain properties. + +My lambda calculus implemented `call/cc` on top of a CEK machine. + +## Foreword + +**Why is this interesting?** Reasoning about languages is one way of ensuring +whole-program correctness. Building up these languages from foundations grounded +in logic helps us achieve our goal with more rigor. + +As an example, suppose I wrote a function that takes a list of numbers and +returns the maximum value. Mathematically speaking, this function would be +_non-total_; an input consisting of an empty set would not produce reasonable +output! If this were a library function I'd like to tell people who write code +that uses this function "don't give me an empty list!" + +Unfortunately, just writing this in documentation isn't enough. What we'd really +like is for a tool (like a compiler) to tell any developer who is trying to pass +an empty list into our maximum function "You can't do that." Unfortunately, most +of the popular languages being used today have no way of describing "a list +that's not empty." + +## Lambda calculus + +The lambda calculus is a mathematical structure for describing computation. At +the most basic level, it defines a concept called a _term_. Everything that can +be represented in a lambda calculus is some combination of terms. A term can +have several constructors: + +- **Var.** This is just a variable, like `x` or `y`. During evaluation, a + variable can resolve to a value in the evaluation environment by name. If + the environment says `{ x = 5 }`, then evaluating `x` would result in 5. + +- **Abstraction, or lambda (λ).** An _abstraction_ is a term that describes some + other computation. From an algebraic perspective, it can be thought of as a + function with a single argument (i.e f(x) = 2x is an abstraction, although + it would be written `(λx.2x)`) + +- **Application.** Application is sort of the opposite of abstraction, exposing + the computation that was abstracted away. From an algebraic perspective, + this is just function application (i.e applying `f(x) = 2x` to 3 would + result in 2\*3. Note that only a simple substitution has been done and + further evaluation is required to reduce 2*3) + +### Why? + +The reason it's set up this way is so we can reason about terms inductively. The +idea is that because terms are just nested constructors, we can describe the +behavior of any term by just defining the behavior of these 3 constructors. + +Interestingly, the lambda calculus is Turing-complete, so any computation can be +reduced to those 3 constructs. I used numbers liberally in the examples above, +but in a lambda calculus without numbers, you could define integers recursively +like this: + +- Let `z` represent zero. +- Let `s` represent a "successor", or increment function. `s(z)` represents 1, + `s(s(z))` represents 2, and so on. + +In lambda calculus terms, this would look like: + +- 0 = `λs.(λz.z)` +- 1 = `λs.(λz.s(z))` +- 2 = `λs.(λz.s(s(z)))` +- 3 = `λs.(λz.s(s(s(z))))` + +In practice, many lambda calculus have a set of "base" values from which to +build off, such as unit values, booleans, and natural numbers (having numbers in +the language means we don't need the `s` and `z` dance to refer to them). + +### Turing completeness + +As I noted above, the lambda calculus is _Turing-complete_. One feature of +Turing complete systems is that they have a (provably!) unsolvable "halting" +problem. + +### Simply-typed lambda calculus (STLC) + +## CEK machine + +A CEK machine diff --git a/layouts/_default/_markup/render-heading.html b/layouts/_default/_markup/render-heading.html new file mode 100644 index 0000000..ea750a6 --- /dev/null +++ b/layouts/_default/_markup/render-heading.html @@ -0,0 +1,3 @@ + + {{ .Text | safeHTML }} + diff --git a/layouts/partials/post-list.html b/layouts/partials/post-list.html index c80ace8..18bdd03 100644 --- a/layouts/partials/post-list.html +++ b/layouts/partials/post-list.html @@ -1,19 +1,21 @@ {{- range .Pages -}} - - + - +
+ + + {{ end }} {{- end -}}
- - {{ .Title }} - -
- - {{ .ReadingTime }} min read - + {{ if not .Draft }} +
+ + {{ .Title }} + +
+ + {{ .ReadingTime }} min read - - {{ .Date.Format "Mon Jan 02, 2006" }} - + {{ .Date.Format "Mon Jan 02, 2006" }} + -
-
diff --git a/layouts/posts/single.html b/layouts/posts/single.html index 5c5eb5b..70caf6a 100644 --- a/layouts/posts/single.html +++ b/layouts/posts/single.html @@ -18,24 +18,28 @@ - {{ .ReadingTime }} min read -{{ if .Params.toc }} -
-
- Table of Contents - {{ .TableOfContents }} -
+
+ {{ if .Params.toc }} +
+
+ Table of Contents + {{ .TableOfContents }} +
+
+
+ {{ .TableOfContents }} +
+ {{ end }} +
{{ .Content }}
-{{ end }} - -
{{ .Content }}
Thanks for reading! - {{ if .Params.mastodon }} - Have comments? Discuss this post on Mastodon. - {{ end }} + + Have comments? Discuss this post by sending me a + public email. {{- end -}}