1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
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);
}
});
|
