From 016d498862bd91b3bdc0f83b8c0cb614e1bed2e8 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Wed, 29 May 2024 06:30:49 -0600 Subject: [PATCH] Fixup lambda calculus flashcards. --- .../plugins/obsidian-to-anki-plugin/data.json | 16 ++++++++----- notes/_journal/2024-05-29.md | 9 ++++++++ notes/_journal/{ => 2024-05}/2024-05-27.md | 0 notes/_journal/2024-05/2024-05-28.md | 9 ++++++++ notes/algebra/polynomials.md | 4 ++-- notes/programming/lambda-calculus.md | 23 ++++--------------- notes/programming/pred-trans.md | 2 +- notes/set/index.md | 6 ++--- notes/set/trees.md | 4 ++-- 9 files changed, 40 insertions(+), 33 deletions(-) create mode 100644 notes/_journal/2024-05-29.md rename notes/_journal/{ => 2024-05}/2024-05-27.md (100%) create mode 100644 notes/_journal/2024-05/2024-05-28.md diff --git a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json index 0cf8085..dd4a2e1 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": "4a190fea888f896f6784f350216cdf46", + "set/index.md": "74b50d8ca249c4e99b22abd4adedb300", "set/graphs.md": "4bbcea8f5711b1ae26ed0026a4a69800", "_journal/2024-03-19.md": "a0807691819725bf44c0262405e97cbb", "_journal/2024-03/2024-03-18.md": "63c3c843fc6cfc2cd289ac8b7b108391", @@ -334,7 +334,7 @@ "x86-64/declarations.md": "75bc7857cf2207a40cd7f0ee056af2f2", "x86-64/instructions.md": "c9ae5dedaa22fbcdc486663877fc1c1e", "git/refs.md": "e20c2c9b14ba6c2bd235416017c5c474", - "set/trees.md": "c29347ec0ac2e8d5339514c869ecaedf", + "set/trees.md": "b085bd8d08dccd8cbf02bb1b7a4baa43", "_journal/2024-03-24.md": "1974cdb9fc42c3a8bebb8ac76d4b1fd6", "_journal/2024-03/2024-03-23.md": "ad4e92cc2bf37f174a0758a0753bf69b", "_journal/2024-03/2024-03-22.md": "a509066c9cd2df692549e89f241d7bd9", @@ -372,7 +372,7 @@ "_journal/2024-04/2024-04-14.md": "037c77d0e11f2d58ffee61ea0a1708ab", "_journal/2024-04-16.md": "0bf6e2f2a3afab73d528cee88c4c1a92", "_journal/2024-04/2024-04-15.md": "256253b0633d878ca58060162beb7587", - "algebra/polynomials.md": "6e20029b44fe0d0c4f35ef8ee4874d82", + "algebra/polynomials.md": "da56d2d6934acfa2c6b7b2c73c87b2c7", "algebra/sequences/delta-constant.md": "70f45d7b8d5c3a147fabc279105c4983", "_journal/2024-04-19.md": "a293087860a7f378507a96df0b09dd2b", "_journal/2024-04/2024-04-18.md": "f6e5bee68dbef90a21ca92a846930a88", @@ -436,7 +436,7 @@ "_journal/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b", "_journal/2024-05/2024-05-12.md": "ca9f3996272152ef89924bb328efd365", "git/remotes.md": "2208e34b3195b6f1ec041024a66fb38b", - "programming/pred-trans.md": "24fb4b8d8137626dcacbc02c9ecd07a1", + "programming/pred-trans.md": "6925b0be2de73c214df916a53e23fd5a", "set/axioms.md": "063955bf19c703e9ad23be2aee4f1ab7", "_journal/2024-05-14.md": "f6ece1d6c178d57875786f87345343c5", "_journal/2024-05/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b", @@ -466,7 +466,7 @@ "programming/λ-Calculus.md": "bf36bdaf85abffd171bb2087fb8228b2", "_journal/2024-05-23.md": "9d9106a68197adcee42cd19c69d2f840", "_journal/2024-05/2024-05-22.md": "3c29eec25f640183b0be365e7a023750", - "programming/lambda-calculus.md": "6930e7031babe1fb5a2dec9cc3bedcac", + "programming/lambda-calculus.md": "2d68babe42439dc5daa318ec3f28881f", "_journal/2024-05-25.md": "04e8e1cf4bfdbfb286effed40b09c900", "_journal/2024-05/2024-05-24.md": "86132f18c7a27ebc7a3e4a07f4867858", "_journal/2024-05/2024-05-23.md": "d0c98b484b1def3a9fd7262dcf2050ad", @@ -476,7 +476,11 @@ "_journal/2024-05/2024-05-26.md": "abe84b5beae74baa25501c818e64fc95", "algebra/set.md": "d7b4c7943f3674bb152389f4bef1a234", "algebra/boolean.md": "56d2e0be2853d49b5dface7fa2d785a9", - "git/merge-conflicts.md": "cb7d4d373639f75f6647be60f3fe97f3" + "git/merge-conflicts.md": "cb7d4d373639f75f6647be60f3fe97f3", + "_journal/2024-05-28.md": "0f6aeb5ec126560acdc2d8c5c6570337", + "_journal/2024-05/2024-05-27.md": "e498d5154558ebcf7261302403ea8016", + "_journal/2024-05-29.md": "566571bac8f4945bde6bc4483e3d6bc6", + "_journal/2024-05/2024-05-28.md": "28297d2a418f591ebc15c74fa459ddd9" }, "fields_dict": { "Basic": [ diff --git a/notes/_journal/2024-05-29.md b/notes/_journal/2024-05-29.md new file mode 100644 index 0000000..423f40f --- /dev/null +++ b/notes/_journal/2024-05-29.md @@ -0,0 +1,9 @@ +--- +title: "2024-05-29" +--- + +- [x] Anki Flashcards +- [x] KoL +- [ ] Sheet Music (10 min.) +- [ ] Go (1 Life & Death Problem) +- [ ] Korean (Read 1 Story) \ No newline at end of file diff --git a/notes/_journal/2024-05-27.md b/notes/_journal/2024-05/2024-05-27.md similarity index 100% rename from notes/_journal/2024-05-27.md rename to notes/_journal/2024-05/2024-05-27.md diff --git a/notes/_journal/2024-05/2024-05-28.md b/notes/_journal/2024-05/2024-05-28.md new file mode 100644 index 0000000..167bd59 --- /dev/null +++ b/notes/_journal/2024-05/2024-05-28.md @@ -0,0 +1,9 @@ +--- +title: "2024-05-28" +--- + +- [x] Anki Flashcards +- [x] KoL +- [ ] Sheet Music (10 min.) +- [ ] Go (1 Life & Death Problem) +- [ ] Korean (Read 1 Story) \ No newline at end of file diff --git a/notes/algebra/polynomials.md b/notes/algebra/polynomials.md index cbfe364..fa5e57b 100644 --- a/notes/algebra/polynomials.md +++ b/notes/algebra/polynomials.md @@ -14,8 +14,8 @@ The coefficients of $p(n)$ are $a_0, a_1, \ldots, a_d$. Furthermore, $a_d \neq 0 %%ANKI Basic -Using sigma notation, a polynomial in $n$ of degree $d$ is a function of what form? -Back: $p(n) = \sum_{i=0}^d a_in^i$ where $a_d \neq 0$. +Using sigma notation, a polynomial $p(n)$ in $n$ of degree $d$ is a function of what form? +Back: $p(n) = \sum_{k=0}^d a_kn^k$ where $a_d \neq 0$. Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). END%% diff --git a/notes/programming/lambda-calculus.md b/notes/programming/lambda-calculus.md index 36c97c1..03f6470 100644 --- a/notes/programming/lambda-calculus.md +++ b/notes/programming/lambda-calculus.md @@ -145,7 +145,7 @@ END%% %%ANKI Basic -What term refers to the inductive cases of the $\lambda$-term definition? +What terms refer 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). @@ -197,14 +197,6 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi END%% -%%ANKI -Basic -How is expression $MNPQ$ written with parentheses reintroduced? -Back: $(((MN)P)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 Cloze By convention, parentheses in $\lambda$-calculus are {left}-associative. @@ -220,13 +212,6 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi END%% -%%ANKI -Cloze -Expression $(MN)$ is interpreted as applying {$M$} to {$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 How are parentheses conventionally reintroduced to $\lambda$-term $MN$? @@ -398,7 +383,7 @@ END%% %%ANKI Basic What preprocessing step does Hindley et al. recommend when counting occurrences of $\lambda$-terms? -Back: Reintroduce parentheses in the top-level term. +Back: Reintroduce parentheses. 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%% @@ -423,7 +408,7 @@ END%% %%ANKI Basic What is the scope of the leftmost $\lambda y$ in the following term? $$(\lambda y. yx(\lambda x. y(\lambda y.z)x))vw$$ -Back: $yx(\lambda x. y(\lambda y. z)x))vw$ +Back: $yx(\lambda x. y(\lambda y. z)x)$ 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%% @@ -462,7 +447,7 @@ $FV(P)$ denotes the set of all free variables of $P$. A **closed term** is a ter %%ANKI Basic -What kind of $\lambda$-terms are considered bound or free? +What kind of $\lambda$-terms can be classified as bound and/or free? Back: 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). diff --git a/notes/programming/pred-trans.md b/notes/programming/pred-trans.md index bd18398..cd57519 100644 --- a/notes/programming/pred-trans.md +++ b/notes/programming/pred-trans.md @@ -128,7 +128,7 @@ END%% %%ANKI Basic *Why* is $\{T\}\; \text{while }T\text{ do skip}\; \{T\}$ everywhere false? -Back: Because $\text{while }T\text{ do skip}$ never terminates. +Back: Because "$\text{while }T\text{ do skip}$" never terminates. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. END%% diff --git a/notes/set/index.md b/notes/set/index.md index 147a564..f9e3bdd 100644 --- a/notes/set/index.md +++ b/notes/set/index.md @@ -182,7 +182,7 @@ 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$$ +If two sets have exactly the same members, then they are equal: $$\forall A, \forall B, (\forall x, x \in A \Leftrightarrow x \in B) \Rightarrow A = B$$ %%ANKI Basic What does the extensionality axiom state? @@ -194,14 +194,14 @@ END%% %%ANKI Basic How is the extensionality axiom expressed using first-order logic? -Back: $$\forall A, \forall B, (x \in A \Leftrightarrow x \in B) \Rightarrow A = B$$ +Back: $$\forall A, \forall B, (\forall x, x \in A \Leftrightarrow x \in B) \Rightarrow A = B$$ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). END%% %%ANKI Basic -The following encodes which set theory axiom? $$\forall A, \forall B, (x \in A \Leftrightarrow x \in B) \Rightarrow A = B$$ +The following encodes which set theory axiom? $$\forall A, \forall B, (\forall x, x \in A \Leftrightarrow x \in B) \Rightarrow A = B$$ Back: The extensionality axiom. Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). diff --git a/notes/set/trees.md b/notes/set/trees.md index 89b319e..f5c84aa 100644 --- a/notes/set/trees.md +++ b/notes/set/trees.md @@ -1477,7 +1477,7 @@ Basic How should the nil constructor of an inductive binary tree, say `Tree`, be defined? Back: ```lean -| constructor : Tree α +| nil : Tree α ``` Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). Tags: lean @@ -1489,7 +1489,7 @@ Basic How should the non-nil constructor of an inductive binary tree, say `Tree`, be defined? Back: ```lean -| constructor : α → Tree α → Tree α → Tree α +| node : α → Tree α → Tree α → Tree α ``` Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). Tags: lean