2023-09-01 14:16:36 +00:00
|
|
|
---
|
2023-09-01 14:24:12 +00:00
|
|
|
title: Building a formal CEK machine in Agda
|
2023-09-01 14:16:36 +00:00
|
|
|
draft: true
|
|
|
|
date: 2023-09-01T13:53:23.974Z
|
2023-09-01 14:24:12 +00:00
|
|
|
tags:
|
|
|
|
- computer-science
|
|
|
|
- programming-languages
|
|
|
|
- formal-verification
|
|
|
|
- lambda-calculus
|
|
|
|
|
|
|
|
heroImage: ./header.jpg
|
|
|
|
heroAlt: gears spinning wallpaper
|
|
|
|
math: true
|
2023-09-01 14:16:36 +00:00
|
|
|
---
|
|
|
|
|
|
|
|
Back in 2022, I took a special topics course, CSCI 8980, on [reasoning about
|
|
|
|
programming languages using Agda][plfa], 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.
|
|
|
|
|
|
|
|
[plfa]: https://plfa.github.io/
|
|
|
|
|
|
|
|
My lambda calculus implemented `call/cc` on top of a CEK machine.
|
|
|
|
|
|
|
|
<details>
|
|
|
|
<summary><b>Why is this interesting?</b></summary>
|
|
|
|
|
|
|
|
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!"
|
|
|
|
|
|
|
|
But 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."
|
|
|
|
|
|
|
|
We still have a way to prevent people from running into this problem, though
|
|
|
|
it involves pushing the problem to runtime rather than compile time. The
|
|
|
|
maximum function could return an "optional" maximum. Some languages'
|
|
|
|
implementations of optional values force programmers to handle the "nothing"
|
|
|
|
case, while others ignore it silently. But in the more optimistic case, even
|
|
|
|
if the list was empty, the caller would have handled it and treated it
|
|
|
|
accordingly.
|
|
|
|
|
|
|
|
This isn't a pretty way to solve this problem. _Dependent types_ gives us
|
|
|
|
tools to solve this problem in an elegant way, by giving the type system the
|
|
|
|
ability to contain values. This also opens its own can of worms, but for
|
|
|
|
questions about program correctness, it is more valuable than depending on
|
|
|
|
catching problems at runtime.
|
|
|
|
|
|
|
|
</details>
|
|
|
|
|
|
|
|
## Crash course on the lambda calculus
|
|
|
|
|
|
|
|
The [lambda calculus] is a mathematical abstraction for computation. The core
|
|
|
|
mechanism it uses is 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:
|
|
|
|
|
|
|
|
[lambda calculus]: https://en.wikipedia.org/wiki/Lambda_calculus
|
|
|
|
|
2023-09-01 14:24:12 +00:00
|
|
|
- **Var.** This is just a variable, like `x` or `y`. By itself it holds no
|
|
|
|
meaning, but during evaluation, the evaluation _environment_ holds a mapping
|
|
|
|
from variable names to the values. If the environment says `{ x = 5 }`, then
|
|
|
|
evaluating `x` would result in 5.
|
2023-09-01 14:16:36 +00:00
|
|
|
|
|
|
|
- **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.
|
|
|
|
Rather than having lots of syntax for making it easier for programmers to write
|
|
|
|
a for loop as opposed to a while loop, or constructing different kinds of
|
|
|
|
values, the lambda calculus focuses on function abstraction and calls, and
|
|
|
|
strips everything else away.
|
|
|
|
|
|
|
|
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. The
|
|
|
|
flavorful features of other programming languages can be implemented on top of
|
|
|
|
the function call rules in ways that don't disrupt the basic function of the
|
|
|
|
evaluation.
|
|
|
|
|
2023-09-01 14:24:12 +00:00
|
|
|
In fact, the lambda calculus is [Turing-complete][tc], so any computation can
|
2023-09-01 14:16:36 +00:00
|
|
|
technically 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 using a recursive strategy called [Church numerals]. It looks like this:
|
|
|
|
|
|
|
|
[church numerals]: https://en.wikipedia.org/wiki/Church_encoding
|
|
|
|
|
|
|
|
- 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 incorporate higher level constructors such as
|
|
|
|
numbers or lists to make it so we can avoid having to represent them using only
|
|
|
|
a series of function calls. However, any time we add more syntax to a language,
|
|
|
|
we increase its complexity in proofs, so for now let's keep it simple.
|
|
|
|
|
|
|
|
### The Turing completeness curse
|
|
|
|
|
|
|
|
As I noted above, the lambda calculus is [_Turing-complete_][tc]. One feature of
|
|
|
|
Turing complete systems is that they have a (provably!) unsolvable "halting"
|
|
|
|
problem. Most of the simple terms shown above terminate predictably. But as an
|
|
|
|
example of a term that doesn't halt, consider the _Y combinator_, an example of
|
|
|
|
a fixed-point combinator:
|
|
|
|
|
|
|
|
[tc]: https://en.wikipedia.org/wiki/Turing_completeness
|
|
|
|
|
|
|
|
Y = λf.(λx.f(x(x)))(λx.f(x(x)))
|
|
|
|
|
|
|
|
That's quite a mouthful. If you tried calling Y on some term, you will find that
|
|
|
|
evaluation will quickly expand infinitely. That makes sense given its purpose:
|
|
|
|
to find a _fixed point_ of whatever function you pass in.
|
|
|
|
|
|
|
|
> As an example, the fixed-point of the function f(x) = sqrt(x) is 1. That's
|
|
|
|
> because f(1) = 1. The Y combinator attempts to find the fixed point by simply
|
|
|
|
> applying the function multiple times. In the untyped lambda calculus, this can
|
|
|
|
> be used to implement simple (but possibly unbounded) recursion.
|
|
|
|
|
|
|
|
This actually proves disastrous for trying to reason about the logic of a
|
|
|
|
program. If we don't even know for sure if something will halt, how can we know
|
|
|
|
that it'll produce the correct value? In fact, you can prove false statements
|
|
|
|
using infinite recursion as a basis.
|
|
|
|
|
|
|
|
This is why we actually prefer _not_ to work with Turing-complete languages when
|
|
|
|
doing logical reasoning on program evaluation. Instead, we always want to add
|
|
|
|
some constraints on it to make evaluation total, ensuring that we have perfect
|
|
|
|
information about our program's behavior.
|
|
|
|
|
|
|
|
### Simply-typed lambda calculus
|
|
|
|
|
2023-09-01 14:24:12 +00:00
|
|
|
The [simply-typed lambda calculus] (STLC) adds types to every term. Types are
|
2023-09-01 14:16:36 +00:00
|
|
|
crucial to any kind of static program analysis. Suppose I was trying to apply
|
|
|
|
the term 5 to 6 (in other words, call 5 with the argument 6 as if 5 was a
|
|
|
|
function). As humans we can look at that and instantly recognize that the
|
|
|
|
evaluation would be invalid, yet under the untyped lambda calculus, it would be
|
|
|
|
completely representable.
|
|
|
|
|
2023-09-01 14:24:12 +00:00
|
|
|
[simply-typed lambda calculus]: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
|
|
|
|
|
2023-09-01 14:16:36 +00:00
|
|
|
To solve this in STLC, we would make this term completely unrepresentable at
|
|
|
|
all. To say you want to apply 5 to 6 would not be a legal STLC term. We do this
|
|
|
|
by requiring that all STLC terms are untyped lambda calculus terms accompanied
|
|
|
|
by a _type_.
|
|
|
|
|
|
|
|
This gives us more information about what's allowed before we run the
|
|
|
|
evaluation. For example, numbers may have their own type `Nat` (for "natural
|
|
|
|
number"), while functions have a special "arrow" type `_ -> _`, where the
|
|
|
|
underscores represent other types. A function that takes a number and returns a
|
|
|
|
boolean (like isEven) would have the type `Nat -> Bool`, while a function that
|
|
|
|
takes a boolean and returns another boolean would be `Bool -> Bool`.
|
|
|
|
|
|
|
|
With this, we have a framework for rejecting terms that would otherwise be legal
|
|
|
|
in untyped lambda calculus, but would break when we tried to evaluate them. A
|
|
|
|
function application would be able to require that the argument is the same type
|
|
|
|
as what the function is expecting.
|
|
|
|
|
|
|
|
The nice property you get now is that all valid STLC programs will never get
|
|
|
|
_stuck_, which is being unable to evaluate due to some kind of error. Each term
|
|
|
|
will either be able to be evaluated to a next state, or is done.
|
|
|
|
|
|
|
|
A semi-formal definition for STLC terms would look something like this:
|
|
|
|
|
|
|
|
- **Var.** Same as before, it's a variable that can be looked up in the
|
|
|
|
environment.
|
|
|
|
|
|
|
|
- **Abstraction, or lambda (λ).** This is a function that carries three pieces
|
|
|
|
of information: (1) the name of the variable that its input will be substituted
|
|
|
|
for, (2) the _type_ of the input, and (3) the body in which the substitution
|
|
|
|
will happen.
|
|
|
|
|
|
|
|
- **Application.** Same as before.
|
|
|
|
|
|
|
|
It doesn't really seem like changing just one term changes the language all that
|
|
|
|
much. But as a result of this tiny change, _every_ term now has a type:
|
|
|
|
|
|
|
|
- `5 :: Nat`
|
|
|
|
- `λ(x:Nat).2x :: Nat -> Nat`
|
|
|
|
- `isEven(3) :: (Nat -> Bool) · Nat = Bool`
|
|
|
|
|
|
|
|
Notation: (`x :: T` means `x` has type `T`, and `f · x` means `f` applied to
|
|
|
|
`x`)
|
|
|
|
|
|
|
|
This also means that some values are now unrepresentable:
|
|
|
|
|
|
|
|
- `isEven(λx.2x) :: (Nat -> Bool) · (Nat -> Nat)` doesn't work because the type
|
|
|
|
of `λx.2x :: Nat -> Nat` can't be used as an input for `isEven`, which is
|
|
|
|
expecting a `Nat`.
|
|
|
|
|
|
|
|
We have a good foundation for writing programs now, but this by itself can't
|
|
|
|
qualify as a system for computation. We need an abstract machine of sorts that
|
|
|
|
can evaluate these symbols and actually compute on them.
|
|
|
|
|
|
|
|
In practice, there's a number of different possible abstract machines that can
|
|
|
|
evaluate the lambda calculus. Besides the basic direct implementation, alternate
|
|
|
|
implementations such as [interaction nets] have become popular due to being able
|
|
|
|
to be parallelized efficiently.
|
|
|
|
|
|
|
|
[interaction nets]: https://en.wikipedia.org/wiki/Interaction_nets
|
|
|
|
|
|
|
|
## CEK machine
|
|
|
|
|
|
|
|
A CEK machine is responsible for evaluating a lambda calculus term.
|