simponic/compiling-the-lambda-calculus
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

add all the stuff

Browse Source
This commit is contained in:
Elizabeth Hunt 2024-02-13 20:00:02 -07:00
parent 512c245466
commit 0c476e92e1
Signed by: simponic
GPG Key ID: 52B3774857EB24B1
53 changed files with 3421 additions and 224 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

151
examples/sum_of_even_squares.ts Normal file
View File

@ -0,0 +1,151 @@
const isEven = (n: number) => {
let even = true; // 0 is even
for (let i = 1; i <= n; i++) {
even = !even;
}
return even;
};
const sumOfEvenSquares = (upTo: number) => {
let sum = 0;
for (let i = 1; i <= upTo; i++) {
if (isEven(i)) {
sum += i * i;
}
}
return sum;
};
/**
* functional
*/
const isEvenHelper = (curr: number, max: number, previous = false) => {
if (curr === max) {
return !previous;
}
return isEvenHelper(curr + 1, max, !previous);
};
const isEvenFn = (n: number) => {
return isEvenHelper(0, n);
};
const map = (
transform: (x: number, ind: number) => number,
list: number[],
index = 0,
) => {
if (list.length === 0) {
return [];
}
const [head, ...tail] = list;
const transformed = transform(head, index);
return [transformed].concat(map(transform, tail, index + 1));
};
const filter = (predicate: (x: number) => boolean, list: number[]) => {
if (list.length === 0) {
return [];
}
const [head, ...tail] = list;
if (predicate(head)) {
return [head].concat(filter(predicate, tail));
}
return filter(predicate, tail);
};
const reduce = (
accumulation: (x: number, accumulator: number) => number,
accumulator: number,
list: number[],
) => {
if (list.length === 0) {
return accumulator;
}
const [head, ...tail] = list;
const newAccumulator = accumulation(head, accumulator);
return reduce(accumulation, newAccumulator, tail);
};
const curriedReduce = (
accumulation: (x: number, accumulator: number) => number,
) => {
return (accumulator: number) => {
const reduce = (list: number[]) => {
if (list.length === 0) {
return accumulator;
}
const [head, ...tail] = list;
const newAccumulator = accumulation(head, accumulator);
return curriedReduce(accumulation)(newAccumulator)(tail);
};
return reduce;
};
};
const sum = curriedReduce((x, acc) => x + acc)(0);
const sumOfEvenSquaresFn = (upTo: number) => {
const numbersUpTo = Array(upTo + 1)
.fill(0)
.map((_, i) => i);
const squares = numbersUpTo.filter((x) => isEvenFn(x)).map((x) => x * x);
return sum(squares);
};
/**
* test
*/
const assert = (predicate: () => boolean, message: string) => {
const start = performance.now();
console.log(message + "...");
const result = predicate();
const runtimeFmt = ` in ${(performance.now() - start).toFixed(5)}ms`;
if (result) {
console.log(" ... PASSED" + runtimeFmt);
return;
}
console.error(" ... FAILED" + runtimeFmt);
throw new Error("predicate failed for test: " + message);
};
/*
Σ(2i)^2 = 4 * Σ(i)^2 = 4 * (n * (n + 1) * (2 * n + 1)) / 6
*/
const constantTimeMathMagic = (x: number) => {
const n = Math.floor(x / 2); // even numbers
return (4 * (n * (n + 1) * (2 * n + 1))) / 6;
};
const test = (sumEvenSquarer: (x: number) => number) => {
assert(() => sumEvenSquarer(5) === 2 ** 2 + 4 ** 2, "up to 5");
assert(
() => sumEvenSquarer(10) === 2 ** 2 + 4 ** 2 + 6 ** 2 + 8 ** 2 + 10 ** 2,
"up to 10",
);
//assert(
// () => sumEvenSquarer(75_000) === constantTimeMathMagic(75_000),
// "up to 75,000",
//);
};
test(sumOfEvenSquares);
test(sumOfEvenSquaresFn);

BIN
public/amogus.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 32 KiB

BIN
public/img/cell_division.mp4 Normal file
View File

Binary file not shown.

BIN
public/img/curry.mp4 Normal file
View File

Binary file not shown.

BIN
public/img/me.jpg
View File

Binary file not shown.
Side by Side

Before

Width:  |  Height:  |  Size: 149 KiB

BIN
public/img/pengy.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 358 KiB

503
script.md
View File

