From 1f454d68831099411ede6f3681d9fd01c578d6a1 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Fri, 5 Apr 2024 21:52:20 -0500
Subject: [PATCH] lambda calc post

---
 astro.config.ts                               |   6 +-
 plugin/remark-admonitions.ts                  |  14 +-
 .../posts/2024-04-04-lambda-calculus.md       | 145 ++++++++++++++++++
 src/content/posts/2024-04-04-test.md          |  36 -----
 4 files changed, 156 insertions(+), 45 deletions(-)
 create mode 100644 src/content/posts/2024-04-04-lambda-calculus.md
 delete mode 100644 src/content/posts/2024-04-04-test.md

diff --git a/astro.config.ts b/astro.config.ts
index e00c05e..e4c8a9f 100644
--- a/astro.config.ts
+++ b/astro.config.ts
@@ -4,7 +4,7 @@ import sitemap from "@astrojs/sitemap";
 import { rehypeAccessibleEmojis } from "rehype-accessible-emojis";
 
 import remarkReadingTime from "./plugin/remark-reading-time";
-import emoji from "remark-emoji";
+import remarkEmoji from "remark-emoji";
 import remarkMermaid from "astro-diagram/remark-mermaid";
 import remarkDescription from "astro-remark-description";
 import remarkAdmonitions from "./plugin/remark-admonitions";
