update
All checks were successful
ci/woodpecker/push/woodpecker Pipeline was successful

This commit is contained in:
Michael Zhang 2023-09-01 09:24:12 -05:00
parent b47c8ffae3
commit 5ecc5f8eed
3 changed files with 19 additions and 7 deletions

View file

@ -26,6 +26,7 @@ const posts = defineCollection({
tags: z.array(z.string()), tags: z.array(z.string()),
draft: z.boolean().default(false), draft: z.boolean().default(false),
math: z.boolean().default(false),
}), }),
}); });

Binary file not shown.

After

Width:  |  Height:  |  Size: 630 KiB

View file

@ -1,8 +1,16 @@
--- ---
title: Building a formal CEK machine in agda title: Building a formal CEK machine in Agda
draft: true draft: true
date: 2023-09-01T13:53:23.974Z date: 2023-09-01T13:53:23.974Z
tags: ["computer-science", "programming-languages", "formal-verification", "lambda-calculus"] tags:
- computer-science
- programming-languages
- formal-verification
- lambda-calculus
heroImage: ./header.jpg
heroAlt: gears spinning wallpaper
math: true
--- ---
Back in 2022, I took a special topics course, CSCI 8980, on [reasoning about Back in 2022, I took a special topics course, CSCI 8980, on [reasoning about
@ -58,9 +66,10 @@ several constructors:
[lambda calculus]: https://en.wikipedia.org/wiki/Lambda_calculus [lambda calculus]: https://en.wikipedia.org/wiki/Lambda_calculus
- **Var.** This is just a variable, like `x` or `y`. During evaluation, a - **Var.** This is just a variable, like `x` or `y`. By itself it holds no
variable can resolve to a value in the evaluation environment by name. If meaning, but during evaluation, the evaluation _environment_ holds a mapping
the environment says `{ x = 5 }`, then evaluating `x` would result in 5. from variable names to the values. If the environment says `{ x = 5 }`, then
evaluating `x` would result in 5.
- **Abstraction, or lambda (λ).** An _abstraction_ is a term that describes some - **Abstraction, or lambda (λ).** An _abstraction_ is a term that describes some
other computation. From an algebraic perspective, it can be thought of as a other computation. From an algebraic perspective, it can be thought of as a
@ -87,7 +96,7 @@ 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 the function call rules in ways that don't disrupt the basic function of the
evaluation. evaluation.
In fact, the lambda calculus is Turing-complete, so any computation can In fact, the lambda calculus is [Turing-complete][tc], so any computation can
technically be reduced to those 3 constructs. I used numbers liberally in the 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 examples above, but in a lambda calculus without numbers, you could define
integers using a recursive strategy called [Church numerals]. It looks like this: integers using a recursive strategy called [Church numerals]. It looks like this:
@ -143,13 +152,15 @@ information about our program's behavior.
### Simply-typed lambda calculus ### Simply-typed lambda calculus
The simply-typed lambda calculus (STLC) adds types to every term. Types are The [simply-typed lambda calculus] (STLC) adds types to every term. Types are
crucial to any kind of static program analysis. Suppose I was trying to apply 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 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 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 evaluation would be invalid, yet under the untyped lambda calculus, it would be
completely representable. completely representable.
[simply-typed lambda calculus]: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
To solve this in STLC, we would make this term completely unrepresentable at 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 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 requiring that all STLC terms are untyped lambda calculus terms accompanied