@ -1,18 +1,16 @@
About Me # About Me
===
"For the new faces, I'm Elizabeth, or simponic on the discord..." "For the new faces, I'm Elizabeth, or simponic on the discord..."
- I love functional programming; I've been enjoying programs functionally for over 3 years; in LISP and Elixir mostly. I've loved every second of it. Well, maybe not every second, bust definitely most of them. - I love functional programming; I've been enjoying programs functionally for over 3 years; in LISP and Elixir mostly. I've loved every second of it. Well, maybe not every second, but definitely most of them.
- Soon to be SDE at AWS - Soon to be SDE at AWS
- I'm 20 years old, graduating this semester once I'm done with my final general class I missed on my grad plan (2credits only, ugh, ask me after if you want to hear the bureacracy) - I'm 20 years old, graduating this semester
- I was president of the USU Linux club from 2021 - 2024 - I was president of the USU Linux club from 2021 - 2024
Of course this presentation is open source at the link you see on the board. Of course this presentation is open source at the link you see on the board.
# Flirting With Functions
Flirting With Functions
===
Tomorrow's Valentine's day, but you realize; you don't have a Valentine! Tomorrow's Valentine's day, but you realize; you don't have a Valentine!
Desparate to make yourself feel better, you turn to your computer and open Emacs, asking the M-x doctor for help. Desparate to make yourself feel better, you turn to your computer and open Emacs, asking the M-x doctor for help.
@ -58,13 +56,13 @@ Imagine asking your partner about what food they want to eat. But instead of a s
Let's see what causes this in this black box we don't love; don't pay attention to the implementation (there's some stuff we haven't talked about yet), but check out this line (MATH.RANDOM). This is a side effect; an unpredictible effect on the output. Let's see what causes this in this black box we don't love; don't pay attention to the implementation (there's some stuff we haven't talked about yet), but check out this line (MATH.RANDOM). This is a side effect; an unpredictible effect on the output.
Side effects introduce unpredictability into our programming relationships. Where output is not just determined by its input but also by the state of the outside world, or the system at the time of execution. Suddenly, the predictability we cherished is compromised. Side effects introduce unpredictability into our programming relationships. Where output is not just determined by its input but also by the state of the outside world, or the system at the time of execution. Suddenly, the predictability we cherished is compromised.
We call a function that is unpredictable, or has side effects, "impure", and one that isn't - "pure". We call a function that is unpredictable, or has side effects, "impure", and one that isn't - "pure".
It was obvious how we could cause unpredictability by including randomness. But here's another example, on left we have two impure functions. It was obvious how we could cause unpredictability by including randomness. But here's another example, on left we have two impure functions.
When we execute the first block, we get the expected result of `fib(5)`. When we execute the first block, we get the expected result of `fib(5)`.
But because `fact` uses the same cache, we'll run fact(5)... `fact(5)` returns fib(5)! But because `fact` uses the same cache, we'll run fact(5)... `fact(5)` returns fib(5)!
@ -74,33 +72,10 @@ For now let's move back to studying our pure black boxes.
We love our black boxes a lot, and we want to share them with other people in our lives. So let's create another that takes a list of people and creates a custom valentine's letter for them. We love our black boxes a lot, and we want to share them with other people in our lives. So let's create another that takes a list of people and creates a custom valentine's letter for them.
```python
def make_valentines_letters(people):
letters = []
for person in people:
letters.append(f"Dear, {person.name}\nYour smile lights up my world. Happy Valentine's Day!")
return letters
```
Good! Now they will all share our love. Good! Now they will all share our love.
[SPACE] But a few months goes by, and all our friends' birthdays are soon coming up (why are so many cs people born in June)! We don't want to make them sad, as we see here, so we make another black box to generate a letter, and in how many days we should give it to them: [SPACE] But a few months goes by, and all our friends' birthdays are soon coming up (why are so many cs people born in June)! We don't want to make them sad, as we see here, so we make another black box to generate a letter, and in how many days we should give it to them:
```python
def make_birthday_cards(people):
today = new Date()
cards = []
for person in people:
days_until_birthday = toDays(new Date(person.birthday, today.year) - today)
age = today.year - person.birthday.year
card = f"Happy Birthday {name}\nI can't believe you're already {age} years old!"
cards.append({ "message": card, "deliver_in_days": days_until_birthday })
return cards
```
There, now, we can make sure our friends are happy on their birthdays! There, now, we can make sure our friends are happy on their birthdays!
But, this is getting annoying; what about Christmas, Thanksgiving, or Easter? Making a new black box to make a list of new cards, going through each person, every single time to construct a list of cards, is getting really tedious. But, this is getting annoying; what about Christmas, Thanksgiving, or Easter? Making a new black box to make a list of new cards, going through each person, every single time to construct a list of cards, is getting really tedious.
@ -111,156 +86,404 @@ Then, we can use a new black box that takes a list of people, and applies this t
The ability in a language to pass a function around like this - like a variable - is what makes functions "first class". And the `buildCards` function takes a function as input, making it a "higher order function". The ability in a language to pass a function around like this - like a variable - is what makes functions "first class". And the `buildCards` function takes a function as input, making it a "higher order function".
Functional Reproduction # Functional Reproduction
===
After exploring the simple yet profound beauty of higher order black boxes, our journey into the functional programming romance takes an intriguing turn. What's better than one black box? A black box that creates more black boxes. After exploring the simple yet profound beauty of higher order black boxes, our journey into the functional programming romance takes an intriguing turn. What's better than one black box? A black box that creates more black boxes.
All life on Earth contains instructions in the form of DNA. During mitosis, special mechanisms in our cells read the instructions and create new instructions to give to another cell. All life on Earth contains instructions in the form of DNA. During mitosis, special mechanisms in our cells read the instructions and create new instructions to give to another cell.
Very similarly, we can give our black boxes DNA from parents to reproduce and create new child black boxes. But in our world of black boxes, we refer to this DNA as "closures". Very similarly, we can give our black boxes DNA from parents to reproduce and create new child black boxes. But in our world of black boxes, we refer to this DNA as "closures"; a function with its "environment" - the variables it has access to - attached to it. [SPACE]
``` Here we've created a black box that outputs a black box to create a certain type of letter for a person encoded in its DNA. If the type is "birthday", the output is a birthday card generator, and if it's "valentine", it's a valentine letter generator.
def cardGeneratorFor(person, type):
def personBirthdayCard():
return birthdayCard(person)
def personValentineLetter():
return valentineLetter(person)
if type == "valentine": When we put in "Alan Turing" and "valentine", we obtain a black box with "person" (in this case, Alan Turing) in its DNA [OPEN DEV TOOLS -> valentineCardGenerator]. Now we evaluate the black box, and it returns a valentine letter for that person.
return personValentineLetter
if type == "birthday":
return personBirthdayCard
raise NotImplementedError
joseph = {"name": "Joseph", birthday: new Date()}
josephValentineCardGenerator = cardGenerators(joseph, "valentine")
print(josephValentineCard())
```
Here we've created two children with the DNA of cardGenerators; i.e., we get the "person" from the parent black box's DNA.
We can even go a step further: We can even go a step further:
```
def cardGenerators(person):
def personBirthdayCard():
return birthdayCard(person)
def personValentineLetter():
return valentineLetter(person)
def messageType(type):
if type == "valentine":
return personValentineLetter
if type == "birthday":
return personBirthdayCard
raise NotImplementedError()
return messageType
joseph = {"name": "Joseph", birthday: new Date()}
josephValentineCard = (cardGenerators(joseph))("valentine")
print(josephValentineCards)
```
Wait, do you guys smell that? Wait, do you guys smell that?
Quick Aside: Delicious Curry # Quick Aside: Delicious Curry
===
Sneakily, we've actually started preparing curry! Sneakily, we've actually started preparing curry!
We've broken up the input of the black box ~cardGenerator~ into it and its child. This is called ~currying~, and it's something we'll touch on in more detail later. We've broken up the input of the black box ~cardGenerator~ into a series of functions with a single input. This is called ~currying~.
There's another way that we could implement the same functionality - "partial function application"; a fancy name for a simple idea: To curry the function `cardGeneratorFor` we:
first created a new closure over the person to provide a function that takes only the type
returned that closure
removed the now unnecessary type argument since that's now curried
and finally changed the function signature to reflect the curried function
``` There's another way that we could implement the same functionality - "partial function application"; a fancy name for a simple idea; locking some arguments to partial inputs in a function and passing the rest to be applied.
def josephCard(type):
joseph = {"name": "Joseph", birthday: new Date()}
cardGenerator = cardGeneratorFor(joseph, type)
return cardGenerator()
print(josephCardGenerator("valentine") # Immutability
```
Immutability We briefly mentioned side effects and alluded them to the unpredictability of a partner choosing their food. We love our black boxes because they're reliable. But, we've actually had an impostor among us throughout this presentation.
===
We briefly mentioned side effects and alluded them to the unpredictability of a partner. We love our black boxes because they're reliable.
But, we've actually had an impostor among us (AMOGUS sound??) throughout this presentation. Specifically in `buildCards`: Specifically in `buildCards` [SPACE]
``` This function actually has a small side effect - though it's contained entirely within the function - when we append to the cards list. If we were to go about living a side effect free life, that means we can't change _anything_ lest something else depends on it.
def buildCards(people, cardMaker):
cards = []
for person in people: # side effect (mutation of person)
card = cardMaker(person)
cards.append(card) # side effect (mutation of cards)
# someone could do something nasty with "cards" before it's returned here
return cards
cards = buildCards(people, valentineMaker) In this case, looping through "people" inherently produces a side effect via mutation of the loop variable, so we need to eliminate it.
```
This function actually has a small side effect - though it's contained entirely within the function - when we append to the cards list. If we were to go about living a side effect free life, that means we can't change _anything_.
Loops inherently produce side effects (mutation of the loop variable), so we need to eliminate them.
So how do we sus out an impostor? With copies and recursion. So how do we sus out an impostor? With copies and recursion.
``` Here we're not changing anything at all (except the stack), but we've kept the same functionality; this code is "immutable". When we call `build_cards` on a list of people, we're 100% certain we're not gonna change something and get something odd, short of a bug.
def build_cards(people, card_maker):
if (len(people) == 0): # base case, no more people to process
return []
# get the first person in the list and make their card
person = people[0]
card = card_maker(person)
rest_people = people[1:] # get sublist of everyone except the first
return [card] + build_cards(rest_people, card_maker)
```
Here we're not changing anything at all (except the stack), with the same functionality; this code is "immutable". When we call `build_cards` on a list of people, we're 100% certain we're not gonna get something odd short of a bug. At a high level there are so many benefits to immutable functional programming:
At a high level there are so many benefits to immutability: - Readability and reasoning about code. Functional, immutable code reads like a book!
+ Concurrency (TODO: go into more detail) - Concurrency. When everything is immutable, it's much easier to prevent race conditions and deadlock. If you can avoid a mutex or semaphore here and there, that simplifies things so much. You also know for certain every thread or processor is working on the same data; it couldn't have changed when it was distributed.
+ Easier to verify correctness. - No side effects. I can't think about how many times I've spent hours poring through a code base to find where exactly something is changing or what it can effect. This helps verify correctness and makes unit testing a dream.
+ Compiler optimizations. - I suppose this is more subjective, but it gives you an entirely new view of how computers work. When you work with functions you're directly treating the computer as an automaton or turing machine. There's so much to learn around functional programming, type theory, and it touches almost any given field of mathematics and computer science.
+ Easy to read and understand.
But there are also downsides: But there are also downsides:
+ Keeping immutability requires more computation (data structures)
+ More difficult to write (huge selling point for Object Oriented Programming; encapsulation) - Keeping immutability requires more computation in many cases (special data structures and copying)
- Typical arrays go out the window in most applications. The cons cell / linked list is much preferred. - You also don't typically have mutable datastructures like hash maps. Instead, you need to reach to balanced trees or tries. It takes a lot of practice but you _can_ always write code just as efficiently in terms of time complexity.
- All things considered, to write and learn, it's difficult. The rabbit hole is as deep as your imagination. I haven't even talked about monads or treating code as data (macros); barely even scratched the surface.
But like all relationships, we need to compromise with our black boxes. Side effects are effectively _unavoidable_ as programmers; when people press the button, they don't want the computation to just exist out there in the computer void. No! They want to see the pop up box, and the value updated on their account. We need to be able to mutate state where the tradeoff of extra compute time is unavoidable like in I/O or a relatively large database. But like all relationships, we need to compromise with our black boxes. Side effects are effectively _unavoidable_ as programmers; when people press the button, they don't want the computation to just exist out there in the computer void. No! They want to see the pop up box, and the value updated on their account. We need to be able to mutate state where the tradeoff of extra compute time is unavoidable like in I/O or a relatively large database.
Writing Code Functionally # Writing Code Functionally
===
Determining if a natural number is even or odd in the best way possible is a problem that's stood unsolved since the dawn of time. We'll use this incredibly difficult task to show how we can refactor some code to use the paradigms we just learned.
The best way to learn is by practicing. So we'll spend some time refactoring some code to be more functional and develop some higher order functions and practice currying.
We'll start with a simple example: a function that takes a list of numbers and returns the sum of the squares of the even numbers.
For millenia humans have thought about how best to find if a number is even. So the first function is the _most efficient_ way to do so; we know 0 is even, and then numbers alternatve between even and odd. We could prove this by induction but it's up to the reader.
Then for our `sumOfEvenSquares` we go through all the numbers `upTo` and add its square if it's even.
To make this functional, we first need to keep `isEven` pure and immutable. We can do this again via recursion; 0 is even, so we do the same alternation between even and odd.
For sumOfEvenSquares, we can make some higher order function to filter out the even numbers, and then map over the list to square them, and then reduce to sum them.
```typescript
const isEvenFn = (n: number) => {
if (n === 0) {
return true;
}
return !isEvenFn(n - 1);
};
const map = (
transform: (x: number, ind: number) => number,
list: number[],
index = 0
) => {
if (list.length === 0) {
return [];
}
const [head, ...tail] = list;
const transformed = transform(head, index);
return [transformed].concat(map(transform, tail, index + 1));
};
const filter = (predicate: (x: number) => boolean, list: number[]) => {
if (list.length === 0) {
return [];
}
const [head, ...tail] = list;
if (predicate(head)) {
return [head].concat(filter(predicate, tail));
}
return filter(predicate, tail);
};
const reduce = (
accumulation: (x: number, acc: number) => number,
accumulator: number,
list: number[]
) => {
if (list.length === 0) {
return accumulator;
}
const [head, ...tail] = list;
const newAccumulator = accumulation(head, accumulator);
return reduce(accumulation, newAccumulator, tail);
};
const sumOfEvenSquaresFn = (upTo: number) => {
const numbersUpTo = map((_, i) => i, Array(upTo + 1).fill(0));
const evens = filter((x) => isEvenFn(x), numbersUpTo);
const evensSquared = map((x) => x * x, evens);
return reduce((x, acc) => x + acc, 0, evensSquared);
};
```
And all our tests pass!
We can also use currying to make our code more readable and easier to use; for example, we can curry our reduce function to implement a sum function.
```typescript
const curriedReduce = (accumulation: (x: number, acc: number) => number) => {
return (accumulator: number) => {
const reduce = (list: number[]) => {
if (list.length === 0) {
return accumulator;
}
const [head, ...tail] = list;
const newAccumulator = accumulation(head, accumulator);
return curriedReduce(accumulation)(newAccumulator)(tail);
};
return reduce;
};
};
const sum = curriedReduce((x: number, acc: number) => x + acc)(0);
...
return sum(evensSquared);
...
```
And our tests pass once again! But one of them is commented... hmm... it's pretty big
And, we fail, getting a "maximum call stack size exceeded" error in our incredibly naive recursive implementation of `filter`, `map`, and `reduce`. Thankfully javascript has these builtin, so we'll use those.
```typescript
const sumOfEvenSquaresFn = (upTo: number) => {
const numbersUpTo = Array(upTo + 1)
.fill(0)
.map((_, i) => i);
return numbersUpTo
.filter((x) => isEvenFn(x))
.map((x) => x * x)
.reduce((x, acc) => x + acc, 0);
};
```
There, much shorter. But, we still get the same error. This time in `isEven` at the recursive call.
Now, we're gonna start getting into the weeds. The reason this is happening is because essentially the code is being transformed into:
```typescript
const isEvenFn = (n: number) => {
if (n === 0) {
return true;
}
const isEven = isEvenFn(n - 1);
return !isEven;
};
```
So everytime we check the number previous, we create a whole new stack frame to evaluate `isEvenFn(n-1)` and return control to the callee. Then we evaluate "!isEven" which requires that stack frame.
The runtime I'm using, Bun, uses JavaScriptCore - which supports Tail Call Optimization (which is, sadly, not in the JS spec). What is TCO? Tail Call Optimizations allows us to write recursive functions that overwrite the same stack frame when the last expression evaluated does not leave control of the function.
To do this, we need to ensure that inside of isEvenFn, the last expression evaluated is always `isEvenFn`, not `!isEven`.
It takes a bit of ingenuity, but to do this, we can use an accumulator _inside an argument_ and change the logic up a bit. Here's what I mean:
```typescript
const isEvenHelper = (curr: number, max: number, previous = false) => {
if (curr === max) {
return !previous;
}
return isEvenHelper(curr + 1, !previous);
};
const isEvenFn = (n: number) => {
return isEvenHelper(0, n);
};
```
And there we go! It's passing. But, it's much much slower than the iterative solution. But from my experimentation, Tail Call Optimization won't help us much here since we spend most of our time doing our isEven check in linear time, and we're constantly doing garbage collection whereas our iterative solution has nothing to clean up.
The keen eyed among you might notice that since we can represent the sum of the first $n$ natural number's squares as (n _ (n + 1) _ (2 \* n + 1)) / 6, then transform each natural number to its nearest even entry by scaling by two, and halve the bounds of the sum. Which is constant time. Yeah. But that's not as fun.
======== ========
Part Two - A Deeper Dive # Part Two - Marrying Functions
===
The Lambda Calculus # The Lambda Calculus
===
The Lambda calculus, developed by Alonzo Church in the 1930s, is a "formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution".
Completeness of the Lambda Calculus There are three rules that define the semantics of the Lambda Calculus:
===
Mention how alonzo church actually failed on his first attempt, natural numbers
Writing a Compiler 1. "x": A variable is a character or string representing a parameter, and is a valid lambda term.
=== 2. "(λ x . t)" is an "abstraction" - a function definition, taking as input the bound variable x and returning the lambda term t.
3. (M N) is an "application", applying a lambda term M with a lambda term N.
A Compiler As A Sequence of Transformations There, we're done; the rest is an exercise to the reader. Have a good day everyone! No... I wouldn't be that mean.
===
Continuation Passing Style We can "evaluate" a lambda term by performing three types of reduction:
===
1. α - conversion: Renaming of bound variables to avoid name clashes (out of scope - we're gonna assume user knows not to bind variable names already chosen elsewhere).
2. β - reduction: Application of a function to an argument.
3. η - reduction: Conversion of a function to a point-free form (out of scope).
To perform a β-reduction, we substitute the argument into the body of the function, replacing all instances of the bound variable with the argument.
For example, given the lambda term `(λ x . x) y`, we can do a β-reduction to obtain the value `y` after substituting x. This folllows pretty intuitively, but more formally - we define substitution recursively - given M and N as lambda terms and x,y as variables, as follows:
1. x[x := N] = N
2. y[x := N] = y` if y != x
3. (M N)[x := P] = (M[x := P]) (N[x := P])
4. (λ x . M)[x := N] = λ x . M
5. (λ y . M)[x := N] = λ y . (M[x := N]) if y != x and y is not _free_ in N
A variable is _free_ in a lambda term if it is not bound by a λ abstraction. In other words, a free variable is one that is not a parameter of the function, or in the immediate scope of an abstraction.
# Lambda Calculus as a Computational Model
We encode all computation and values in the lambda calculus as a series of functions and applications. For example, we can encode a natural number n as a function that takes a function f and a value x, and applies f to x n times.
1. `0 = λ f . λ x . x` (no application of f)
2. `1 = λ f . λ x . f x` (one application of f )
3. `2 = λ f . λ x . f (f x)` (two applications of f)
This is called the "Church encoding" of the natural numbers.
We can also define the successor function `succ` as a function that takes a church encoded natural number n, and a function f, and a value x, and performs f on x n times, and then once more.
1. `succ = λ n . λ f . λ x . n f (f x)`
For example, we do an application of `succ` on `0`: `(succ 0) = 1`, and `(succ 1) = 2`.
1. We perform substituion on ,n with the church encoding for 0
2. Substituting g with f has no effect and returns the term (lambda y . y)
3. (lambda y . y) is the identity function.
We're Done! We've constructed 1 from 0. We'll go through the same process to construct 2 from 1.
We can define the boolean values `true` and `false` as functions that take two arguments and return the first and second, respectively.
1. `true = λ x . λ y . x`
2. `false = λ x . λ y . y`
We can then define the logical operators `and`, `or`, and `not` in terms of these boolean values.
1. `and = λ p . λ q . p q false`
2. `or = λ p . λ q . p true q`
3. `not = λ p . p false true`
(a few examples...)
Recursion is also possible in the lambda calculus via the funny-looking thing on the board, which you've probably seen before - the Y combinator. The Y combinator should satisfy the equation `(Y f) = (f (Y f))`, and is defined as follows:
1. `Y = λ f . (λ x . f (x x)) (λ x . f (x x))`
If we let it run by itself, we can see how our recursion works. We can kinda see some formation of a "stack" of sorts.
When we apply the Y combinator to a function, it will apply the function to itself, and then apply the function to itself again, and so on, until the function returns a value.
# Writing a Quick Lambda Calculus Interpreter
I think the best way to learn the lambda calculus is by building an interpreter for it, it's a quick exercise and it's a lot of fun.
When writing a Lambda Calculus interpreter, there are a few decisions to be made:
- [ ] is it the typed or untyped lambda calculus?
- [ ] is the language lazy or strict / eager?
- [ ] call by value or call by name? (call by value - environment, closures)
```
LambdaTerm
= Abstraction
/ Application
/ Variable
Application
= LPAREN _? left:LambdaTerm _? right:LambdaTerm _? RPAREN {
return { left, right };
}
Abstraction
= LPAREN _? LAMBDA _? param:Variable _? DOT _? body:LambdaTerm _? RPAREN {
return { param, body };
}
Variable
= name:([a-z] [A-Z0-9a-z]*) { return { name: name[0] + name[1].join('') }; }
LAMBDA = "λ" / "\"
DOT = "."
LPAREN = "("
RPAREN = ")"
_ = (" " / "\n" / "\t" / "\t\n")+
private substitute(
ast: LambdaTerm,
param: string,
replacement: LambdaTerm
): LambdaTerm {
const node = ast as any;
if (this.isVariable(node)) {
return node.name === param ? replacement : node;
} else if (this.isApplication(node)) {
const left = this.substitute(node.left, param, replacement);
const right = this.substitute(node.right, param, replacement);
return { left, right } as Application;
}
return {
param: node.param,
body: this.substitute(node.body, param, replacement) as Abstraction,
};
}
public fullBetaReduction(ast: LambdaTerm = this.ast): LambdaTerm {
const node = ast as any;
if (this.isApplication(node)) {
const { left, right } = node as Application;
if (this.isAbstraction(left)) {
return this.fullBetaReduction(
this.substitute(left.body, left.param.name, right)
);
}
return {
left: this.fullBetaReduction(left),
right: this.fullBetaReduction(right),
} as Application;
}
if (this.isAbstraction(node)) {
return {
param: node.param,
body: this.fullBetaReduction(node.body),
} as Abstraction;
}
return node;
}
```
There are a lot of bugs in our interpreter; first, there is no alpha conversion, there's a high chance we could have name conflicts within lambda terms. We could use de brujin indexing, but that's outside the scope of this presentation.
# Further
Obviously we've only scratched the surface of the lambda calculus and functional programming; I didn't even mention a lot of things I wanted to get to. So here's a list you can study on your own:
Pattern matching is a fun paradigm and allows one to write much more declarative code.
The lambda calculus is a "universal model of computation", meaning that any computable function can be expressed in the lambda calculus. This is known as the Church-Turing thesis, and is the basis for the theory of computation.
I highly recommend reading the paper "Compilation of Lambda-Calculus into Functional Machine Code". You know how we alluded to the "stack" that the Y combinator produced? This paper goes into how we can utilize that stack to compile lambda calculus into machine code on a stack machine by reversing the order through continuation passing style.
# Extending our interpreter into A Compiler As A Sequence of Transformations
# Continuation Passing Style
======= =======
Conclusion # Conclusions and Comparisons
===

153
src/components/function_box.tsx
View File

@ -72,9 +72,13 @@ export class FunctionBox extends Node {
this.padding = props?.padding ?? 100; this.padding = props?.padding ?? 100;
this.workingText = props?.workingText ?? "👷‍♀️⚙️"; this.workingText = props?.workingText ?? "👷‍♀️⚙️";
this.idlingText = props?.idlingText ?? "😴"; this.idlingText = props?.idlingText ?? "😴";
this.isChild = props?.isChild ?? false; this.isChild = props?.isChild ?? false;
if (this.isChild) {
this.idlingText += " | 🧬";
}
this.outputFontSize = props?.outputFontSize ?? 30; this.outputFontSize = props?.outputFontSize ?? 30;
this.inputFontSize = props?.inputFontSize ?? 30; this.inputFontSize = props?.inputFontSize ?? 30;
@ -82,80 +86,97 @@ export class FunctionBox extends Node {
this.add( this.add(
<Rect <Rect
opacity={this.opacity} opacity={this.opacity}
direction={"row"} direction="column"
alignItems={"center"} alignItems="center"
layout layout
> >
<Rect direction={"column"} alignItems={"end"} gap={10}> <Rect direction="row" alignItems="center">
{range(this.arity).map((i) => ( <Rect
<Rect direction={"row"} alignItems={"center"} gap={10}> direction="column"
<Rect justifyContent="center"
direction={"row"} alignItems="end"
fontSize={0} gap={10}
ref={makeRef(this.inputs, i)} >
justifyContent={"end"} {range(this.arity).map((i) => (
opacity={1} <Rect direction="row" alignItems="center" gap={10}>
></Rect> <Rect
direction="row"
fontSize={0}
ref={makeRef(this.inputs, i)}
justifyContent="end"
opacity={1}
></Rect>
<Line
points={[]}
stroke={theme.green.hex}
ref={makeRef(this.inputSegments, i)}
lineWidth={5}
arrowSize={10}
endArrow
></Line>
</Rect>
))}
</Rect>
<Rect
ref={this.rect}
radius={4}
stroke={theme.overlay0.hex}
fill={theme.crust.hex}
lineWidth={4}
padding={60}
direction="row"
height="100%"
alignItems="center"
>
<Txt
fontFamily={theme.font}
fill={theme.text.hex}
ref={this.boxMoji}
>
{this.idlingText}
</Txt>
<Rect
gap={10}
alignItems="center"
direction="column"
ref={this.node}
opacity={0}
>
<CodeBlock
fontFamily={theme.font}
language="typescript"
ref={this.block}
fontSize={0}
code={this.source}
></CodeBlock>
</Rect>
</Rect>
<Rect
direction="column"
height={"100%"}
alignItems={"end"}
justifyContent="center"
>
<Rect direction="row" alignItems="center" gap={10}>
<Line <Line
points={[]} points={[]}
stroke={theme.green.hex} stroke={theme.red.hex}
ref={makeRef(this.inputSegments, i)}
lineWidth={5} lineWidth={5}
arrowSize={10} arrowSize={10}
ref={this.outputSegment}
endArrow endArrow
></Line> ></Line>
<Rect
direction={"row"}
ref={this.output}
justifyContent={"end"}
opacity={1}
fontSize={0}
></Rect>
</Rect> </Rect>
))}
</Rect>
<Rect
ref={this.rect}
radius={4}
stroke={theme.overlay0.hex}
fill={theme.crust.hex}
lineWidth={4}
padding={60}
direction="row"
height="100%"
alignItems="center"
>
<Txt fontFamily={theme.font} fill={theme.text.hex} ref={this.boxMoji}>
{this.idlingText}
</Txt>
<Node ref={this.node} opacity={0}>
<CodeBlock
fontFamily={theme.font}
language="typescript"
ref={this.block}
fontSize={0}
code={this.source}
></CodeBlock>
</Node>
</Rect>
<Rect
direction="column"
height={"100%"}
alignItems={"end"}
justifyContent="center"
>
<Rect direction="row" alignItems="center" gap={10}>
<Line
points={[]}
stroke={theme.red.hex}
lineWidth={5}
arrowSize={10}
ref={this.outputSegment}
endArrow
></Line>
<Rect
direction={"row"}
ref={this.output}
justifyContent={"end"}
opacity={1}
fontSize={0}
></Rect>
</Rect> </Rect>
</Rect> </Rect>
</Rect>, </Rect>,
@ -252,11 +273,15 @@ export class FunctionBox extends Node {
const output = this.function(...this.currentArgs.map((input) => input.val)); const output = this.function(...this.currentArgs.map((input) => input.val));
switch (typeof output) { switch (typeof output) {
case "function": case "function":
console.dir(output);
yield this.output().add( yield this.output().add(
<FunctionBox <FunctionBox
opacity={0} opacity={0}
isChild={true} isChild={true}
ref={this.child} ref={this.child}
outputFontSize={this.outputFontSize}
inputFontSize={this.inputFontSize}
fn={output} fn={output}
></FunctionBox>, ></FunctionBox>,
); );

188
src/components/lambda_reducer.tsx Normal file
View File

@ -0,0 +1,188 @@
import { Rect, Node, Txt, Line, NodeProps } from "@motion-canvas/2d";
import { createRef, all, range, makeRef, DEFAULT } from "@motion-canvas/core";
import {
CodeBlock,
insert,
edit,
lines,
} from "@motion-canvas/2d/lib/components/CodeBlock";
import { Abstraction, Application, LambdaTerm, parse } from "../parser/parser";
import {
EditOperation,
calculateLevenshteinOperations,
} from "../utils/levenshtein";
export interface LambdaReducerProps extends NodeProps {
lambdaTerm?: string;
definitions?: Record<string, string>;
}
export class LambdaReducer extends Node {
private readonly codeBlock = createRef<CodeBlock>();
private reductions: string[];
private ast: LambdaTerm;
public constructor(props?: LambdaReducerProps) {
super({
...props,
});
const functionDefinitions = props.definitions ?? {};
let lambdaTerm = props.lambdaTerm ?? "((λ x . x) (λ y . y))";
while (
Object.keys(functionDefinitions).some((x) => lambdaTerm.includes(x))
) {
lambdaTerm = Object.entries(functionDefinitions).reduce(
(acc, [name, definition]) => {
return acc.replace(new RegExp(name, "g"), definition);
},
lambdaTerm
);
}
console.log(lambdaTerm);
this.reductions = [props.lambdaTerm, lambdaTerm];
this.ast = parse(lambdaTerm);
this.add(
<CodeBlock
fontSize={25}
ref={this.codeBlock}
language="racket"
code={this.getReductions()}
></CodeBlock>
);
}
private getReductions() {
return this.reductions.filter((x) => x).join("\n=> ");
}
private isApplication(ast: any): boolean {
return ast.left && ast.right;
}
private isAbstraction(ast: any): boolean {
return ast.param && ast.body;
}
private isVariable(ast: any): boolean {
return !!ast.name;
}
private substitute(
ast: LambdaTerm,
param: string,
replacement: LambdaTerm
): LambdaTerm {
const node = ast as any;
if (this.isVariable(node)) {
return node.name === param ? replacement : node;
} else if (this.isApplication(node)) {
const left = this.substitute(node.left, param, replacement);
const right = this.substitute(node.right, param, replacement);
return { left, right } as Application;
}
return {
param: node.param,
body: this.substitute(node.body, param, replacement) as Abstraction,
};
}
public getCode() {
return this.emitCode(this.ast);
}
private betaReduceStep(ast: LambdaTerm): LambdaTerm {
const node = ast as any;
if (this.isApplication(node)) {
const left = node.left as any;
const right = node.right as any;
if (this.isAbstraction(left)) {
return this.substitute(left.body, left.param.name, right);
}
return {
left: this.betaReduceStep(left),
right: this.betaReduceStep(right),
} as Application;
}
if (this.isAbstraction(node)) {
return {
param: node.param,
body: this.betaReduceStep(node.body),
} as Abstraction;
}
return node;
}
private emitCode(ast: LambdaTerm): string {
const node = ast as any;
if (this.isVariable(node)) {
return node.name;
} else if (this.isApplication(node)) {
return `(${this.emitCode(node.left)} ${this.emitCode(node.right)})`;
} else if (this.isAbstraction(node)) {
return `(λ ${node.param.name}.${this.emitCode(node.body)})`;
}
throw new Error("Invalid lambda term");
}
public isDone() {
return (
this.emitCode(this.betaReduceStep(this.ast)) === this.emitCode(this.ast)
);
}
public *step(duration: number) {
yield* this.codeBlock().selection([], 0);
const old = this.getReductions();
const next = this.betaReduceStep(this.ast);
const nextCode = this.emitCode(next);
const operations = calculateLevenshteinOperations(
this.reductions.at(-1),
nextCode
);
yield* this.codeBlock().edit(duration)`${old}${insert(
"\n=> " + this.reductions.at(-1)
)}`;
let code = `this.codeBlock().edit(duration)\`${old}\\n=> `;
// this is SO FUCKING CURSED
window.editInLambda = edit;
window.insertInLambda = insert;
for (const { operation, diff } of operations) {
const next = `'${diff.new ?? ""}'`;
const old = `'${diff.old ?? ""}'`;
if (operation === EditOperation.Edit) {
code += `\${editInLambda(${old}, ${next})}`;
continue;
}
if (operation === EditOperation.Insert) {
code += `\${insertInLambda(${next})}`;
continue;
}
code += diff.new ?? "";
}
code += "`;";
yield* eval(code);
yield* this.codeBlock().selection(lines(this.reductions.length), 0.3);
this.reductions.push(nextCode);
this.ast = next;
}
}