@@ -26,12 +26,12 @@ export default defineConfig({
     syntaxHighlight: "shiki",
     shikiConfig: { theme: "css-variables" },
     remarkPlugins: [
+      remarkMath,
       remarkAdmonitions,
       remarkReadingTime,
       remarkTypst,
-      [remarkMath, {}],
       remarkMermaid,
-      emoji,
+      remarkEmoji,
       [remarkDescription, { name: "excerpt" }],
     ],
     rehypePlugins: [
diff --git a/plugin/remark-admonitions.ts b/plugin/remark-admonitions.ts
index 4900a5f..1391833 100644
--- a/plugin/remark-admonitions.ts
+++ b/plugin/remark-admonitions.ts
@@ -16,13 +16,13 @@ export default remarkAdmonitions;
 
 const handleNode = (config: Config): BuildVisitor => (node) => {
   // Filter required elems
-  if (node.type != "blockquote") return;
+  if (node.type !== "blockquote") return;
   const blockquote = node as Blockquote;
 
-  if (blockquote.children[0]?.type != "paragraph") return;
+  if (blockquote.children[0]?.type !== "paragraph") return;
 
   const paragraph = blockquote.children[0];
-  if (paragraph.children[0]?.type != "text") return;
+  if (paragraph.children[0]?.type !== "text") return;
 
   const text = paragraph.children[0];
 
@@ -139,8 +139,8 @@ type ClassNameMap = ClassNames | ((title: string) => ClassNames);
 
 export function classNameMap(gen: ClassNameMap) {
   return (title: string) => {
-    const classNames = typeof gen == "function" ? gen(title) : gen;
-    return typeof classNames == "object" ? classNames.join(" ") : classNames;
+    const classNames = typeof gen === "function" ? gen(title) : gen;
+    return typeof classNames === "object" ? classNames.join(" ") : classNames;
   };
 }
 
@@ -148,6 +148,8 @@ type NameFilter = ((title: string) => boolean) | string[];
 
 export function nameFilter(filter: NameFilter) {
   return (title: string) => {
-    return typeof filter == "function" ? filter(title) : filter.includes(title);
+    return typeof filter === "function"
+      ? filter(title)
+      : filter.includes(title);
   };
 }
diff --git a/src/content/posts/2024-04-04-lambda-calculus.md b/src/content/posts/2024-04-04-lambda-calculus.md
new file mode 100644
index 0000000..96d71ca
--- /dev/null
+++ b/src/content/posts/2024-04-04-lambda-calculus.md
@@ -0,0 +1,145 @@
+---
+title: The Lambda Calculus
+date: 2024-04-04T21:45:28.264
+draft: true
+toc: true
+languages: ["typst"]
+tags: ["typst"]
+---
+
+The lambda calculus is an abstract machine for modeling computation. In this
+tutorial I will build up the lambda calculus from scratch.
+
+## Expressions
+
+Let's start with expressions. You've probably encountered these in math class.
+They look like things like:
+
+- $3$
+- $5 \times 5$
+- $2\sqrt{12} - 5i$
+
+Some of these probably look like they can be simplified. That's fine! We're not
+worried about that yet. The computation aspect will come in a bit.
+
+### Expression Trees
+
+The important thing here is that all of these have some tree-like structure. For
+example, look at $5 \times 5$:
+
+```typst
+#import "@preview/fletcher:0.4.3" as fletcher: *
+#set page(width: auto, height: auto, margin: (x: 0.25pt, y: 0.25pt))
+#set text(18pt)
+#diagram(cell-size: 0.5cm, $
+    & times edge("dl", ->) edge("dr", ->) \
+    5 & & 5 \
+$)
+```
+
+And that last one, $2\sqrt{12} - 5i$:
+
+```typst
+#import "@preview/fletcher:0.4.3" as fletcher: *
+#import math
+#set page(width: auto, height: auto, margin: (x: 0.5em, y: 0.5em))
+#set text(18pt)
+#diagram(cell-size: 0.5cm, {
+    node(pos: (0, 0), label: $-$)
+    node(pos: (-1, 1), label: $times$)
+    node(pos: (1, 1), label: $times$)
+    edge((0, 0), (-1, 1))
+    edge((0, 0), (1, 1))
+    node(pos: (-1.5, 2), label: $2$)
+    node(pos: (-0.5, 2), label: $math.sqrt(...)$)
+    node(pos: (-0.5, 3), label: $12$)
+    edge((-1, 1), (-1.5, 2))
+    edge((-1, 1), (-0.5, 2))
+    edge((-0.5, 2), (-0.5, 3))
+    node(pos: (0.5, 2), label: $5$)
+    node(pos: (1.5, 2), label: $i$)
+    edge((1, 1), (0.5, 2))
+    edge((1, 1), (1.5, 2))
+})
+```
+
+These follow the order of operations (also known as PEMDAS). They tell you that
+_if_ you were going to evaluate this, you would want to apply it in this
+fashion.
+
+If you look at each point in the tree, you might notice that there's several different types of branches:
+
+- Numbers, like $2$, $5$, or $12$ don't have any children
+- The square root function, $\sqrt{...}$ has 1 child
+- The subtraction ($-$) and multiplication ($\times$) functions have 2 children
+
+The important thing to us is to define a **language** for expressions. This
+way, we know exactly what kinds of expressions we can build. Let's take the
+few operations in the list above and turn it into a **language** for writing
+expressions:
+
+$$
+    e ::= n \mid \sqrt{e} \mid e - e \mid e \times e
+$$
+
+We call these **constructors** of the expression. The notation is a bit dense,
+but this essentially means $e$, which is shorthand for _expression_, is defined
+to be either of ($|$):
+
+- $n$, which is just a convention meaning "any number"
+- $\sqrt{e}$, which means "square root of another expression"
+- $e - e$ and $e \times e$, which correspond to subtraction and multiplication respectively
+
+If you look closely, the number of $e$s in each option corresponds exactly to
+the number of children it had in the expression tree.
+
+Let's write down an expression language for the lambda calculus. In its simplest form, it looks like this:
+
+$$
+    e ::= x \mid \lambda x.e \mid e\; e
+$$
+
+Here, $x$ is a convention that stands for "some variable". Without knowing what any of this means, we can already start putting together some expressions:
+
+- $\lambda x.x$
+- $\lambda s.(\lambda z.(s\; z))$
+
+As an exercise, try drawing some of the expression trees that correspond to
+these expressions. Once you're familiar enough with how expressions are built
+syntactically, we can talk about evaluation.
+
+## Evaluation
+
+The expression language we just defined is typically considered the _statics_ of
+the language. It defines how we can write down the language. What we're going to
+talk about now is the _dynamics_, or how it's evaluated.
+
+<details>
+  <summary>Semantics vs. Implementation</summary>
+
+At this point it's probably a good idea to make a note about _semantics_ vs. _implementation_.
+
+Semantics describe the outcome. If my arithmetic language defines
+multiplication's _semantics_ it would require that multiplication of two numbers
+to achieve another number that has some certain properties, like "repeatedly
+subtracting the first number the same number of times as the second number
+produces 0."
+
+Implementation, on the other hand, needs to conform to the semantics. If I asked
+you to compute $15 \times 16$ by hand, you'd probably bust out some pencil and
+paper and do some long form multiplication, where you'd compute a couple of
+intermediate results and add them, getting $240$.
+
+A computer, on the other hand, notices $16 = 10000_2$, and just shifts $15 =
+0111_2$ over by 4 bits, to get $01110000_2 = 240$. The ways that this same
+result was computed were different, but they achieved the same final result, and
+that result has the property required by the semantics of multiplication.
+
+Just like the example above, the lambda calculus has several different
+implementations of its semantics (for example, the CESK machine or the SECD
+machine). They have a more complex stack structure than a straightforward
+machine implementation in, for example Python, to take. However, we can prove
+that the semantics are the same.
+
+</details>
+
diff --git a/src/content/posts/2024-04-04-test.md b/src/content/posts/2024-04-04-test.md
deleted file mode 100644
index 7a6ae0e..0000000
--- a/src/content/posts/2024-04-04-test.md
+++ /dev/null
@@ -1,36 +0,0 @@
----
-title: test
-date: 2024-04-04T21:45:28.264
-draft: true
-languages: ["typst"]
-tags: ["typst"]
----
-
-```typst
-#import "@preview/fletcher:0.4.3" as fletcher: diagram, node, edge
-#set page(
-  width: auto,
-  height: auto,
-  margin: (x: 0.25em, y: 0.25em),
-)
-#set text(18pt)
-
-#diagram(
-  node-stroke: .1em,
-  node-fill: gradient.radial(blue.lighten(80%), blue, center: (30%, 20%), radius: 80%),
-  spacing: 4em,
-  edge((-1,0), "r", "-|>", `open(path)`, label-pos: 0, label-side: center),
-  node((0,0), `reading`, radius: 2em),
-  edge(`read()`, "-|>"),
-  node((1,0), `eof`, radius: 2em),
-  edge(`close()`, "-|>"),
-  node((2,0), `closed`, radius: 2em, extrude: (-2.5, 0)),
-  edge((0,0), (0,0), `read()`, "--|>", bend: 130deg),
-  edge((0,0), (2,0), `close()`, "-|>", bend: -40deg),
-)
-
-// #diagram(cell-size: 15mm, $
-//   G edge(f, ->) edge("d", pi, ->>) & im(f) \
-//   G slash ker(f) edge("ur", tilde(f), "hook-->")
-// $)
-```