From e87168b297a9632018467210e779c48f90137077 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sun, 26 May 2024 17:06:33 -0600 Subject: [PATCH] Additional lambda calculus notes. --- .../plugins/obsidian-to-anki-plugin/data.json | 16 +- notes/_journal/2024-05-26.md | 11 + notes/_journal/{ => 2024-05}/2024-05-24.md | 2 +- notes/_journal/2024-05/2024-05-25.md | 9 + notes/algorithms/sorting/selection-sort.md | 8 + notes/hashing/direct-addressing.md | 2 +- notes/programming/lambda-calculus.md | 390 +++++++++++++++++- notes/programming/pred-trans.md | 10 +- notes/set/index.md | 4 +- 9 files changed, 435 insertions(+), 17 deletions(-) create mode 100644 notes/_journal/2024-05-26.md rename notes/_journal/{ => 2024-05}/2024-05-24.md (67%) create mode 100644 notes/_journal/2024-05/2024-05-25.md diff --git a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json index ba90e22..6845249 100644 --- a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json +++ b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json @@ -179,7 +179,7 @@ "algorithms/running-time.md": "5efc0791097d2c996f931c9046c95f65", "algorithms/order-growth.md": "12bf6c10653912283921dcc46c7fa0f8", "_journal/2024-02-08.md": "19092bdfe378f31e2774f20d6afbfbac", - "algorithms/sorting/selection-sort.md": "4c63541e8a886f17e4dc2b24215fefe8", + "algorithms/sorting/selection-sort.md": "73415c44d6f4429f43c366078fd4bf98", "algorithms/index 1.md": "6fada1f3d5d3af64687719eb465a5b97", "binary/hexadecimal.md": "c3d485f1fd869fe600334ecbef7d5d70", "binary/index.md": "9089c6f0e86a0727cd03984f51350de0", @@ -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": "6677229fea638f06e473b47aee1cd57a", + "set/index.md": "87f04456ea94ca2d06514f98101fa39a", "set/graphs.md": "4bbcea8f5711b1ae26ed0026a4a69800", "_journal/2024-03-19.md": "a0807691819725bf44c0262405e97cbb", "_journal/2024-03/2024-03-18.md": "63c3c843fc6cfc2cd289ac8b7b108391", @@ -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": "db73cc035e92cd019e7e6f79921e6c1e", + "programming/pred-trans.md": "c3039011d2ec6f968cd0c759cbc4b2e6", "set/axioms.md": "063955bf19c703e9ad23be2aee4f1ab7", "_journal/2024-05-14.md": "f6ece1d6c178d57875786f87345343c5", "_journal/2024-05/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b", @@ -450,7 +450,7 @@ "_journal/2024-05-17.md": "fb880d68077b655ede36d994554f3aba", "_journal/2024-05/2024-05-16.md": "9fdfadc3f9ea6a4418fd0e7066d6b10c", "_journal/2024-05-18.md": "c0b58b28f84b31cea91404f43b0ee40c", - "hashing/direct-addressing.md": "7ffaa27c01130d21aa32cf3b1c407785", + "hashing/direct-addressing.md": "87d1052ac7eae3061d88d011432cb693", "hashing/index.md": "c870cf66e0224db58315ac0ba43b9cb1", "set/classes.md": "18a09731868070e0c24a42bf0f582619", "_journal/2024-05-19.md": "fddd90fae08fab9bd83b0ef5d362c93a", @@ -465,7 +465,13 @@ "set/algebra.md": "a6877ceca952c417b52ea637716addbf", "programming/λ-Calculus.md": "bf36bdaf85abffd171bb2087fb8228b2", "_journal/2024-05-23.md": "9d9106a68197adcee42cd19c69d2f840", - "_journal/2024-05/2024-05-22.md": "5b4473b7c6483f3aa8727ad0a12f0408" + "_journal/2024-05/2024-05-22.md": "5b4473b7c6483f3aa8727ad0a12f0408", + "programming/lambda-calculus.md": "6930e7031babe1fb5a2dec9cc3bedcac", + "_journal/2024-05-25.md": "04e8e1cf4bfdbfb286effed40b09c900", + "_journal/2024-05/2024-05-24.md": "86132f18c7a27ebc7a3e4a07f4867858", + "_journal/2024-05/2024-05-23.md": "d0c98b484b1def3a9fd7262dcf2050ad", + "_journal/2024-05-26.md": "3b95f86726d646f157ebe2ae55e2afda", + "_journal/2024-05/2024-05-25.md": "3e8a0061fa58a6e5c48d12800d1ab869" }, "fields_dict": { "Basic": [ diff --git a/notes/_journal/2024-05-26.md b/notes/_journal/2024-05-26.md new file mode 100644 index 0000000..20bb74b --- /dev/null +++ b/notes/_journal/2024-05-26.md @@ -0,0 +1,11 @@ +--- +title: "2024-05-26" +--- + +- [x] Anki Flashcards +- [x] KoL +- [ ] Sheet Music (10 min.) +- [ ] Go (1 Life & Death Problem) +- [ ] Korean (Read 1 Story) + +* Additional foundational notes on $\lambda$-calculus (length, scope, bound variables, etc.). \ No newline at end of file diff --git a/notes/_journal/2024-05-24.md b/notes/_journal/2024-05/2024-05-24.md similarity index 67% rename from notes/_journal/2024-05-24.md rename to notes/_journal/2024-05/2024-05-24.md index 063297d..2e6273b 100644 --- a/notes/_journal/2024-05-24.md +++ b/notes/_journal/2024-05/2024-05-24.md @@ -2,7 +2,7 @@ title: "2024-05-24" --- -- [ ] Anki Flashcards +- [x] Anki Flashcards - [x] KoL - [ ] Sheet Music (10 min.) - [ ] Go (1 Life & Death Problem) diff --git a/notes/_journal/2024-05/2024-05-25.md b/notes/_journal/2024-05/2024-05-25.md new file mode 100644 index 0000000..3e2f5cc --- /dev/null +++ b/notes/_journal/2024-05/2024-05-25.md @@ -0,0 +1,9 @@ +--- +title: "2024-05-25" +--- + +- [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/algorithms/sorting/selection-sort.md b/notes/algorithms/sorting/selection-sort.md index 0f9dba8..24c30f4 100644 --- a/notes/algorithms/sorting/selection-sort.md +++ b/notes/algorithms/sorting/selection-sort.md @@ -69,6 +69,14 @@ Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition ( END%% +%%ANKI +Basic +*Why* isn't `SELECTION_SORT` stable? +Back: The current element of an iteration is potentially swapped into an unstable position. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + %%ANKI Basic Is `SELECTION_SORT` adaptive? diff --git a/notes/hashing/direct-addressing.md b/notes/hashing/direct-addressing.md index af15f4b..269b8c4 100644 --- a/notes/hashing/direct-addressing.md +++ b/notes/hashing/direct-addressing.md @@ -108,7 +108,7 @@ END%% %%ANKI Basic In what situation does direct addressing waste space? -Back: When the number of keys used is much less than the size of the universe. +Back: When the number of keys used is less than the size of the universe. 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 ba942cc..36c97c1 100644 --- a/notes/programming/lambda-calculus.md +++ b/notes/programming/lambda-calculus.md @@ -10,9 +10,9 @@ tags: 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**) +* 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**. @@ -227,6 +227,390 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi END%% +%%ANKI +Basic +How are parentheses conventionally reintroduced to $\lambda$-term $MN$? +Back: $(MN)$ +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 $MNPQ$? +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 +Basic +How are parentheses conventionally reintroduced to $\lambda$-term $\lambda x. PQ$? +Back: $(\lambda x. (PQ))$ +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 +$(MN)$ is interpreted as applying {1:$M$} to {1:$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%% + +The length of a $\lambda$-term (denoted $lgh$) is equal to the number of atoms in the term: + +* $lgh(a) = 1$ for all atoms $a$; +* $lgh(MN) = lgh(M) + lgh(N)$; +* $lgh(\lambda x. M) = 1 + lgh(M)$. + +%%ANKI +Basic +What is the base case of the recursive definition of the "length of a $\lambda$-term"? +Back: $lgh(a) = 1$ for all atoms $a$. +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 the length of a $\lambda$-term measure? +Back: The number of atoms in the term. +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 +For atom $a$, what does $lgh(a)$ equal? +Back: $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%% + +%%ANKI +Basic +What is the recursive definition of the "length of application"? +Back: For $\lambda$-terms $M$ and $N$, $lgh(MN) = lgh(M) + lgh(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 +For $\lambda$-terms $M$ and $N$, what does $lgh(MN)$ equal? +Back: $lgh(M) + lgh(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 is the recursive definition of the "length of abstraction"? +Back: For $\lambda$-term $M$, $lgh(\lambda x. M) = 1 + lgh(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 +For $\lambda$-term $M$, what does $lgh(\lambda x. M)$ equal? +Back: $1 + lgh(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 does $lgh(x(\lambda y. yux))$ equal? +Back: $5$ +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 +The phrase "{induction on $M$}" is shorthand for phrase "{induction on $lgh(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%% + +For $\lambda$-terms $P$ and $Q$, the relation **$P$ occurs in $Q$** is defined by induction on $Q$ as: + +* $P$ occurs in $P$; +* if $P$ occurs in $M$ or in $N$, then $P$ occurs in $(MN)$; +* if $P$ occurs in $M$ or $P$ is $x$, then $P$ occurs in $(\lambda x. M)$. + +%%ANKI +Basic +What is the base case of recursive definition "$P$ occurs in $Q$"? +Back: $P$ occurs in $P$. +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 intuition does the "occurs in" relation aim to capture? +Back: Whether a $\lambda$-term appears somewhere in another $\lambda$-term. +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 +If $P$ occurs in {1:$M$} or {1:$N$}, then $P$ occurs in $(MN)$. +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 +If $P$ occurs in {1:$M$} or $P$ {1:is $x$}, then $P$ occurs in $(\lambda 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 "occurs in" recursively defined for application? +Back: If $P$ occurs in $M$ or $N$, then $P$ occurs in $(MN)$. +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 "occurs in" recursively defined for abstraction? +Back: If $P$ occurs in $M$ or $P$ is $x$, then $P$ occurs in $(\lambda 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 many occurences of $x$ are in $((xy)(\lambda x. (xy)))$? +Back: Three. +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 preprocessing step does Hindley et al. recommend when counting occurrences of $\lambda$-terms? +Back: Reintroduce parentheses in the top-level term. +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%% + +For a particular occurrence of $\lambda x. M$ in a term $P$, the occurrence of $M$ is called the **scope** of the occurrence of $\lambda x$. + +%%ANKI +Cloze +Given term $\lambda x. M$, the occurrence of {1:$M$} is called the {2:scope} of the occurrence of {1:$\lambda 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%% + +%%ANKI +Basic +The concept of scope is relevant to what kind of $\lambda$-term? +Back: 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%% + +%%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$ +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 the scope of $\lambda x$ in the following term? $$(\lambda y. yx(\lambda x. y(\lambda y.z)x))vw$$ +Back: $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%% + +%%ANKI +Basic +What is the scope of the rightmost $\lambda y$ in the following term? $$(\lambda y. yx(\lambda x. y(\lambda y.z)x))vw$$ +Back: $z$ +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 wrong with asking "what is the scope of $x$ in $\lambda$-term $P$"? +Back: We should be asking about a $\lambda 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%% + +An occurrence of a variable $x$ in a term $P$ is called + +* **bound** if it is in the scope of a $\lambda x$ in $P$; +* **bound and binding** iff it is the $x$ in $\lambda x$; +* **free** otherwise. + +$FV(P)$ denotes the set of all free variables of $P$. A **closed term** is a term without any free variables. + +%%ANKI +Basic +What kind of $\lambda$-terms are considered bound 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). + +END%% + +%%ANKI +Basic +When is variable $x$ in term $P$ said to be "bound"? +Back: When it is in the scope of a $\lambda x$ in $P$. +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 variable $x$ in term $P$ said to be "bound and binding"? +Back: If and only if it is the $x$ in some occurrence of $\lambda 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%% + +%%ANKI +Basic +When is variable $x$ in term $P$ said to be "free"? +Back: When it is not bound. +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 variable $x$ in term $P$ said to be "free and binding"? +Back: N/A. +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 variable $x$ in term $P$ said to be "bound" and "free"? +Back: When one occurrence is bound and another occurrence is free. +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 variable $x$ called a "bound variable of $P$"? +Back: When $x$ has at least one binding occurrence in $P$. +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 variable $x$ called a "free variable of $P$"? +Back: When $x$ has at least one free occurrence in $P$. +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 +{$FV(P)$} denotes the {set of all free variables} of $P$. +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$-term considered "closed"? +Back: When the term has no free 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 term describes $\lambda$-term $P$ satisfying $FV(P) = \varnothing$? +Back: Closed. +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 +Using $FV$, when is $\lambda$-term $P$ closed? +Back: When $FV(P) = \varnothing$. +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. y$ a closed term? Why or why not? +Back: No. $y$ is a free 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 +Is $\lambda x. x$ a closed term? Why or why not? +Back: Yes. The term has no free 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 +Which specific occurrences are bound in $\lambda x. x(\lambda y. yz)$? +Back: Each $x$ and each $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 +Which specific occurrences are free in $\lambda x. x(\lambda y. yz)$? +Back: The only $z$. +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 +Which specific occurrences are bpund and binding in $\lambda x. x(\lambda y. yz)$? +Back: The first $x$ and the first $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 expression $FV(\lambda x. xyz)$ evaluate to? +Back: $\{y, z\}$ +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$, what kind of mathematic object is $FV(P)$? +Back: A set. +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/programming/pred-trans.md b/notes/programming/pred-trans.md index ca5f64f..e528971 100644 --- a/notes/programming/pred-trans.md +++ b/notes/programming/pred-trans.md @@ -410,7 +410,7 @@ END%% %%ANKI Basic -Is $wp(S, Q \lor R) \Rightarrow wp(S, Q) \lor wp(S, R)$ true if $S$ is nondeterministic? +Assuming $S$ is nondeterministic, is the following a tautology? $$wp(S, Q \lor R) \Rightarrow wp(S, Q) \lor wp(S, R)$$ Back: No. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. @@ -418,7 +418,7 @@ END%% %%ANKI Basic -Is $wp(S, Q) \lor wp(S, R) \Rightarrow wp(S, Q \lor R)$ true if $S$ is nondeterministic? +Assuming $S$ is nondeterministic, is the following a tautology? $$wp(S, Q) \lor wp(S, R) \Rightarrow wp(S, Q \lor R)$$ Back: Yes. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. @@ -426,7 +426,7 @@ END%% %%ANKI Basic -Is $wp(S, Q \lor R) \Rightarrow wp(S, Q) \lor wp(S, R)$ true if $S$ is deterministic? +Assuming $S$ is deterministic, is the following a tautology? $$wp(S, Q \lor R) \Rightarrow wp(S, Q) \lor wp(S, R)$$ Back: Yes. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. @@ -434,7 +434,7 @@ END%% %%ANKI Basic -Is $wp(S, Q) \lor wp(S, R) \Rightarrow wp(S, Q \lor R)$ true if $S$ is deterministic? +Assuming $S$ is deterministic, is the following a tautology? $$wp(S, Q) \lor wp(S, R) \Rightarrow wp(S, Q \lor R)$$ Back: Yes. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. @@ -482,7 +482,7 @@ END%% %%ANKI Basic -What determines the direction of implication in Distributivity of Disjunction? +What constant operand evaluations determine the direction of implication in Distributivity of Disjunction? Back: $F \Rightarrow T$ evaluates truthily but $T \Rightarrow F$ does not. Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. diff --git a/notes/set/index.md b/notes/set/index.md index 7914434..fda0ce6 100644 --- a/notes/set/index.md +++ b/notes/set/index.md @@ -422,7 +422,7 @@ END%% %%ANKI Basic How is the union axiom (general form) expressed using first-order logic? -Back: $$\forall A, \exists B, \forall x, x \in B \Leftrightarrow (\exists b \in B, x \in b)$$ +Back: $$\forall A, \exists B, \forall x, x \in B \Leftrightarrow (\exists a \in A, x \in a)$$ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). END%% @@ -462,7 +462,7 @@ END%% %%ANKI Basic How is $\bigcup A$ represented in first-order logic? -Back: $\{x \mid \exists b \in A, x \in b\}$ +Back: $\{x \mid \exists a \in A, x \in a\}$ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). END%%