Start drafting CEK
This commit is contained in:
Michael Zhang
parent
f4d9ae6b14
commit
56bbbc5dee
7 changed files with 185 additions and 29 deletions
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ language = "languages"
|
|||
|
||||
[markup.tableOfContents]
|
||||
endLevel = 4
|
||||
ordered = true
|
||||
ordered = false
|
||||
startLevel = 2
|
||||
|
||||
[markup.goldmark.renderer]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
+++
|
||||
|
||||
<!--more-->
|
||||
|
||||
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
|
||||
3
layouts/_default/_markup/render-heading.html
Normal file
3
layouts/_default/_markup/render-heading.html
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
<h{{ .Level }} id="{{ .Anchor | safeURL }}" class="heading">
|
||||
<a href="#{{ .Anchor | safeURL }}">{{ .Text | safeHTML }}</a>
|
||||
</h{{ .Level }}>
|
||||
|
|
@ -1,19 +1,21 @@
|
|||
<table style="width: 100%;">
|
||||
{{- range .Pages -}}
|
||||
<tr class="postlisting-row">
|
||||
<td>
|
||||
<span class="title">
|
||||
<a href="{{ .RelPermalink }}" class="brand-colorlink">{{ .Title }}</a>
|
||||
</span>
|
||||
<br />
|
||||
<small>
|
||||
{{ .ReadingTime }} min read -
|
||||
{{ if not .Draft }}
|
||||
<tr class="postlisting-row">
|
||||
<td>
|
||||
<span class="title">
|
||||
<a href="{{ .RelPermalink }}" class="brand-colorlink">{{ .Title }}</a>
|
||||
</span>
|
||||
<br />
|
||||
<small>
|
||||
{{ .ReadingTime }} min read -
|
||||
|
||||
{{ .Date.Format "Mon Jan 02, 2006" }}
|
||||
</small>
|
||||
{{ .Date.Format "Mon Jan 02, 2006" }}
|
||||
</small>
|
||||
|
||||
<br />
|
||||
</td>
|
||||
</tr>
|
||||
<br />
|
||||
</td>
|
||||
</tr>
|
||||
{{ end }}
|
||||
{{- end -}}
|
||||
</table>
|
||||
|
|
|
|||
|
|
@ -18,24 +18,28 @@
|
|||
- {{ .ReadingTime }} min read
|
||||
</small>
|
||||
|
||||
{{ if .Params.toc }}
|
||||
<div class="toc">
|
||||
<details>
|
||||
<summary>Table of Contents</summary>
|
||||
{{ .TableOfContents }}
|
||||
</details>
|
||||
<div class="post-container">
|
||||
{{ if .Params.toc }}
|
||||
<div class="toc-drawer">
|
||||
<details>
|
||||
<summary>Table of Contents</summary>
|
||||
{{ .TableOfContents }}
|
||||
</details>
|
||||
</div>
|
||||
<div class="toc-list">
|
||||
{{ .TableOfContents }}
|
||||
</div>
|
||||
{{ end }}
|
||||
<div id="content" class="post-content">{{ .Content }}</div>
|
||||
</div>
|
||||
{{ end }}
|
||||
|
||||
<div id="content" class="post-content">{{ .Content }}</div>
|
||||
|
||||
<hr />
|
||||
|
||||
<small>
|
||||
Thanks for reading!
|
||||
{{ if .Params.mastodon }}
|
||||
Have comments? Discuss this post on <a href="{{ .Params.mastodon }}" target="_blank">Mastodon</a>.
|
||||
{{ end }}
|
||||
|
||||
Have comments? Discuss this post by sending me a
|
||||
<a href="mailto:~mzhang/public-inbox@lists.sr.ht?subject=Re:+{{ .Title }}">public email</a>.
|
||||
</small>
|
||||
|
||||
{{- end -}}
|
||||
|
|
|
|||
Loading…
Reference in a new issue