From a73c219b534918e1829ab50eac4cbeb813dc6ff2 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sat, 15 Jun 2024 12:20:06 -0600 Subject: [PATCH] Notes on alpha-conversion and beta-reduction. --- .../plugins/obsidian-to-anki-plugin/data.json | 5 +- notes/_journal/2024-06-15.md | 3 +- notes/lambda-calculus/alpha-conversion.md | 92 +++++++++- notes/lambda-calculus/beta-reduction.md | 172 ++++++++++++++++++ 4 files changed, 268 insertions(+), 4 deletions(-) create mode 100644 notes/lambda-calculus/beta-reduction.md diff --git a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json index 04a38d1..3b0a83f 100644 --- a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json +++ b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json @@ -512,7 +512,7 @@ "_journal/2024-06/2024-06-06.md": "db3407dcc86fa759b061246ec9fbd381", "_journal/2024-06-08.md": "b20d39dab30b4e12559a831ab8d2f9b8", "_journal/2024-06/2024-06-07.md": "c6bfc4c1e5913d23ea7828a23340e7d3", - "lambda-calculus/alpha-conversion.md": "9965a24624a745af16f10d9ffd78cc0c", + "lambda-calculus/alpha-conversion.md": "d3a10cb834e696909b04611c83f738cb", "lambda-calculus/index.md": "756c93b8717fd00b04f8a99509066486", "x86-64/instructions/condition-codes.md": "56ad6eb395153609a1ec51835925e8c9", "x86-64/instructions/logical.md": "818428b9ef84753920dc61e5c2de9199", @@ -535,7 +535,8 @@ "_journal/2024-06/2024-06-13.md": "e2722a00585d94794a089e8035e05728", "set/functions.md": "34bf35a8ae16a0d735ce7e3e1b5bfa05", "_journal/2024-06-15.md": "92cb8dc5c98e10832fb70c0e3ab3cec4", - "_journal/2024-06/2024-06-14.md": "5d12bc272238ac985a1d35d3d63ea307" + "_journal/2024-06/2024-06-14.md": "5d12bc272238ac985a1d35d3d63ea307", + "lambda-calculus/beta-reduction.md": "aa1b302755cde85085abedbde85161df" }, "fields_dict": { "Basic": [ diff --git a/notes/_journal/2024-06-15.md b/notes/_journal/2024-06-15.md index b9970e9..fad9788 100644 --- a/notes/_journal/2024-06-15.md +++ b/notes/_journal/2024-06-15.md @@ -8,4 +8,5 @@ title: "2024-06-15" - [ ] Sheet Music (10 min.) - [ ] Korean (Read 1 Story) -* [[functions|Notes]] on injections, surjections, and bijections. \ No newline at end of file +* [[functions|Notes]] on injections, surjections, and bijections. +* Start defining [[beta-reduction|β-reduction]]. \ No newline at end of file diff --git a/notes/lambda-calculus/alpha-conversion.md b/notes/lambda-calculus/alpha-conversion.md index 03f7b5c..b61fe8b 100644 --- a/notes/lambda-calculus/alpha-conversion.md +++ b/notes/lambda-calculus/alpha-conversion.md @@ -20,6 +20,14 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi END%% +%%ANKI +Basic +What two ways can we pronounce $P \equiv_\alpha Q$? +Back: "$P$ is congruent to $Q$" and "$P$ $\alpha$-converts to $Q$". +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + %%ANKI Basic If $P \equiv_\alpha Q$, does $P \equiv Q$? @@ -28,6 +36,22 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi END%% +%%ANKI +Basic +What does an $\alpha$-conversion refer to? +Back: The act of replacing an occurrence of $(\lambda x. M)$ with $\lambda y. [y/x]M$. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +What distinguishes terms "$\alpha$-conversion" and "$\alpha$-converts"? +Back: The latter refers to 0 or more applications of the former. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + %%ANKI Basic $\alpha$-conversion is most related to what kind of $\lambda$-term? @@ -44,6 +68,20 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi END%% +%%ANKI +Cloze +"$\alpha$-{conversion}" refers to exactly one change of bound variable. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Cloze +"$\alpha$-{converts}" refers to zero or more change of bound variables. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + %%ANKI Basic What *kind* of conversion is a change of bound variable? @@ -102,11 +140,19 @@ END%% %%ANKI Cloze -$\alpha$-conversion is known as a change of {bound variables}. +$\alpha$-conversion is known as a change of {bound variable}. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). END%% +%%ANKI +Basic +What greek-prefixed term is a change of bound variable known as? +Back: An $\alpha$-conversion. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + %%ANKI Basic If $P \equiv_\alpha Q$, what can be said about the free variables of $P$ and $Q$? @@ -384,6 +430,50 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi END%% +## Simultaneous Substitution + +Substitution can be generalized in the natural way to define simultaneous substitution $$[N_1/x_1, N_2/x_2, \ldots, N_n/x_n]M$$ for $n \geq 2$. As in [[equiv-trans#Substitution|equivalence-transformation]], simultaneous substitution is different from sequential substitution. + +%%ANKI +Basic +How is simultaneous substitution of $N_1$ for $x_1$ and $N_2$ for $x_2$ in $M$ denoted? +Back: $[N_1/x_1, N_2/x]M$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +How is $[N_1/x_1, N_2/x_2]M$ denoted in the equivalence-transformation system? +Back: $M_{N_1, N_2}^{x_1, x_2}$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +How is $M_{N_1, N_2}^{x_1, x_2}$ denoted in $\lambda$-calculus? +Back: $[N_1/x_1, N_2/x_2]M$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +Suppose $M \equiv x_1x_2$. What is the result of $[u/x_1]([x_1/x_2]M)$? +Back: $uu$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +Suppose $M \equiv x_1x_2$. What is the result of $[u/x_1, x_1/x_2]M$? +Back: $ux_1$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + ## Bibliography * Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). \ No newline at end of file diff --git a/notes/lambda-calculus/beta-reduction.md b/notes/lambda-calculus/beta-reduction.md new file mode 100644 index 0000000..d901b82 --- /dev/null +++ b/notes/lambda-calculus/beta-reduction.md @@ -0,0 +1,172 @@ +--- +title: β-reduction +TARGET DECK: Obsidian::STEM +FILE TAGS: λ-calculus +tags: + - λ-calculus +--- + +## Overview + +Any term of form $(\lambda x. M)N$ is called a **$\beta$-redex**. The corresponding term $[N/x]M$ is its **contractum**. If and only if a term $P$ contains an occurrence of $(\lambda x. M)N$ and we replace that occurrence by $[N/x]M$, and the result is $P'$, we say we have **contracted** the redex-occurrence in $P$, and $P$ $\beta$-contracts to $P'$ or $P \,\triangleright_{1\beta}\, P'$. + +If and only if $P$ can be changed to a term $Q$ by a finite series of $\beta$-contractions and changes of bound variables, we say $P$ $\beta$-reduces to $Q$, or $P \,\triangleright_{\beta}\, Q$. + +%%ANKI +Cloze +$\alpha$-{converts} is to $\beta$-{reduces}. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Cloze +$\alpha$-{conversion} is to $\beta$-{contraction}. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Cloze +"$\beta$-{contracts}" refers to exactly one contraction of a redex-occurrence. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Cloze +"$\beta$-{reduces}" refers to zero or more contractions of redex-occurrences. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Cloze +{1:$(\lambda x.M)N$} is to a {2:$\beta$-redex} whereas {2:$[N/x]M$} is to a {1:contractum}. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +What is a $\lambda$-term of $(\lambda x.M)N$ called? +Back: A $\beta$-redex. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +What contractum corresponds to $\beta$-redex $(\lambda x. M)N$? +Back: $[N/x]M$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +What $\beta$-redex corresponds to contractum $[N/x]M$? +Back: $(\lambda x. M)N$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +What does it mean to contract a redex-occurrence of $P$? +Back: A $\beta$-redex in $P$ was replaced by its contractum. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +How do we denote "$P$ $\beta$-contracts to $Q$"? +Back: $P \,\triangleright_{1\beta}\, Q$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +How do we denote "$P$ $\beta$-reduces to $Q$"? +Back: $P \,\triangleright_{\beta}\, Q$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +Given $\lambda$-term $P$, is $P \,\triangleright_{1\beta}\, P$ true? +Back: No. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +Given $\lambda$-term $P$, *why* isn't $P \,\triangleright_{1\beta}\, P$ true? +Back: Replacing a $\beta$-redex in $P$ with its contractum cannot again yield $P$ again. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +Given $\lambda$-term $P$, is $P \,\triangleright_{\beta}\, P$ true? +Back: Yes. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +Is $(\lambda x. x) \,\triangleright_{1\beta}\, (\lambda y. y)$ true? +Back: No. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +Is $(\lambda x. x) \,\triangleright_{\beta}\, (\lambda y. y)$ true? +Back: Yes. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +In what way is $\beta$-contraction a stricter operation than $\beta$-reduction? +Back: The former *requires* replacing a $\beta$-redex occurrence with its contractum. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +In what way is $\beta$-reduction more general than $\alpha$-conversion? +Back: $\beta$-reduction involves a finite sequence of $\beta$-contractions *and* $\alpha$-conversions. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +How do we pronounce $P \,\triangleright_{1\beta}\, Q$? +Back: $P$ $\beta$-contracts to $Q$. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +How do we pronounce $P \,\triangleright_{\beta}\, Q$? +Back: $P$ $\beta$-reduces to $Q$. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +## Bibliography + +* Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). \ No newline at end of file