From 8fda87c218cca04d89c85d5242588ba64583d94f Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Thu, 23 May 2024 14:02:55 -0600 Subject: [PATCH] Initial notes on lambda-calculus. --- .../plugins/obsidian-to-anki-plugin/data.json | 8 +- notes/_journal/2024-05-23.md | 3 +- notes/programming/λ-Calculus.md | 194 ++++++++++++++++++ notes/set/index.md | 39 ++++ 4 files changed, 240 insertions(+), 4 deletions(-) create mode 100644 notes/programming/λ-Calculus.md diff --git a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json index 270cfba..8badf81 100644 --- a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json +++ b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json @@ -313,7 +313,7 @@ "_journal/2024-03-18.md": "8479f07f63136a4e16c9cd07dbf2f27f", "_journal/2024-03/2024-03-17.md": "23f9672f5c93a6de52099b1b86834e8b", "set/directed-graph.md": "b4b8ad1be634a0a808af125fe8577a53", - "set/index.md": "67d869ecf287867199e197b3a7269c52", + "set/index.md": "6677229fea638f06e473b47aee1cd57a", "set/graphs.md": "4bbcea8f5711b1ae26ed0026a4a69800", "_journal/2024-03-19.md": "a0807691819725bf44c0262405e97cbb", "_journal/2024-03/2024-03-18.md": "63c3c843fc6cfc2cd289ac8b7b108391", @@ -460,10 +460,12 @@ "_journal/2024-05/2024-05-19.md": "fc14fc23d4ddca3628df7eec71a07e27", "_journal/2024-05-21.md": "7028d18a55f0a1f65dc0753af431ca42", "_journal/2024-05/2024-05-20.md": "d58a4ecd3bf9621cbe688f043be61239", - "_journal/2024-05-22.md": "5b4473b7c6483f3aa8727ad0a12f0408", + "_journal/2024-05-22.md": "da0364a086746087236eb8afd5770ca3", "_journal/2024-05/2024-05-21.md": "f20e4dd94ea22fcb26049de128bc944e", "set/algebra.md": "a6877ceca952c417b52ea637716addbf", - "_journal/2024-05-23.md": "a615207d43991ed0fa09fe0d913567b9" + "programming/λ-Calculus.md": "678d665f0c783a47d33b659a6980804b", + "_journal/2024-05-23.md": "8b614b7fb2ed72a0372756a576238439", + "_journal/2024-05/2024-05-22.md": "5b4473b7c6483f3aa8727ad0a12f0408" }, "fields_dict": { "Basic": [ diff --git a/notes/_journal/2024-05-23.md b/notes/_journal/2024-05-23.md index dfbe504..e7b63aa 100644 --- a/notes/_journal/2024-05-23.md +++ b/notes/_journal/2024-05-23.md @@ -8,4 +8,5 @@ title: "2024-05-23" - [ ] Go (1 Life & Death Problem) - [ ] Korean (Read 1 Story) -* Watched [Lecture #10 - Sorting & Aggregation Algorithms](https://www.youtube.com/watch?v=CMzf9Az1vl4) on databases. \ No newline at end of file +* Watched [Lecture #10 - Sorting & Aggregation Algorithms](https://www.youtube.com/watch?v=CMzf9Az1vl4) on databases. +* Work through chapter 1 of "Lambda-Calculus and Combinators, an Introduction". \ No newline at end of file diff --git a/notes/programming/λ-Calculus.md b/notes/programming/λ-Calculus.md new file mode 100644 index 0000000..ee4a0bb --- /dev/null +++ b/notes/programming/λ-Calculus.md @@ -0,0 +1,194 @@ +--- +title: λ-Calculus +TARGET DECK: Obsidian::STEM +FILE TAGS: λ-calculus +tags: + - λ-calculus +--- + +## Overview + +Assume that there is given an infinite sequence of expressions called **variables** and a finite or infinite sequence of expressions called **atomic constants**, different from the variables. The set of expressions called $\lambda$-terms is defined inductively as follows: + +* all variables and atomic constants are $\lambda$-terms (called **atoms**) +* if $M$ and $N$ are $\lambda$-terms, then $(MN)$ is a $\lambda$-term (called **application**) +* if $M$ is a $\lambda$-term and $x$ is a variable, then $(\lambda x. M)$ is a $\lambda$-term (called **abstraction**) + +If the sequence of atomic constants is empty, the system is called **pure**. Otherwise it is called **applied**. + +%%ANKI +Basic +What does a "higher-order function" refer to? +Back: A function that acts on other functions. +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 $f(x) = x - y$ written using $\lambda$-calculus? +Back: $\lambda x. x - y$ +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 $f(x, y) = x - y$ written using (uncurried) $\lambda$-calculus? +Back: $\lambda x y. x - y$ +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 you curry expression $\lambda x y. x - y$? +Back: $\lambda x. \lambda y. x - y$ +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 you uncurry expression $\lambda x. \lambda y. x - y$? +Back: $\lambda x y. x - y$ +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 $(\lambda x. x - y)(0)$ evaluate to? +Back: $0 - y$ +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 many variables exist in a $\lambda$-calculus formal system? +Back: An infinite number. +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 many atomic constants exist in a $\lambda$-calculus formal system? +Back: Zero or more. +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 variables and atomic constants? +Back: The latter is meant to refer to constants outside the formal system. +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 two classes of expressions does an "atom" potentially refer to? +Back: Variables and atomic constants. +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 general term describes both variables and atomic constants? +Back: Atoms. +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 +Why are variables and atomic constants called "atoms"? +Back: They are not composed of smaller $\lambda$-terms. +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 +When is a $\lambda$-calculus considered pure? +Back: When there exist no atomic constants in the system. +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 +When is a $\lambda$-calculus considered applied? +Back: When there exists at least one atomic constant in the system. +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 +A $\lambda$-calculus is either {pure} or {applied}. +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 term refers to the base case of the $\lambda$-term definition? +Back: The atoms. +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 term refers to the inductive cases of the $\lambda$-term definition? +Back: Application and abstraction. +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 +Given $\lambda$-terms $M$ and $N$, {$(MN)$} is referred to as {application}. +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 +Given $\lambda$-term $M$ and variable $x$, {$(\lambda x. M)$} is referred to as {abstraction}. +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 +Consider term $(\lambda x. x)(0)$. Is our $\lambda$-calculus pure or applied? +Back: Applied. +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 +Consider term $(\lambda x. x)(y)$. Is our $\lambda$-calculus pure or applied? +Back: Indeterminate. +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 three terms categorize all $\lambda$-terms? +Back: Atoms, applications, and abstractions. +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/set/index.md b/notes/set/index.md index 213e251..7914434 100644 --- a/notes/set/index.md +++ b/notes/set/index.md @@ -134,6 +134,45 @@ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Pre END%% +%%ANKI +Basic +What does an atom refer to in set theory? +Back: Any entity that is not a set but can exist in one. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Cloze +An {1:atom} in set theory is to {2:atomic} logical statements whereas {2:sets} are to {1:molecular} statements. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What distinguishes a set from an atom? +Back: An atom cannot contain other entitites. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What intuition is broken when a box is viewed as an atom? +Back: When viewed as an atom, the box is no longer a container. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Enderton's exposition makes what assumption about atoms? +Back: The set of all atoms is the empty set. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + ## Extensionality If two sets have exactly the same members, then they are equal: $$\forall A, \forall B, (x \in A \Leftrightarrow x \in B) \Rightarrow A = B$$