Notes on alpha-conversion and beta-reduction.

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": [

notes/_journal/2024-06-15.md

@@ -9,3 +9,4 @@ title: "2024-06-15"
 - [ ] Korean (Read 1 Story)
 
 * [[functions|Notes]] on injections, surjections, and bijections.
+* Start defining [[beta-reduction|β-reduction]].

notes/lambda-calculus/alpha-conversion.md

@@ -20,6 +20,14 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi
 <!--ID: 1717687744134-->
 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).
+<!--ID: 1718475477173-->
+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
 <!--ID: 1717687744141-->
 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).
+<!--ID: 1718475424870-->
+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).
+<!--ID: 1718475424871-->
+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
 <!--ID: 1717687744147-->
 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).
+<!--ID: 1718475424873-->
+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).
+<!--ID: 1718475424874-->
+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).
 <!--ID: 1717687744176-->
 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).
+<!--ID: 1718475424876-->
+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
 <!--ID: 1718422981125-->
 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).
+<!--ID: 1718473252304-->
+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).
+<!--ID: 1718473252307-->
+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).
+<!--ID: 1718473252312-->
+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).
+<!--ID: 1718473252309-->
+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).
+<!--ID: 1718473252311-->
+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).

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).
+<!--ID: 1718475424836-->
+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).
+<!--ID: 1718475424840-->
+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).
+<!--ID: 1718475424841-->
+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).
+<!--ID: 1718475424843-->
+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).
+<!--ID: 1718475424844-->
+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).
+<!--ID: 1718475424846-->
+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).
+<!--ID: 1718475424848-->
+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).
+<!--ID: 1718475424849-->
+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).
+<!--ID: 1718475424850-->
+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).
+<!--ID: 1718475424852-->
+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).
+<!--ID: 1718475424853-->
+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).
+<!--ID: 1718475424855-->
+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).
+<!--ID: 1718475424857-->
+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).
+<!--ID: 1718475424859-->
+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).
+<!--ID: 1718475424860-->
+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).
+<!--ID: 1718475424862-->
+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).
+<!--ID: 1718475424864-->
+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).
+<!--ID: 1718475424865-->
+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).
+<!--ID: 1718475424867-->
+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).
+<!--ID: 1718475424868-->
+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).