27
src/parser/grammar.pegjs Normal file
View File

@ -0,0 +1,27 @@
LambdaTerm
= Abstraction
/ Application
/ Variable
Application
= LPAREN _? left:LambdaTerm _? right:LambdaTerm _? RPAREN {
return { left, right };
}
Abstraction
= LPAREN _? LAMBDA _? param:Variable _? DOT _? body:LambdaTerm _? RPAREN {
return { param, body };
}
Variable
= name:([a-zA-Z][A-Z0-9a-z]*) { return { name: name[0] + name[1].join('') }; }
LAMBDA = "λ"
DOT = "."
LPAREN = "("
RPAREN = ")"
_ = (" " / "\n" / "\t" / "\t\n")+

1282
src/parser/parser.ts Normal file
View File

File diff suppressed because it is too large Load Diff

4
src/project.meta
View File

@ -3,8 +3,8 @@
"shared": { "shared": {
"background": "rgb(30,30,46)", "background": "rgb(30,30,46)",
"range": [ "range": [
0, 3.5666656666666667,
33.18333233333333 null
], ],
"size": { "size": {
"x": 1920, "x": 1920,

5
src/scenes/boolean_algebra_lambda.meta Normal file
View File

@ -0,0 +1,5 @@
{
"version": 0,
"timeEvents": [],
"seed": 2667185663
}

49
src/scenes/boolean_algebra_lambda.tsx Normal file
View File

@ -0,0 +1,49 @@
import { Layout, makeScene2D } from "@motion-canvas/2d";
import {
Direction,
beginSlide,
createRef,
slideTransition,
} from "@motion-canvas/core";
import { LambdaReducer } from "../components/lambda_reducer";
import { baseDefinitions } from "../utils/lambdas";
export default makeScene2D(function* (view) {
const lambdaReducer = createRef<LambdaReducer>();
const layout = createRef<Layout>();
view.add(
<Layout
layout
ref={layout}
direction="column"
alignItems="center"
gap={50}
></Layout>
);
yield* slideTransition(Direction.Right);
yield* beginSlide("Boolean Reductions");
for (const term of [
"((false one) zero)",
"((true one) zero)",
"(((if true) one) zero)",
]) {
yield* layout().opacity(0, 0.5);
layout().add(
<LambdaReducer
ref={lambdaReducer}
lambdaTerm={term}
definitions={baseDefinitions}
></LambdaReducer>
);
yield* layout().opacity(1, 0.5);
yield* beginSlide("Next Reduction " + term);
for (let i = 0; !lambdaReducer().isDone(); i++) {
yield* lambdaReducer().step(0.5);
yield* beginSlide(term + " Next Step " + i);
}
layout().removeChildren();
}
});

5
src/scenes/boolean_encoding.meta Normal file
View File

@ -0,0 +1,5 @@
{
"version": 0,
"timeEvents": [],
"seed": 2394701117
}

42
src/scenes/boolean_encoding.tsx Normal file
View File

@ -0,0 +1,42 @@
import { Layout, Txt, makeScene2D } from "@motion-canvas/2d";
import {
Direction,
beginSlide,
createRef,
slideTransition,
} from "@motion-canvas/core";
import { theme } from "../theme";
const boolE = [
"true = λ t . λ f . t",
"false = λ t . λ f . f",
"if = λ b . λ x . λ y . b x y",
"not = λ b . b false true",
"and = λ b . λ c . b c false",
];
export default makeScene2D(function* (view) {
const numerals = createRef<Txt>();
view.add(
<Layout layout direction="column" alignItems="center">
<Txt fontSize={40} fontFamily={theme.font} fill={theme.text.hex}>
Boolean Encoding
</Txt>
<Txt
ref={numerals}
fontSize={30}
fontFamily={theme.font}
fill={theme.text.hex}
></Txt>
</Layout>
);
yield* slideTransition(Direction.Right);
yield* beginSlide("The Lambda Calculus - Boolean Encoding");
for (const bool of boolE) {
yield* numerals().text(numerals().text() + "\n\n" + bool, 1);
yield* beginSlide("boolean - " + bool);
}
});

5
src/scenes/church_encoding.meta Normal file
View File

@ -0,0 +1,5 @@
{
"version": 0,
"timeEvents": [],
"seed": 533121975
}

41
src/scenes/church_encoding.tsx Normal file
View File

@ -0,0 +1,41 @@
import { Layout, Txt, makeScene2D } from "@motion-canvas/2d";
import {
Direction,
beginSlide,
createRef,
slideTransition,
} from "@motion-canvas/core";
import { theme } from "../theme";
const churchNumerals = [
"0 = λ f . λ x . x (no application of f)",
"1 = λ f . λ x . f x (one application of f)",
"2 = λ f . λ x . f (f x) (two applications of f)",
"succ = λ n . λ f . λ x . f ((n f) x)",
];
export default makeScene2D(function* (view) {
const numerals = createRef<Txt>();
view.add(
<Layout layout direction="column" alignItems="center">
<Txt fontSize={40} fontFamily={theme.font} fill={theme.text.hex}>
Church Encoding
</Txt>
<Txt
ref={numerals}
fontSize={30}
fontFamily={theme.font}
fill={theme.text.hex}
></Txt>
</Layout>
);
yield* slideTransition(Direction.Right);
yield* beginSlide("The Lambda Calculus - Church Encoding");
for (const numeral of churchNumerals) {
yield* numerals().text(numerals().text() + "\n\n" + numeral, 1);
yield* beginSlide("substitution - " + numeral);
}
});

5
src/scenes/currying.meta Normal file
View File

@ -0,0 +1,5 @@
{
"version": 0,
"timeEvents": [],
"seed": 2262306570
}

114
src/scenes/currying.tsx Normal file
View File

@ -0,0 +1,114 @@
import { Video, Layout, makeScene2D } from "@motion-canvas/2d";
import {
Direction,
all,
beginSlide,
createRef,
slideTransition,
} from "@motion-canvas/core";
import { PEOPLE, Person, PersonI } from "../components/person";
import { birthdayCardFn, valentineCardFn } from "./generalized";
import { CardI } from "./birthday_letters";
import { FunctionBox } from "../components/function_box";
import curry from "../../public/img/curry.mp4";
export const cardGeneratorsFor = (
person: PersonI,
): ((type: string) => () => CardI) => {
const birthdayCardGenerator = () => birthdayCardFn(person);
const valentineCardGenerator = () => valentineCardFn(person);
const messageType = (type: string) => {
switch (type) {
case "valentine":
return valentineCardGenerator;
case "birthday":
return birthdayCardGenerator;
}
throw new Error(type + " not implemented");
};
return messageType;
};
export const cardGeneratorsForSource = `const cardGeneratorsFor = (person: PersonI): ((type: string) => () => CardI) => {
const birthdayCardGenerator = () => birthdayCardFn(person);
const valentineCardGenerator = () => valentineCardFn(person);
const generatorForType = (type: string) => {
switch (type) {
case "valentine":
return valentineCardGenerator;
case "birthday":
return birthdayCardGenerator;
}
throw new Error(type + " not implemented");
};
return generatorForType;
};`;
export default makeScene2D(function* (view) {
const box = createRef<FunctionBox>();
const vid = createRef<Video>();
view.add(
<Layout>
<FunctionBox
ref={box}
fn={cardGeneratorsFor}
source={cardGeneratorsForSource}
outputFontSize={20}
/>
<Video ref={vid} src={curry} width={0} />
</Layout>,
);
yield* all(
box().reset(0.1),
box().showCode(0.5),
slideTransition(Direction.Left, 0.5),
);
yield* beginSlide("show code");
const [alan] = PEOPLE;
yield* box().setInputs([{ val: alan, node: <Person person={alan} /> }], 0.5);
yield* beginSlide("show inputs");
yield* box().hideCode(0.5);
yield* box().propogateInput(0.5);
yield* box().propogateOutput(0.5);
yield* beginSlide("create child function");
const child = box().getChild();
yield* child().showCode(0.5);
yield* beginSlide("show child function");
yield* child().hideCode(0.5);
yield* child().setInputs([{ val: "valentine" }], 0.5);
yield* child().propogateInput(0.5);
yield* child().propogateOutput(0.5);
const curriedChild = child().getChild();
yield* curriedChild().showCode(0.5);
yield* beginSlide("propogate child function");
yield* curriedChild().hideCode(0.5);
yield* curriedChild().setInputs([{ val: "" }], 0.5);
yield* curriedChild().propogateInput(0.5);
yield* curriedChild().propogateOutput(0.5);
yield* beginSlide("propogate curry");
yield vid().play();
yield vid().loop(true);
yield* vid().width(400, 2);
yield* beginSlide("do i smell curry");
});

5
src/scenes/currying_detail.meta Normal file
View File

@ -0,0 +1,5 @@
{
"version": 0,
"timeEvents": [],
"seed": 2012730104
}

155
src/scenes/currying_detail.tsx Normal file
View File

@ -0,0 +1,155 @@
import { Layout, makeScene2D } from "@motion-canvas/2d";
import {
Direction,
beginSlide,
createRef,
slideTransition,
} from "@motion-canvas/core";
import {
CodeBlock,
edit,
insert,
range,
} from "@motion-canvas/2d/lib/components/CodeBlock";
import { cardGeneratorForSource } from "./function_dna";
import { cardGeneratorsForSource } from "./currying";
export default makeScene2D(function* (view) {
const curried = createRef<CodeBlock>();
view.add(
<Layout direction="row" gap={100} layout>
<CodeBlock
fontSize={25}
language="typescript"
ref={curried}
code={cardGeneratorForSource}
/>
</Layout>,
);
yield* slideTransition(Direction.Left);
yield* beginSlide("show function");
yield* curried().edit(
1,
)`const cardGeneratorFor = (person: PersonI, type: string): (() => CardI) => {
const birthdayCardGenerator = () => birthdayCardFn(person); // closure
const valentineCardGenerator = () => valentineCardFn(person); // closure${insert(
"\n",
)}
${insert(`const generatorForType = (type: string) => {`)}
${insert(" ")}switch (type) {
${insert(" ")} case "valentine":
${insert(" ")} return valentineCardGenerator;
${insert(" ")} case "birthday":
${insert(" ")} return birthdayCardGenerator;
${insert(" ")}}
${insert(" ")}throw new Error(type + " not implemented");
${insert("};\n")}}`;
yield* beginSlide("first currying step");
yield* curried().edit(
1,
)`const cardGeneratorFor = (person: PersonI, type: string): (() => CardI) => {
const birthdayCardGenerator = () => birthdayCardFn(person); // closure
const valentineCardGenerator = () => valentineCardFn(person); // closure
const generatorForType = (type: string) => {
switch (type) {
case "valentine":
return valentineCardGenerator;
case "birthday":
return birthdayCardGenerator;
}
throw new Error(type + " not implemented");
};${insert("\n\n return generatorForType;")}
}`;
yield* beginSlide("second currying step");
yield* curried().edit(1)`const ${edit(
"cardGeneratorFor",
"cardGeneratorsFor",
)} = ${edit(
"(person: PersonI, type: string)",
"(person: PersonI)",
)}: (() => CardI) => {
const birthdayCardGenerator = () => birthdayCardFn(person); // closure
const valentineCardGenerator = () => valentineCardFn(person); // closure
const generatorForType = (type: string) => {
switch (type) {
case "valentine":
return valentineCardGenerator;
case "birthday":
return birthdayCardGenerator;
}
throw new Error(type + " not implemented");
};
return generatorForType;
}`;
yield* beginSlide("third currying step");
yield* curried().edit(1)`const cardGeneratorsFor = (person: PersonI): ${edit(
"(() => CardI)",
"((type: string) => () => CardI)",
)} => {
const birthdayCardGenerator = () => birthdayCardFn(person); // closure
const valentineCardGenerator = () => valentineCardFn(person); // closure
const generatorForType = (type: string) => {
switch (type) {
case "valentine":
return valentineCardGenerator;
case "birthday":
return birthdayCardGenerator;
}
throw new Error(type + " not implemented");
};
return generatorForType;
}`;
yield* beginSlide("fourth currying step");
yield* curried().edit(1)`${edit(
cardGeneratorsForSource,
`const alanCardGenerator = (type: string): (() => CardI) => {
const alan: PersonI = {
name: "Alan Turing",
birthday: new Date("06/23/1912"),
color: theme.green.hex,
};
return cardGeneratorFor(alan, type);
};`,
)}`;
yield* beginSlide("partial application");
yield* curried().selection(
[...range(7, 9, 7, 38), ...range(0, 26, 0, 40)],
1,
);
yield* beginSlide("highlight");
yield* curried().edit(
1,
)`const alanCardGenerator = (type: string): (() => CardI) => {
const alan: PersonI = {
name: "Alan Turing",
birthday: new Date("06/23/1912"),
color: theme.green.hex,
};
return cardGeneratorFor(alan, type);
};${insert(`
(alanCardGenerator("valentine")()).message === (cardGeneratorsFor(alan)("valentine")()).message;`)}`;
yield* beginSlide("show application of pa");
});

5
src/scenes/dna.meta Normal file
View File

@ -0,0 +1,5 @@
{
"version": 0,
"timeEvents": [],
"seed": 659686876
}

22
src/scenes/dna.tsx Normal file
View File

@ -0,0 +1,22 @@
import { Video, Layout, makeScene2D } from "@motion-canvas/2d";
import {
Direction,
beginSlide,
createRef,
slideTransition,
} from "@motion-canvas/core";
import mitosis from "../../public/img/cell_division.mp4";
export default makeScene2D(function* (view) {
const layout = createRef<Layout>();
const vid = createRef<Video>();
view.add(
<Video playbackRate={4} width={900} ref={vid} src={mitosis} x={0} />,
);
yield* slideTransition(Direction.Left);
yield vid().play();
yield vid().loop(true);
yield* beginSlide("show mitosis");
});

5
src/scenes/function_dna.meta Normal file
View File

@ -0,0 +1,5 @@
{
"version": 0,
"timeEvents": [],
"seed": 4141071538
}

91
src/scenes/function_dna.tsx Normal file
View File

@ -0,0 +1,91 @@
import { makeScene2D } from "@motion-canvas/2d";
import {
Direction,
all,
beginSlide,
createRef,
slideTransition,
} from "@motion-canvas/core";
import { PEOPLE, Person, PersonI } from "../components/person";
import { birthdayCardFn, valentineCardFn } from "./generalized";
import { CardI } from "./birthday_letters";
import { FunctionBox } from "../components/function_box";
export const cardGeneratorFor = (
person: PersonI,
type: string,
): (() => CardI) => {
const birthdayCardGenerator = () => birthdayCardFn(person);
const valentineCardGenerator = () => valentineCardFn(person);
switch (type) {
case "valentine":
return valentineCardGenerator;
case "birthday":
return birthdayCardGenerator;
}
throw new Error(type + " not implemented");
};
export const cardGeneratorForSource = `const cardGeneratorFor = (person: PersonI, type: string): (() => CardI) => {
const birthdayCardGenerator = () => birthdayCardFn(person); // closure
const valentineCardGenerator = () => valentineCardFn(person); // closure
switch (type) {
case "valentine":
return valentineCardGenerator;
case "birthday":
return birthdayCardGenerator;
}
throw new Error(type + " not implemented");
}`;
export default makeScene2D(function* (view) {
const box = createRef<FunctionBox>();
view.add(
<FunctionBox
arity={2}
ref={box}
fn={cardGeneratorFor}
source={cardGeneratorForSource}
outputFontSize={20}
/>,
);
yield* all(
box().reset(0.1),
box().showCode(0.5),
slideTransition(Direction.Left, 0.5),
);
yield* beginSlide("show code");
const [alan] = PEOPLE;
yield* box().setInputs(
[{ val: alan, node: <Person person={alan} /> }, { val: "valentine" }],
0.5,
);
yield* beginSlide("show inputs");
yield* box().hideCode(0.5);
yield* box().propogateInput(0.5);
yield* box().propogateOutput(0.5);
yield* beginSlide("create child function");
const child = box().getChild();
yield* child().showCode(0.5);
yield* beginSlide("show child function");
yield* child().hideCode(0.5);
yield* child().setInputs([{ val: "" }], 0.5);
yield* child().propogateInput(0.5);
yield* child().propogateOutput(0.5);
yield* beginSlide("propogate child function");
});

5
src/scenes/further.meta Normal file
View File

@ -0,0 +1,5 @@
{
"version": 0,
"timeEvents": [],
"seed": 60068077
}

43
src/scenes/further.tsx Normal file
View File

@ -0,0 +1,43 @@
import { Layout, Txt, makeScene2D } from "@motion-canvas/2d";
import {
Direction,
beginSlide,
createRef,
slideTransition,
} from "@motion-canvas/core";
import { theme } from "../theme";
const goingFurtherLInes = [
"pattern matching",
"the typed lambda calculus",
"church turing thesis",
"lazy vs eager loading, why we use left innermost reduction",
"compiling to machine code & continuation passing style as IR",
"monads",
];
export default makeScene2D(function* (view) {
const lines = createRef<Txt>();
view.add(
<Layout layout direction="column" alignItems="center">
<Txt fontSize={40} fontFamily={theme.font} fill={theme.text.hex}>
Going Further
</Txt>
<Txt
ref={lines}
fontSize={30}
fontFamily={theme.font}
fill={theme.text.hex}
></Txt>
</Layout>
);
yield* slideTransition(Direction.Right);
yield* beginSlide("Going Further");
for (const line of goingFurtherLInes) {
yield* lines().text(lines().text() + "\n\n" + line, 1);
yield* beginSlide("line - " + line);
}
});

6
src/scenes/generalized.tsx
View File

@ -1,4 +1,4 @@
import { Layout, Txt, makeScene2D } from "@motion-canvas/2d"; import { Layout, makeScene2D } from "@motion-canvas/2d";
import { import {
Direction, Direction,
all, all,
@ -11,7 +11,7 @@ import { FunctionBox } from "../components/function_box";
import { PEOPLE, Person, PersonI } from "../components/person"; import { PEOPLE, Person, PersonI } from "../components/person";
import { CardI, daysUntilNextDate } from "./birthday_letters"; import { CardI, daysUntilNextDate } from "./birthday_letters";
const valentineCardFn = (person: PersonI): CardI => { export const valentineCardFn = (person: PersonI): CardI => {
const valentinesDay = new Date("02/14/2024"); const valentinesDay = new Date("02/14/2024");
const message = const message =
`Dear, ${person.name}\n.` + `Dear, ${person.name}\n.` +
@ -21,7 +21,7 @@ const valentineCardFn = (person: PersonI): CardI => {
return { message, deliverInDays }; return { message, deliverInDays };
}; };
const birthdayCardFn = (person: PersonI): CardI => { export const birthdayCardFn = (person: PersonI): CardI => {
const age = new Date().getFullYear() - person.birthday.getFullYear(); const age = new Date().getFullYear() - person.birthday.getFullYear();
const ending = const ending =
({ 1: "st", 2: "nd", 3: "rd" } as Record<number, string>)[ ({ 1: "st", 2: "nd", 3: "rd" } as Record<number, string>)[

5
src/scenes/impostor.meta Normal file
View File

@ -0,0 +1,5 @@
{
"version": 0,
"timeEvents": [],
"seed": 675349706
}

134
src/scenes/impostor.tsx Normal file
View File

@ -0,0 +1,134 @@
import { Img, Layout, makeScene2D } from "@motion-canvas/2d";
import {
Direction,
beginSlide,
createRef,
slideTransition,
all,
} from "@motion-canvas/core";
import {
CodeBlock,
edit,
insert,
lines,
} from "@motion-canvas/2d/lib/components/CodeBlock";
import amogusSus from "../../public/amogus.png";
const cardBuilder = `const buildCards = (
people: PersonI[],
cardGenerator: (person: PersonI) => CardI,
): CardI[] => {
const cards: CardI[] = [];
for (const person of people) {
const card = cardGenerator(person);
cards.push(card);
}
return cards;
};`;
export default makeScene2D(function* (view) {
const layout = createRef<Layout>();
const buildCards = createRef<CodeBlock>();
const amogus = createRef<Img>();
view.add(
<Layout ref={layout} layout direction="row" gap={0}>
<CodeBlock
fontSize={25}
language="typescript"
ref={buildCards}
code={cardBuilder}
/>
<Img ref={amogus} src={amogusSus} opacity={0} width={0} height={0} />
</Layout>,
);
yield* slideTransition(Direction.Right);
yield* beginSlide("show buildCards");
yield* buildCards().selection([...lines(6), ...lines(8)], 0.75);
yield* all(
amogus().width(300, 0.5),
amogus().height(400, 0.5),
amogus().opacity(1, 0.5),
layout().gap(100, 0.5),
);
yield* beginSlide("show side effects");
yield* all(
buildCards().edit(1.2)`const buildCards = (
people: PersonI[],
cardGenerator: (person: PersonI) => CardI,
): CardI[] => {${insert(`
if (people.length === 0) {
return [];
}
`)}
const cards: CardI[] = [];
for (const person of people) {
const card = cardGenerator(person);
cards.push(card);
}
return cards;
};`,
amogus().width(0, 0.3),
amogus().height(0, 0.3),
layout().gap(0, 0.3),
);
yield* beginSlide("base case");
yield* buildCards().edit(1.2)`const buildCards = (
people: PersonI[],
cardGenerator: (person: PersonI) => CardI,
): CardI[] => {
if (people.length === 0) {
return [];
}
${edit(
"const cards: CardI[] = [];",
`const person = people[0];
const card = cardGenerator(person);`,
)}
for (const person of people) {
const card = cardGenerator(person);
cards.push(card);
}
return cards;
};`;
yield* beginSlide("first card");
yield* buildCards().edit(1.2)`const buildCards = (
people: PersonI[],
cardGenerator: (person: PersonI) => CardI,
): CardI[] => {
if (people.length === 0) {
return [];
}
const person = people[0];
const card = cardGenerator(person);
${edit(
`for (const person of people) {
const card = cardGenerator(person);
cards.push(card);
}`,
`const restPeople = people.slice(1);
const cards = [card].concat(buildCards(restPeople, cardGenerator));`,
)}
return cards;
};`;
yield* beginSlide("recursion");
});

58
src/scenes/index.ts
View File

@ -10,18 +10,54 @@ import valentines_letters from "./valentines_letters?scene";
import birthday_letters from "./birthday_letters?scene"; import birthday_letters from "./birthday_letters?scene";
import sad_people from "./sad_people?scene"; import sad_people from "./sad_people?scene";
import generalized from "./generalized?scene"; import generalized from "./generalized?scene";
import dna from "./dna?scene";
import function_dna from "./function_dna?scene";
import currying from "./currying?scene";
import currying_detail from "./currying_detail?scene";
import impostor from "./impostor?scene";
import pros_cons from "./pros_cons?scene";
import parttwo from "./parttwo?scene";
import the_lambda_calculus from "./the_lambda_calculus?scene";
import reductions from "./reductions?scene";
import substitution from "./substitution?scene";
import lambda_reduction_example from "./lambda_reduction_example?scene";
import church_encoding from "./church_encoding?scene";
import boolean_algebra_lambda from "./boolean_algebra_lambda?scene";
import boolean_encoding from "./boolean_encoding?scene";
import recursion from "./recursion?scene";
import lambda_recursion from "./lambda_recursion?scene";
import further from "./further?scene";
import questions from "./questions?scene";
export const scenes = [ export const scenes = [
//title, title,
//me, me,
//partone, partone,
//flirtingwithfunctions, flirtingwithfunctions,
//doctor, doctor,
//first_box, first_box,
//hungry_partner, hungry_partner,
//pure_functions, pure_functions,
//valentines_letters, valentines_letters,
//sad_people, sad_people,
//birthday_letters, birthday_letters,
generalized, generalized,
dna,
function_dna,
currying,
currying_detail,
impostor,
pros_cons,
parttwo,
the_lambda_calculus,
reductions,
substitution,
church_encoding,
lambda_reduction_example,
boolean_encoding,
boolean_algebra_lambda,
recursion,
lambda_recursion,
further,
questions,
]; ];

5
src/scenes/lambda_recursion.meta Normal file
View File

@ -0,0 +1,5 @@
{
"version": 0,
"timeEvents": [],
"seed": 1988478153
}

45
src/scenes/lambda_recursion.tsx Normal file
View File

@ -0,0 +1,45 @@
import { Layout, makeScene2D } from "@motion-canvas/2d";
import {
Direction,
beginSlide,
createRef,
slideTransition,
} from "@motion-canvas/core";
import { LambdaReducer } from "../components/lambda_reducer";
import { baseDefinitions } from "../utils/lambdas";
export default makeScene2D(function* (view) {
const lambdaReducer = createRef<LambdaReducer>();
const layout = createRef<Layout>();
view.add(
<Layout
layout
ref={layout}
direction="column"
alignItems="center"
gap={50}
></Layout>,
);
yield* slideTransition(Direction.Right);
yield* beginSlide("Boolean Reductions");
for (const term of ["Y", "(Y (λ y . y))"]) {
yield* layout().opacity(0, 0.5);
layout().add(
<LambdaReducer
ref={lambdaReducer}
lambdaTerm={term}
definitions={baseDefinitions}
></LambdaReducer>,
);
yield* layout().opacity(1, 0.5);
yield* beginSlide("Next Reduction " + term);
for (let i = 0; i < 6; i++) {
yield* lambdaReducer().step(0.5);
yield* beginSlide(term + " Next Step " + i);
}
layout().removeChildren();
}
});

5
src/scenes/lambda_reduction_example.meta Normal file
View File

@ -0,0 +1,5 @@
{
"version": 0,
"timeEvents": [],
"seed": 2126031881
}

47
src/scenes/lambda_reduction_example.tsx Normal file
View File

@ -0,0 +1,47 @@
import { Layout, makeScene2D } from "@motion-canvas/2d";
import {
Direction,
beginSlide,
createRef,
slideTransition,
} from "@motion-canvas/core";
import { LambdaReducer } from "../components/lambda_reducer";
import { baseDefinitions } from "../utils/lambdas";
export default makeScene2D(function* (view) {
const lambdaReducer = createRef<LambdaReducer>();
const layout = createRef<Layout>();
view.add(
<Layout layout ref={layout} direction="column" alignItems="center" gap={50}>
<LambdaReducer
ref={lambdaReducer}
lambdaTerm={"(succ zero)"}
definitions={baseDefinitions}
></LambdaReducer>
</Layout>
);
yield* slideTransition(Direction.Right);
yield* beginSlide("Example Reductions");
for (let i = 0; !lambdaReducer().isDone(); i++) {
yield* lambdaReducer().step(0.5);
yield* beginSlide("1 Next Step " + i);
}
const one = lambdaReducer().getCode();
const reduceToTwo = createRef<LambdaReducer>();
layout().add(
<LambdaReducer
ref={reduceToTwo}
lambdaTerm={`(succ ${one})`}
definitions={baseDefinitions}
></LambdaReducer>
);
for (let i = 0; !reduceToTwo().isDone(); i++) {
yield* reduceToTwo().step(0.5);
yield* beginSlide("2 Next Step " + i);
}
});

8
src/scenes/me.tsx
View File

@ -1,7 +1,7 @@
import { Node, Img, Txt, Layout, makeScene2D } from "@motion-canvas/2d"; import { Node, Img, Txt, Layout, makeScene2D } from "@motion-canvas/2d";
import { beginSlide, createRef, all } from "@motion-canvas/core"; import { beginSlide, createRef, all } from "@motion-canvas/core";
import me from "../../public/img/me.jpg"; import pengy from "../../public/img/pengy.png";
import { theme } from "../theme"; import { theme } from "../theme";
export default makeScene2D(function* (view) { export default makeScene2D(function* (view) {
@ -41,11 +41,11 @@ export default makeScene2D(function* (view) {
</Txt> </Txt>
</Node> </Node>
</Layout> </Layout>
<Img y={-10} ref={img} src={me} width={10} alpha={0} radius={20} />{" "} <Img y={-10} ref={img} src={pengy} width={10} alpha={0} radius={20} />{" "}
<Txt opacity={0} ref={src} fontFamily={theme.font} fill={theme.green.hex}> <Txt opacity={0} ref={src} fontFamily={theme.font} fill={theme.green.hex}>
git.simponic.xyz/simponic/compiling-the-lambda-calculus git.simponic.xyz/simponic/compiling-the-lambda-calculus
</Txt> </Txt>
</>, </>
); );
yield img().fill(img().getColorAtPoint(0)); yield img().fill(img().getColorAtPoint(0));
@ -59,7 +59,7 @@ export default makeScene2D(function* (view) {
node().opacity(1, 1), node().opacity(1, 1),
layout().position.x(diff, 1), layout().position.x(diff, 1),
src().opacity(1, 1), src().opacity(1, 1),
src().position.y(290, 1), src().position.y(290, 1)
); );
yield* beginSlide("About Me"); yield* beginSlide("About Me");

5
src/scenes/parttwo.meta Normal file
View File

@ -0,0 +1,5 @@
{
"version": 0,
"timeEvents": [],
"seed": 2908089933
}

16
src/scenes/parttwo.tsx Normal file
View File

@ -0,0 +1,16 @@
import { Layout, Txt, makeScene2D } from "@motion-canvas/2d";
import { Direction, beginSlide, slideTransition } from "@motion-canvas/core";
import { theme } from "../theme";
export default makeScene2D(function* (view) {
yield view.add(
<Layout layout direction="column" alignItems="center">
<Txt fontFamily={theme.font} fontSize={100} fill={theme.text.hex}>
Part Two
</Txt>
</Layout>
);
yield* slideTransition(Direction.Right);
yield* beginSlide("Part Two");
});

5
src/scenes/pros_cons.meta Normal file
View File

@ -0,0 +1,5 @@
{
"version": 0,
"timeEvents": [],
"seed": 3275339858
}

61
src/scenes/pros_cons.tsx Normal file
View File

@ -0,0 +1,61 @@
import { Img, Layout, Txt, makeScene2D } from "@motion-canvas/2d";
import {
Direction,
beginSlide,
createRef,
slideTransition,
} from "@motion-canvas/core";
import { theme } from "../theme";
const PROS = [
"readbility, reasoning",
"concurrency",
"no side effects",
"computers and math!",
];
const CONS = ["more computation", "higher learning curve"];
export default makeScene2D(function* (view) {
const pros = createRef<Txt>();
const cons = createRef<Txt>();
view.add(
<Layout direction="row" justifyContent="center" gap={300} layout>
<Layout direction="column" justifyContent="end">
<Txt fontSize={30} fontFamily={theme.font} fill={theme.green.hex}>
PROS :)
</Txt>
<Txt
ref={pros}
fontSize={30}
fontFamily={theme.font}
fill={theme.text.hex}
></Txt>
</Layout>
<Layout direction="column" justifyContent="start">
<Txt fontSize={30} fontFamily={theme.font} fill={theme.red.hex}>
CONS :(
</Txt>
<Txt
ref={cons}
fontSize={30}
fontFamily={theme.font}
fill={theme.text.hex}
></Txt>
</Layout>
</Layout>,
);
yield* slideTransition(Direction.Right);
yield* beginSlide("layout pros and cons");
for (const pro of PROS) {
yield* pros().text(pros().text() + "\n\n+ " + pro, 0.5);
yield* beginSlide("pro - " + pro);
}
for (const con of CONS) {
yield* cons().text(cons().text() + "\n\n- " + con, 0.5);
yield* beginSlide("con - " + con);
}
});

5
src/scenes/questions.meta Normal file
View File

@ -0,0 +1,5 @@
{
"version": 0,
"timeEvents": [],
"seed": 3904825059
}

16
src/scenes/questions.tsx Normal file
View File

@ -0,0 +1,16 @@
import { Layout, Txt, makeScene2D } from "@motion-canvas/2d";
import { Direction, beginSlide, slideTransition } from "@motion-canvas/core";
import { theme } from "../theme";
export default makeScene2D(function* (view) {
view.add(
<Layout layout direction="column" alignItems="center">
<Txt fontSize={40} fontFamily={theme.font} fill={theme.text.hex}>
Questions?
</Txt>
</Layout>
);
yield* slideTransition(Direction.Right);
yield* beginSlide("Questions");
});

5
src/scenes/recursion.meta Normal file
View File

@ -0,0 +1,5 @@
{
"version": 0,
"timeEvents": [],
"seed": 693500437
}

36
src/scenes/recursion.tsx Normal file
View File

@ -0,0 +1,36 @@
import { Layout, Txt, makeScene2D } from "@motion-canvas/2d";
import {
Direction,
beginSlide,
createRef,
slideTransition,
} from "@motion-canvas/core";
import { theme } from "../theme";
const recursion = ["Y = λ f . (λ x . f (x x)) (λ x . f (x x))"];
export default makeScene2D(function* (view) {
const lines = createRef<Txt>();
view.add(
<Layout layout direction="column" alignItems="center">
<Txt fontSize={40} fontFamily={theme.font} fill={theme.text.hex}>
Recursion and Combinators
</Txt>
<Txt
ref={lines}
fontSize={30}
fontFamily={theme.font}
fill={theme.text.hex}
></Txt>
</Layout>
);
yield* slideTransition(Direction.Right);
yield* beginSlide("The Lambda Calculus - Church Encoding");
for (const line of recursion) {
yield* lines().text(lines().text() + "\n\n" + line, 1);
yield* beginSlide("recursion - " + line);
}
});

5
src/scenes/reductions.meta Normal file
View File

@ -0,0 +1,5 @@
{
"version": 0,
"timeEvents": [],
"seed": 2906227318
}

40
src/scenes/reductions.tsx Normal file
View File

@ -0,0 +1,40 @@
import { Layout, Txt, makeScene2D } from "@motion-canvas/2d";
import {
Direction,
beginSlide,
createRef,
slideTransition,
} from "@motion-canvas/core";
import { theme } from "../theme";
const reductions = [
"1. α - conversion: Renaming of bound variables to avoid name clashes (out of\nscope - assume user knows not to bind variable names already chosen elsewhere).",
"2. β - reduction: Application of a function to an argument.",
"3. η - reduction: Conversion of a function to a point-free form (out of scope).",
];
export default makeScene2D(function* (view) {
const rules = createRef<Txt>();
view.add(
<Layout layout direction="column" alignItems="center">
<Txt fontSize={40} fontFamily={theme.font} fill={theme.text.hex}>
The Lambda Calculus - Reductions
</Txt>
<Txt
ref={rules}
fontSize={30}
fontFamily={theme.font}
fill={theme.text.hex}
></Txt>
</Layout>
);
yield* slideTransition(Direction.Right);
yield* beginSlide("The Lambda Calculus - Reductions");
for (const rule of reductions) {
yield* rules().text(rules().text() + "\n\n" + rule, 1);
yield* beginSlide("reduction - " + rule);
}
});

5
src/scenes/substitution.meta Normal file
View File

@ -0,0 +1,5 @@
{
"version": 0,
"timeEvents": [],
"seed": 3113568447
}

45
src/scenes/substitution.tsx Normal file
View File

@ -0,0 +1,45 @@
import { Layout, Txt, makeScene2D } from "@motion-canvas/2d";
import {
Direction,
beginSlide,
createRef,
slideTransition,
} from "@motion-canvas/core";
import { theme } from "../theme";
const substitution = [
"β-reduce [ (λ x . x) y ] => y\n\n",
"Formal definition:",
"1. x[x := N] = N",
"2. y[x := N] = y if y != x",
"3. (M N)[x := P] = (M[x := P]) (N[x := P])",
"4. (λ x . M)[x := N] = λ x . M",
"5. (λ y . M)[x := N] = λ y . (M[x := N]) if y != x and y is not _free_ in N",
" +=> A variable is _free_ in a lambda term if it is not bound by a λ abstraction.",
];
export default makeScene2D(function* (view) {
const rules = createRef<Txt>();
view.add(
<Layout layout direction="column" alignItems="center">
<Txt fontSize={40} fontFamily={theme.font} fill={theme.text.hex}>
The Lambda Calculus - Substitution Rules
</Txt>
<Txt
ref={rules}
fontSize={30}
fontFamily={theme.font}
fill={theme.text.hex}
></Txt>
</Layout>
);
yield* slideTransition(Direction.Right);
yield* beginSlide("The Lambda Calculus - Substitutions");
for (const rule of substitution) {
yield* rules().text(rules().text() + "\n\n" + rule, 1);
yield* beginSlide("substitution - " + rule);
}
});

5
src/scenes/the_lambda_calculus.meta Normal file
View File

@ -0,0 +1,5 @@
{
"version": 0,
"timeEvents": [],
"seed": 561758562
}

40
src/scenes/the_lambda_calculus.tsx Normal file
View File

@ -0,0 +1,40 @@
import { Layout, Txt, makeScene2D } from "@motion-canvas/2d";
import {
Direction,
beginSlide,
createRef,
slideTransition,
} from "@motion-canvas/core";
import { theme } from "../theme";
const lambdaRules = [
'1. "x": A variable is a character or string representing a parameter, and is a valid lambda term.',
'2. "(λ x . t)" is an "abstraction" - a function definition, taking as input the \nbound variable x and returning the lambda term t.',
'3. (M N) is an "application", applying a lambda term M with a lambda term N.',
];
export default makeScene2D(function* (view) {
const rules = createRef<Txt>();
view.add(
<Layout layout direction="column" alignItems="center">
<Txt fontSize={40} fontFamily={theme.font} fill={theme.text.hex}>
The Lambda Calculus
</Txt>
<Txt
ref={rules}
fontSize={30}
fontFamily={theme.font}
fill={theme.text.hex}
></Txt>
</Layout>
);
yield* slideTransition(Direction.Right);
yield* beginSlide("The Lambda Calculus");
for (const rule of lambdaRules) {
yield* rules().text(rules().text() + "\n\n" + rule, 1);
yield* beginSlide("rule - " + rule);
}
});

35
src/utils/lambdas.ts Normal file
View File

@ -0,0 +1,35 @@
const succ = "(λ n.(λ f.(λ x.(f ((n f) x)))))";
const zero = "(λ g.(λ y.y))";
const one = "(λ g.(λ y.(g y)))";
const two = "(λ g.(λ y.(g (g y))))";
const three = "(λ g.(λ y.(g (g (g y)))))";
const four = "(λ g.(λ y.(g (g (g (g y))))))";
const five = "(λ g.(λ y.(g (g (g (g (g y)))))))";
const mult = "(λ m.(λ n.(λ f.(m (n f)))))";
const trueL = "(λ a.(λ b.a))";
const falseL = "(λ a.(λ b.b))";
const ifL = "(λ b.(λ n.(λ m.((b n) m))))";
const iszero = "(λ num.((num (λ x.false)) true))";
const not = "(λ b.((b false) true))";
const and = "(λ b.(λ c.((b c) false)))";
const or = "(λ b.(λ c.((b true) c)))";
const Y = "(λ h.((λ z.(h (z z))) (λ z.(h (z z)))))";
export const baseDefinitions = {
iszero,
succ,
zero,
one,
two,
three,
four,
five,
mult,
true: trueL,
false: falseL,
if: ifL,
not,
and,
or,
Y,
};

103
src/utils/levenshtein.ts Normal file
View File

@ -0,0 +1,103 @@
export enum EditOperation {
Insert = "insert",
Delete = "delete",
Edit = "edit",
None = "none",
}
interface Diff {
old: string;
new: string;
}
interface Edit {
operation: EditOperation;
diff: Diff;
}
export const calculateLevenshteinOperations = (
str1: string,
str2: string
): Edit[] => {
const len1 = str1.length;
const len2 = str2.length;
const dp: number[][] = Array.from({ length: len1 + 1 }, () =>
Array(len2 + 1).fill(0)
);
// Initialize DP table
for (let i = 0; i <= len1; i++) dp[i][0] = i;
for (let j = 0; j <= len2; j++) dp[0][j] = j;
// Fill DP table
for (let i = 1; i <= len1; i++) {
for (let j = 1; j <= len2; j++) {
const cost = str1[i - 1] === str2[j - 1] ? 0 : 1;
dp[i][j] = Math.min(
dp[i - 1][j] + 1, // Deletion
dp[i][j - 1] + 1, // Insertion
dp[i - 1][j - 1] + cost // Substitution (Edit)
);
}
}
// Backtrack to find operations
let operations: Edit[] = [];
let i = len1,
j = len2;
while (i > 0 || j > 0) {
if (
i > 0 &&
j > 0 &&
dp[i][j] === dp[i - 1][j - 1] &&
str1[i - 1] === str2[j - 1]
) {
// No operation needed
operations.unshift({
operation: EditOperation.None,
diff: { old: str1[i - 1], new: str2[j - 1] },
});
i--;
j--;
} else if (i > 0 && dp[i][j] === dp[i - 1][j] + 1) {
// Delete operation
operations.unshift({
operation: EditOperation.Delete,
diff: { old: str1[i - 1], new: "" },
});
i--;
} else if (j > 0 && dp[i][j] === dp[i][j - 1] + 1) {
// Insert operation
operations.unshift({
operation: EditOperation.Insert,
diff: { old: "", new: str2[j - 1] },
});
j--;
} else if (i > 0 && j > 0) {
// Edit operation
operations.unshift({
operation: EditOperation.Edit,
diff: { old: str1[i - 1], new: str2[j - 1] },
});
i--;
j--;
}
}
// Simplify consecutive "none" operations into single operations
const simplifiedOperations = operations.reduce<Edit[]>((acc, op) => {
if (
acc.length > 0 &&
op.operation === EditOperation.None &&
acc[acc.length - 1].operation === EditOperation.None
) {
acc[acc.length - 1].diff.old += op.diff.old;
acc[acc.length - 1].diff.new += op.diff.new;
} else {
acc.push(op);
}
return acc;
}, []);
return simplifiedOperations;
};