From dc1ee27c4325898cfe26df500501b1b2e60e7361 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Mon, 8 Jul 2024 08:13:15 -0600 Subject: [PATCH] Image operations and the assignment command. --- .../plugins/obsidian-to-anki-plugin/data.json | 16 ++- notes/_journal/2024-07-08.md | 11 ++ notes/_journal/{ => 2024-07}/2024-07-07.md | 0 notes/logic/quantification.md | 16 +++ notes/posix/regexp.md | 2 +- notes/programming/pred-trans.md | 133 +++++++++++++++++ notes/set/functions.md | 136 ++++++++++++++++++ notes/set/index.md | 8 ++ notes/set/relations.md | 6 +- 9 files changed, 317 insertions(+), 11 deletions(-) create mode 100644 notes/_journal/2024-07-08.md rename notes/_journal/{ => 2024-07}/2024-07-07.md (100%) diff --git a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json index d960881..865760a 100644 --- a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json +++ b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json @@ -170,7 +170,7 @@ "posix/index.md": "97b1b8ecb9a953e855a9acf0ab25b8c8", "posix/signals.md": "f4132369878c683bfac4d7fd863d19ba", "templates/daily.md": "7866014e730e85683155207a02e367d8", - "posix/regexp.md": "887711b8fc64ca258d9987133ecf056c", + "posix/regexp.md": "d7d1b8cde49c405d44c7e1d9343769c0", "journal/2024-02-04.md": "e2b5678fc53d7284b71ed6820c02b954", "gawk/regexp.md": "d9229f1eabe1b99e965eecaa03bee86c", "_templates/daily.md": "36d0b695e8a955ff1d8e980154469e03", @@ -194,7 +194,7 @@ "binary/index.md": "9089c6f0e86a0727cd03984f51350de0", "_journal/2024-02-09.md": "a798d35f0b2bd1da130f7ac766166109", "c/types.md": "cf3e66e5aee58a94db3fdf0783908555", - "logic/quantification.md": "1bc37ddebe69b4a291753a6e454d81ef", + "logic/quantification.md": "313cb37b33dfe7604ba4b8d1db4fb90f", "c/declarations.md": "2de27f565d1020819008ae80593af435", "algorithms/sorting/bubble-sort.md": "872fb23e41fb3ac36e8c46240e9a027f", "_journal/2024-02-10.md": "562b01f60ea36a3c78181e39b1c02b9f", @@ -322,7 +322,7 @@ "_journal/2024-03-18.md": "8479f07f63136a4e16c9cd07dbf2f27f", "_journal/2024-03/2024-03-17.md": "23f9672f5c93a6de52099b1b86834e8b", "set/directed-graph.md": "b4b8ad1be634a0a808af125fe8577a53", - "set/index.md": "9a270d08a96d0c8094ffb58671e50a12", + "set/index.md": "43b219df1822f002fdac63aa6d1c8f9a", "set/graphs.md": "55298be7241906cb6b61673cf0a2e709", "_journal/2024-03-19.md": "a0807691819725bf44c0262405e97cbb", "_journal/2024-03/2024-03-18.md": "63c3c843fc6cfc2cd289ac8b7b108391", @@ -445,7 +445,7 @@ "_journal/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b", "_journal/2024-05/2024-05-12.md": "ca9f3996272152ef89924bb328efd365", "git/remotes.md": "cbe2cd867f675f156e7fe71ec615890d", - "programming/pred-trans.md": "bea38879a7c500bc06e6319207f2c3d4", + "programming/pred-trans.md": "3057645553f2a762400c2929cfe926b0", "set/axioms.md": "063955bf19c703e9ad23be2aee4f1ab7", "_journal/2024-05-14.md": "f6ece1d6c178d57875786f87345343c5", "_journal/2024-05/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b", @@ -508,7 +508,7 @@ "_journal/2024-06/2024-06-04.md": "52b28035b9c91c9b14cef1154c1a0fa1", "_journal/2024-06-06.md": "3f9109925dea304e7172df39922cc95a", "_journal/2024-06/2024-06-05.md": "b06a0fa567bd81e3b593f7e1838f9de1", - "set/relations.md": "a57cf42b30db6c6b430b40c6d37a2af6", + "set/relations.md": "63cdf623940e4076d127440574f6b6a2", "_journal/2024-06-07.md": "795be41cc3c9c0f27361696d237604a2", "_journal/2024-06/2024-06-06.md": "db3407dcc86fa759b061246ec9fbd381", "_journal/2024-06-08.md": "b20d39dab30b4e12559a831ab8d2f9b8", @@ -534,7 +534,7 @@ "_journal/2024-06/2024-06-12.md": "f82dfa74d0def8c3179d3d076f94558e", "_journal/2024-06-14.md": "5d12bc272238ac985a1d35d3d63ea307", "_journal/2024-06/2024-06-13.md": "e2722a00585d94794a089e8035e05728", - "set/functions.md": "9647f452fe31324cbb98d9ff27fbf4ba", + "set/functions.md": "1a09c0a0f505c5f551a04f0595971d56", "_journal/2024-06-15.md": "92cb8dc5c98e10832fb70c0e3ab3cec4", "_journal/2024-06/2024-06-14.md": "5d12bc272238ac985a1d35d3d63ea307", "lambda-calculus/beta-reduction.md": "5532f9beec9d265724a8d205326bcf67", @@ -583,7 +583,9 @@ "_journal/2024-07/2024-07-01.md": "7cffc27813fe7a7338e411d054ac3bd5", "set/bags.md": "ba7990801734f411838d7b33e7ec0542", "_journal/2024-07-07.md": "9ee2d5007c34cc7ff681f3d9e998eca4", - "_journal/2024-07/2024-07-06.md": "2b794e424985f0e7d4d899163ce5733c" + "_journal/2024-07/2024-07-06.md": "2b794e424985f0e7d4d899163ce5733c", + "_journal/2024-07-08.md": "03ed5604e680ac9742ee99ae4b1eee8b", + "_journal/2024-07/2024-07-07.md": "9ee2d5007c34cc7ff681f3d9e998eca4" }, "fields_dict": { "Basic": [ diff --git a/notes/_journal/2024-07-08.md b/notes/_journal/2024-07-08.md new file mode 100644 index 0000000..76f62f1 --- /dev/null +++ b/notes/_journal/2024-07-08.md @@ -0,0 +1,11 @@ +--- +title: "2024-07-08" +--- + +- [x] Anki Flashcards +- [x] KoL +- [x] OGS +- [ ] Sheet Music (10 min.) +- [ ] Korean (Read 1 Story) + +* Chapter 9.1 "Assignment to Simple Variables" in "The Science of Programming." \ No newline at end of file diff --git a/notes/_journal/2024-07-07.md b/notes/_journal/2024-07/2024-07-07.md similarity index 100% rename from notes/_journal/2024-07-07.md rename to notes/_journal/2024-07/2024-07-07.md diff --git a/notes/logic/quantification.md b/notes/logic/quantification.md index 2f5cd8d..d045bf6 100644 --- a/notes/logic/quantification.md +++ b/notes/logic/quantification.md @@ -186,6 +186,22 @@ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Pre END%% +%%ANKI +Basic +When does $\exists x, \forall y, P(x, y) \Rightarrow \forall y, \exists x, P(x, y)$ hold true? +Back: Always. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +When does $\forall x, \exists y, P(x, y) \Rightarrow \exists y, \forall x, P(x, y)$ hold true? +Back: When there exists a $y$ that $P(x, y)$ holds for over all quantified $x$. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + ## Identifiers Identifiers are said to be **bound** if they are parameters to a quantifier. Identifiers that are not bound are said to be **free**. A first-order logic formula is said to be in **prenex normal form** (PNF) if written in two parts: the first consisting of quantifiers and bound variables (the **prefix**), and the second consisting of no quantifiers (the **matrix**). diff --git a/notes/posix/regexp.md b/notes/posix/regexp.md index 378526f..6a747dc 100644 --- a/notes/posix/regexp.md +++ b/notes/posix/regexp.md @@ -133,7 +133,7 @@ END%% %%ANKI Basic `^` and `$$` belong to what operator category? -Back: Anchors +Back: Anchors. Reference: “POSIX Basic Regular Expressions,” accessed February 4, 2024, [https://en.wikibooks.org/wiki/Regular_Expressions/POSIX_Basic_Regular_Expressions](https://en.wikibooks.org/wiki/Regular_Expressions/POSIX_Basic_Regular_Expressions). END%% diff --git a/notes/programming/pred-trans.md b/notes/programming/pred-trans.md index b5d2323..63a68f0 100644 --- a/notes/programming/pred-trans.md +++ b/notes/programming/pred-trans.md @@ -620,6 +620,139 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in END%% +### Assignment + +The assignment command has form $x \coloneqq e$, provided the types of $x$ and $e$ are the same. This command is read as "$x$ becomes $e$" and is defined as $$wp(''x \coloneqq e'', R) = domain(e) \,\mathop{\textbf{cand}}\, R_e^x$$ +where $domain(e)$ is a predicate that describes the set of all states in which $e$ may be evaluated. + +%%ANKI +Basic +The assignment command has what form? +Back: $x \coloneqq e$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is assignment "$x \coloneqq e$" pronounced? +Back: As "$x$ becomes $e$". +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is assignment "$x \coloneqq e$" defined in terms of $wp$? +Back: $wp(''x \coloneqq e'', R) = domain(e) \,\mathop{\textbf{cand}}\, R_e^x$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +In the $wp$ definition of "$x \coloneqq e$", what does $domain(e)$ refer to? +Back: A predicate that holds if $e$ is well-defined. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +In the $wp$ definition of "$x \coloneqq e$", $domain(e)$ must exclude which states? +Back: Those in which evaluation of $e$ would be undefined. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What assumption is made when defining assignment as "$wp(''x \coloneqq e'', R) = R_e^x$"? +Back: $domain(e)$, i.e. evaluation of $e$ is well-defined. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is definition "$wp(''x \coloneqq e'', R) = R_e^x$" more completely stated? +Back: $wp(''x \coloneqq e'', R) = domain(e) \,\mathop{\textbf{cand}}\, R_e^x$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +In what way is the $wp$ definition of assignment usually simplified? +Back: It is assumed evaluation of expressions (i.e. the RHS of $\coloneqq$) are always well-defined. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What does Gries state is "bewildering at first" about definition "$wp(''x \coloneqq e'', R) = R_e^x$"? +Back: Operational habits make us feel the precondition should be $R$ and postcondition $R_e^x$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is definition $wp(''x \coloneqq e'', R) = R_e^x$ informally justified? +Back: Since $x$ becomes $e$, $R$ is true after execution iff $R_e^x$ is true before execution. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What does $wp(''x \coloneqq 5'', x = 5)$ evaluate to? +Back: $T$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What does $wp(''x \coloneqq 5'', x \neq 5)$ evaluate to? +Back: $F$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What does $wp(''x \coloneqq x + 1'', x < 0)$ evaluate to? +Back: $x < -1$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given array $b$ with subscript range $0{:}100$, what does $wp(''x \coloneqq b[i]'', x = b[i])$ evaluate to? +Back: $0 \leq i \leq 100$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Assume $c$ is constant and $x, y$ are distinct. What does $wp(''x \coloneqq e'', y = c)$ evaluate to? +Back: $y = c$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What does evaluation "$wp(''x \coloneqq e'', y = c) = (y = c)$" demonstrate? +Back: That assignment (and expression evaluation) should exhibit no side effects. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + ## Bibliography * Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. \ No newline at end of file diff --git a/notes/set/functions.md b/notes/set/functions.md index 275916f..dbb66b6 100644 --- a/notes/set/functions.md +++ b/notes/set/functions.md @@ -1266,6 +1266,142 @@ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Pre END%% +The following holds for any sets $F$, $A$, $B$, and $\mathscr{A}$: + +* The image of unions is the union of the images: + * $F[\![\bigcup\mathscr{A}]\!] = \bigcup\,\{F[\![A]\!] \mid A \in \mathscr{A}\}$ +* The image of intersections is a subset of the intersection of images: + * $F[\![\bigcap \mathscr{A}]\!] \subseteq \bigcap\,\{F[\![A]\!] \mid A \in \mathscr{A}\}$ + * Equality holds if $F$ is single-rooted. + +%%ANKI +Basic +How does the image of unions relate to the union of images? +Back: They are equal. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +How does the union of images relate to the images of unions? +Back: They are equal. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +How does $F[\![A \cup B]\!]$ relate to $F[\![A]\!] \cup F[\![B]\!]$? +Back: They are equal. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What is the generalization of identity $F[\![A \cup B]\!] = F[\![A]\!] \cup F[\![B]\!]$? +Back: $F[\![\bigcup\mathscr{A}]\!] = \bigcup\,\{F[\![A]\!] \mid A \in \mathscr{A}\}$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What is the specialization of identity $F[\![\bigcup\mathscr{A}]\!] = \bigcup\,\{F[\![A]\!] \mid A \in \mathscr{A}\}$? +Back: $F[\![A \cup B]\!] = F[\![A]\!] \cup F[\![B]\!]$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +*Why* is the following identity intuitively true? $$F[\![A \cup B]\!] = F[\![A]\!] \cup F[\![B]\!]$$ +Back: $F(x)$ is in the range of $F$ regardless of whether $x \in A$ or $x \in B$ (or both). +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +How does the image of intersections relate to the intersection of images? +Back: The former is a subset of the latter. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +How does the intersection of images relate to the image of intersections? +Back: The latter is a subset of the former. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What condition on set $F$ makes the following true? $F[\![A \cap B]\!] \subseteq F[\![A]\!] \cap F[\![B]\!]$ +Back: N/A. This is always true. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What condition on set $F$ makes the following true? $F[\![A \cap B]\!] = F[\![A]\!] \cap F[\![B]\!]$ +Back: $F$ is single-rooted. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What condition on set $F$ makes the following true? $F[\![A]\!] \cap F[\![B]\!] \subseteq F[\![A \cap B]\!]$ +Back: $F$ is single-rooted. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What is the generalization of identity $F[\![A \cap B]\!] \subseteq F[\![A]\!] \cap F[\![B]\!]$? +Back: $F[\![\bigcap\mathscr{A}]\!] \subseteq \bigcap\,\{F[\![A]\!] \mid A \in \mathscr{A}\}$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +What is the specialization of identity $F[\![\bigcap\mathscr{A}]\!] \subseteq \bigcap\,\{F[\![A]\!] \mid A \in \mathscr{A}\}$? +Back: $F[\![A \cap B]\!] \subseteq F[\![A]\!] \cap F[\![B]\!]$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +*Why* is the following identity intuitively true? $$F[\![A \cap B]\!] \subseteq F[\![A]\!] \cap F[\![B]\!]$$ +Back: $A \cap B$ could be empty but $F[\![A]\!] \cap F[\![B]\!]$ could be nonempty. +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +The following is analagous to what logical expression of commuting quantifiers? $$F[\![A \cap B]\!] \subseteq F[\![A]\!] \cap F[\![B]\!]$$ +Back: $\exists x, \forall y, P(x, y) \Rightarrow \forall y, \exists x, P(x, y)$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + +%%ANKI +Basic +Given single-rooted $R$, the following is analagous to what logical expression of commuting quantifiers? $$R[\![A \cap B]\!] = R[\![A]\!] \cap R[\![B]\!]$$ +Back: $\exists x, \forall y, P(x, y) \Leftrightarrow \forall y, \exists x, P(x, y)$ +Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). + +END%% + ## Bibliography * “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163). diff --git a/notes/set/index.md b/notes/set/index.md index aa24d26..2dbec4f 100644 --- a/notes/set/index.md +++ b/notes/set/index.md @@ -305,6 +305,14 @@ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Pre END%% +%%ANKI +Basic +How do you rewrite $\{A \mid A \in B\}$ with an existential in the entrance requirement? +Back: $\{v \mid A \in B \land v = A\}$ +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, (\forall x, x \in A \Leftrightarrow x \in B) \Rightarrow A = B$$ diff --git a/notes/set/relations.md b/notes/set/relations.md index c63721a..fc3dc37 100644 --- a/notes/set/relations.md +++ b/notes/set/relations.md @@ -230,7 +230,7 @@ END%% %%ANKI Basic -The following is analagous to what predicate logical expression of commuting quantifiers?$$\mathop{\text{dom}}\bigcup\mathscr{A} = \bigcup\, \{\mathop{\text{dom}} R \mid R \in \mathscr{A}\}$$ +The following is analagous to what logical expression of commuting quantifiers?$$\mathop{\text{dom}}\bigcup\mathscr{A} = \bigcup\, \{\mathop{\text{dom}} R \mid R \in \mathscr{A}\}$$ Back: $\exists x, \exists y, P(x, y) \Leftrightarrow \exists y, \exists x, P(x, y)$ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). @@ -245,7 +245,7 @@ END%% %%ANKI Basic -The following is analagous to what predicate logical expression of commuting quantifiers? $$\mathop{\text{dom}}\bigcap\mathscr{A} \subseteq \bigcap\, \{\mathop{\text{dom}} R \mid R \in \mathscr{A}\}$$ +The following is analagous to what logical expression of commuting quantifiers? $$\mathop{\text{dom}}\bigcap\mathscr{A} \subseteq \bigcap\, \{\mathop{\text{dom}} R \mid R \in \mathscr{A}\}$$ Back: $\exists x, \forall y, P(x, y) \Rightarrow \forall y, \exists x, P(x, y)$ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). @@ -275,7 +275,7 @@ END%% %%ANKI Basic -The following is analagous to what predicate logical expression of commuting quantifiers? $$\mathop{\text{ran}}\bigcap\mathscr{A} \subseteq \bigcap\, \{\mathop{\text{ran}} R \mid R \in \mathscr{A}\}$$ +The following is analagous to what logical expression of commuting quantifiers? $$\mathop{\text{ran}}\bigcap\mathscr{A} \subseteq \bigcap\, \{\mathop{\text{ran}} R \mid R \in \mathscr{A}\}$$ Back: $\exists x, \forall y, P(x, y) \Rightarrow \forall y, \exists x, P(x, y)$ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).