Additional lambda calculus notes.

2024-05-26 17:06:33 -06:00 · 2024-05-26 17:06:33 -06:00 · e87168b297
parent 6b26e89d3c
commit e87168b297
9 changed files with 435 additions and 17 deletions
--- 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": [
--- a/notes/_journal/2024-05-26.md
+++ 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.).
--- a/notes/_journal/2024-05/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)
--- a/notes/_journal/2024-05/2024-05-25.md
+++ 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)
--- 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 (
 <!--ID: 1707398773330-->
 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).
+<!--ID: 1716632860458-->
+END%%
+
 %%ANKI
 Basic
 Is `SELECTION_SORT` adaptive?
--- 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).
 <!--ID: 1716307180986-->
 END%%
--- 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
 <!--ID: 1716498992534-->
 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).
+<!--ID: 1716743248092-->
+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).
+<!--ID: 1716743248095-->
+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).
+<!--ID: 1716743248096-->
+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).
+<!--ID: 1716743248098-->
+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).
+<!--ID: 1716743248100-->
+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).
+<!--ID: 1716743248101-->
+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).
+<!--ID: 1716743248103-->
+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).
+<!--ID: 1716743248104-->
+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).
+<!--ID: 1716743248106-->
+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).
+<!--ID: 1716743248108-->
+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).
+<!--ID: 1716743248110-->
+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).
+<!--ID: 1716743248112-->
+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). 
+<!--ID: 1716743248113-->
+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).
+<!--ID: 1716743248115-->
+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).
+<!--ID: 1716743248117-->
+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).
+<!--ID: 1716743248118-->
+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).
+<!--ID: 1716743248120-->
+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).
+<!--ID: 1716743248122-->
+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).
+<!--ID: 1716743248124-->
+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).
+<!--ID: 1716743248125-->
+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).
+<!--ID: 1716743248127-->
+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).
+<!--ID: 1716745015997-->
+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).
+<!--ID: 1716745016000-->
+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).
+<!--ID: 1716745016002-->
+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).
+<!--ID: 1716745016003-->
+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).
+<!--ID: 1716745016005-->
+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).
+<!--ID: 1716745016007-->
+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).
+<!--ID: 1716745016008-->
+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).
+<!--ID: 1716745016009-->
+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).
+<!--ID: 1716745016011-->
+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).
+<!--ID: 1716745016012-->
+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).
+<!--ID: 1716745016014-->
+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).
+<!--ID: 1716745016015-->
+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).
+<!--ID: 1716745016017-->
+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).
+<!--ID: 1716745016018-->
+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).
+<!--ID: 1716745016020-->
+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).
+<!--ID: 1716745016021-->
+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).
+<!--ID: 1716745016023-->
+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).
+<!--ID: 1716745016024-->
+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).
+<!--ID: 1716745016026-->
+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).
+<!--ID: 1716745016027-->
+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).
+<!--ID: 1716745016028-->
+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).
+<!--ID: 1716745016030-->
+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).
+<!--ID: 1716745016031-->
+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).
+<!--ID: 1716745016033-->
+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).
+<!--ID: 1716745016034-->
+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).
--- 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.
 <!--ID: 1716310927700-->
@ -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.
 <!--ID: 1716310927701-->
@ -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.
 <!--ID: 1716310927703-->
@ -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.
 <!--ID: 1716310927710-->
@ -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.
 <!--ID: 1716310927718-->
--- 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).
 <!--ID: 1716309007849-->
 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).
 <!--ID: 1716309007859-->
 END%%