From 2ab913f70e0e4f1c3bed1cb58472c4f98e38f781 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sat, 20 Jul 2024 09:41:15 -0600 Subject: [PATCH] Prep for general textual substitution and assignment. --- .../plugins/obsidian-to-anki-plugin/data.json | 16 +- notes/_journal/2024-07-20.md | 11 + notes/_journal/{ => 2024-07}/2024-07-19.md | 0 notes/algorithms/order-growth.md | 4 +- notes/combinatorics/permutations.md | 1 + notes/hashing/index.md | 213 +++++++++- notes/logic/equiv-trans.md | 369 +++++++++--------- notes/programming/pred-trans.md | 16 +- notes/set/index.md | 2 +- 9 files changed, 421 insertions(+), 211 deletions(-) create mode 100644 notes/_journal/2024-07-20.md rename notes/_journal/{ => 2024-07}/2024-07-19.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 fee2a6d..f3fff0c 100644 --- a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json +++ b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json @@ -183,12 +183,12 @@ "_journal/2024-02-02.md": "a3b222daee8a50bce4cbac699efc7180", "_journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb", "_journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970", - "logic/equiv-trans.md": "f910dc13cb20db291b1d1241e8046bee", + "logic/equiv-trans.md": "34c29b7686b373916e247f700be488b9", "_journal/2024-02-07.md": "8d81cd56a3b33883a7706d32e77b5889", "algorithms/loop-invariants.md": "cbefc346842c21a6cce5c5edce451eb2", "algorithms/loop-invariant.md": "3b390e720f3b2a98e611b49a0bb1f5a9", "algorithms/running-time.md": "5efc0791097d2c996f931c9046c95f65", - "algorithms/order-growth.md": "8f6f38331bc4f7640f71794dd616bd23", + "algorithms/order-growth.md": "1c3f7ff710b6e67a04e16cdfd0f63e8c", "_journal/2024-02-08.md": "19092bdfe378f31e2774f20d6afbfbac", "algorithms/sorting/selection-sort.md": "73415c44d6f4429f43c366078fd4bf98", "algorithms/index 1.md": "6fada1f3d5d3af64687719eb465a5b97", @@ -244,7 +244,7 @@ "combinatorics/additive-principle.md": "d036ac511e382d5c1caca437341a5915", "_journal/2024-02-19.md": "30d16c5373deb9cb128d2e7934ae256a", "_journal/2024-02/2024-02-18.md": "67e36dbbb2cac699d4533b5a2eaeb629", - "combinatorics/permutations.md": "1b994b48798699655ee64df29c640251", + "combinatorics/permutations.md": "efd0820ab3cc7faa5b2df3fe40105110", "combinatorics/combinations.md": "396fc32255710eaf33213efaafdc43d4", "_journal/2024-02-20.md": "b85ba0eeeb16e30a602ccefabcc9763e", "_journal/2024-02/2024-02-19.md": "df1a9ab7ab89244021b3003c84640c78", @@ -324,7 +324,7 @@ "_journal/2024-03-18.md": "8479f07f63136a4e16c9cd07dbf2f27f", "_journal/2024-03/2024-03-17.md": "23f9672f5c93a6de52099b1b86834e8b", "set/directed-graph.md": "b4b8ad1be634a0a808af125fe8577a53", - "set/index.md": "ea5e92b9792a8e093bac259f85f1f829", + "set/index.md": "6670c57f29c84eef8dcfff7a8901befe", "set/graphs.md": "1a0c09f643829dae6a101b96de31eb40", "_journal/2024-03-19.md": "a0807691819725bf44c0262405e97cbb", "_journal/2024-03/2024-03-18.md": "63c3c843fc6cfc2cd289ac8b7b108391", @@ -447,7 +447,7 @@ "_journal/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b", "_journal/2024-05/2024-05-12.md": "ca9f3996272152ef89924bb328efd365", "git/remotes.md": "cbe2cd867f675f156e7fe71ec615890d", - "programming/pred-trans.md": "3057645553f2a762400c2929cfe926b0", + "programming/pred-trans.md": "ea5555291f8cdd3974ac09ea7b120a16", "set/axioms.md": "063955bf19c703e9ad23be2aee4f1ab7", "_journal/2024-05-14.md": "f6ece1d6c178d57875786f87345343c5", "_journal/2024-05/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b", @@ -462,7 +462,7 @@ "_journal/2024-05/2024-05-16.md": "9fdfadc3f9ea6a4418fd0e7066d6b10c", "_journal/2024-05-18.md": "c0b58b28f84b31cea91404f43b0ee40c", "hashing/direct-addressing.md": "f75cc22e74ae974fe4f568a2ee9f951f", - "hashing/index.md": "e3ab1dd55eb7bb97a73b48241a006deb", + "hashing/index.md": "ee4335b307ff1dc740789e9972b19e50", "set/classes.md": "6776b4dc415021e0ef60b323b5c2d436", "_journal/2024-05-19.md": "fddd90fae08fab9bd83b0ef5d362c93a", "_journal/2024-05/2024-05-18.md": "c0b58b28f84b31cea91404f43b0ee40c", @@ -617,7 +617,9 @@ "abstract-rewriting-systems/index.md": "b7486b7635cb0d8bafc2a2f095af90fb", "abstract-rewriting-systems/normal-form.md": "2fff9a1d85bca0a2941a54b0084a0309", "_journal/2024-07-19.md": "ced9d4c4759468885d85efa0b87b7823", - "_journal/2024-07/2024-07-18.md": "237918b58424435959cbc949d01e7932" + "_journal/2024-07/2024-07-18.md": "237918b58424435959cbc949d01e7932", + "_journal/2024-07-20.md": "aa70e639c362764a930c2fa71e030768", + "_journal/2024-07/2024-07-19.md": "e9fe4569f88e1ba9393292bcf092edfc" }, "fields_dict": { "Basic": [ diff --git a/notes/_journal/2024-07-20.md b/notes/_journal/2024-07-20.md new file mode 100644 index 0000000..d9b3414 --- /dev/null +++ b/notes/_journal/2024-07-20.md @@ -0,0 +1,11 @@ +--- +title: "2024-07-20" +--- + +- [x] Anki Flashcards +- [x] KoL +- [x] OGS +- [ ] Sheet Music (10 min.) +- [ ] Korean (Read 1 Story) + +* Begin notes on [[hashing/index#Random Hashing|random hashing]] and, more specifically, [[hashing/index#Universal Hashing|universal hashing]]. \ No newline at end of file diff --git a/notes/_journal/2024-07-19.md b/notes/_journal/2024-07/2024-07-19.md similarity index 100% rename from notes/_journal/2024-07-19.md rename to notes/_journal/2024-07/2024-07-19.md diff --git a/notes/algorithms/order-growth.md b/notes/algorithms/order-growth.md index ccae8cb..76ea5ac 100644 --- a/notes/algorithms/order-growth.md +++ b/notes/algorithms/order-growth.md @@ -760,7 +760,7 @@ END%% %%ANKI Cloze -In $O(g(n))$, bound {1:$0 \leq f(n) \leq cg(n)$} holds for {1:some $c > 0$}. In $o(g(n))$, {2:$0 \leq f(n) < cg(n)$} holds for {2:all $c > 0$}. +In $O(g(n))$, bound {1:$0 \leq f(n) \leq cg(n)$} holds for {1:some $c > 0$}. In $o(g(n))$, bound {2:$0 \leq f(n) < cg(n)$} holds for {2:all $c > 0$}. Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). END%% @@ -1163,7 +1163,7 @@ END%% %%ANKI Cloze -In $\Omega(g(n))$, bound {1:$0 \leq cg(n) \leq f(n)$} holds for {1:some $c > 0$}. In $\omega(g(n))$, {2:$0 \leq cg(n) < f(n)$} holds for {2:all $c > 0$}. +In $\Omega(g(n))$, bound {1:$0 \leq cg(n) \leq f(n)$} holds for {1:some $c > 0$}. In $\omega(g(n))$, bound {2:$0 \leq cg(n) < f(n)$} holds for {2:all $c > 0$}. Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). END%% diff --git a/notes/combinatorics/permutations.md b/notes/combinatorics/permutations.md index 8609cc0..2ca5765 100644 --- a/notes/combinatorics/permutations.md +++ b/notes/combinatorics/permutations.md @@ -469,6 +469,7 @@ Basic What combinatorial problem does $(n)_0$ represent? Back: The number of ways to choose $0$ objects from $n$ choices. Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf). + END%% %%ANKI diff --git a/notes/hashing/index.md b/notes/hashing/index.md index 46c7db4..023f987 100644 --- a/notes/hashing/index.md +++ b/notes/hashing/index.md @@ -203,8 +203,6 @@ END%% An **independent uniform hash function** is the ideal theoretical abstraction. For each possible input $k$ in universe $U$, an output $h(k)$ is produced randomly and independently chosen from range $\{0, 1, \ldots, m - 1\}$. Once a value $h(k)$ is chosen, each subsequent call to $h$ with the same input $k$ yields the same output $h(k)$. -Independent uniform hashing is **universal**, meaning the chance of any two distinct keys colliding is at most $1 / m$. - %%ANKI Basic What is considered an ideal (though theoretical) hash function? @@ -279,7 +277,7 @@ END%% ## Static Hashing -Static hashing refers to providing a single fixed hash function intended to work well on *any* data. Generally speaking, this should not be favored over random hashing. +**Static hashing** refers to providing a single fixed hash function intended to work well on *any* data. Generally speaking, this should not be favored over random hashing. %%ANKI Basic @@ -570,6 +568,213 @@ Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition ( END%% +## Random Hashing + +**Random hashing** refers to choosing a hash function randomly in a way that is independent of the keys being stored. + +%%ANKI +Basic +What does random hashing refer to? +Back: Choosing a hash function randomly and independently of the keys being stored. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random + +END%% + +%%ANKI +Basic +What does random hashing avoid that static hashing doesn't? +Back: Randomization guarantees no single input always evokes worst-case behavior. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random + +END%% + +### Universal Hashing + +Let $\mathscr{H}$ be a finite family of hash functions that map a given universe $U$ of keys into range $\{0, 1, \ldots, m - 1\}$. Such a family is said to be **universal** if $$\forall x, y \in U, x \neq y \Rightarrow |\{h \in \mathscr{H} \mid h(x) = h(y)\}| \leq \frac{|\mathscr{H}|}{m}.$$ + +%%ANKI +Basic +Which of universal hashing or random hashing more general? +Back: Random hashing. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +With respect to universal hashing, what mathematical object is property "universal" attributed to? +Back: A finite set of hash functions. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +What does "family" refer to in the context of universal hashing? +Back: A finite set of hash functions. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +Consider a hash table with $m = 1$ slot. Which hash function families are universal? +Back: Finite families of hash functions mapping to e.g. $\{0\}$. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +A "universal family" refers to a finite set of what? +Back: Hash functions. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +Let $\mathscr{H}$ be a universal family and $h \in \mathscr{H}$. What is the domain of $h$? +Back: The universe of keys. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +Let $\mathscr{H}$ be a universal family and $h \in \mathscr{H}$. What is the codomain of $h$? +Back: $\{0, 1, \ldots, m - 1\}$ (or similar), where $m$ refers to the number of hash table slots. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +Consider universal family $\mathscr{H}$ and universe $U$. What does the following evaluate to? $$|\{h \in \mathscr{H} \mid h(x) = h(y)\}| \text{ for distinct } x, y \in U$$ +Back: A value between $0$ and $|\mathscr{H}|$ inclusive. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +Let $\mathscr{H} = \{h \mid U \rightarrow \{0, 1, \ldots, m - 1\}\}$ be universal. What first-order logic statement holds? +Back: $$\forall x, y \in U, x \neq y \Rightarrow |\{h \in \mathscr{H} \mid h(x) = h(y)\}| \leq \frac{|\mathscr{H}|}{m}$$ +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +Let $\mathscr{H} = \{h \mid U \rightarrow \{0, 1, \ldots, m - 1\}\}$ be universal. What does $m > |\mathscr{H}|$ imply? +Back: For any distinct $x, y \in U$, $h(x) \neq h(y)$ for all $h \in \mathscr{H}$. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +Independent uniform hashing is equivalent to picking a function from what universal family? +Back: $^U\{0, 1, \ldots, m\}$, i.e. the set of functions from $U$ to $\{0, 1, \ldots, m\}$. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +Consider universe $U$ and $\mathscr{H} = \{I_U\}$. Is $\mathscr{H}$ universal? +Back: Yes. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +Consider universe $U$ and $\mathscr{H} = \{I_U\}$. *Why* is $\mathscr{H}$ universal? +Back: Because for any distinct $x, y \in U$, $I_U(x) \neq I_U(y)$. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +Consider universe $U$ and $\mathscr{H} = \{h\}$ where $h(x) = 0$. Is $\mathscr{H}$ universal? +Back: Not necessarily. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +Consider universe $U$ and $\mathscr{H} = \{h\}$ where $h(x) = 0$. *When* is $\mathscr{H}$ universal? +Back: When there exists only one slot in the relevant hash table. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +Consider universe $U$ and $\mathscr{H} = \{h\}$ where $h(x) = 0$. *When* is $\mathscr{H}$ not universal? +Back: When there exists more than one slot in the relevant hash table. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +Let $\mathscr{H} = \{h \mid U \rightarrow \{0, 1, \ldots, m - 1\}\}$ be universal. What number decreases as $m$ increases? +Back: The number of permitted conflicts for each $h \in \mathscr{H}$. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +Let $\mathscr{H} = \{h \mid U \rightarrow \{0, 1, \ldots, m - 1\}\}$ be universal. What number increases as $|\mathscr{H}|$ increases? +Back: The number of permitted conflicts for each $h \in \mathscr{H}$. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +Is $\varnothing$ a universal family? +Back: Yes. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + +%%ANKI +Basic +How might we redefine "universal" to prevent $\varnothing \subseteq \{h \mid h \colon U \rightarrow \{0, 1, \ldots, m - 1\}$ being considered universal? +Back: $$\forall x, y \in U, x \neq y \Rightarrow \frac{|\varnothing|}{|\varnothing|} \leq \frac{1}{m}$$ +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +Tags: hashing::random hashing::universal + +END%% + ## Bibliography -* Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). \ No newline at end of file +* Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). +* “Universal Hashing,” in _Wikipedia_, April 18, 2024, [https://en.wikipedia.org/w/index.php?title=Universal_hashing](https://en.wikipedia.org/w/index.php?title=Universal_hashing&oldid=1219538176). \ No newline at end of file diff --git a/notes/logic/equiv-trans.md b/notes/logic/equiv-trans.md index c9530d1..4a23e9e 100644 --- a/notes/logic/equiv-trans.md +++ b/notes/logic/equiv-trans.md @@ -224,190 +224,11 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in END%% -## Substitution +## Selectors -**Textual substitution** refers to the simultaneous replacement of a free identifier with an expression, introducing parentheses as necessary. This concept is just the [[#Equivalence Rules|Substitution Rule]] with different notation. Let $\bar{x}$ denote a list of distinct identifiers. If $\bar{e}$ is a list of expressions of the same length as $\bar{x}$, then simultaneous substitution of $\bar{x}$ by $\bar{e}$ in expression $E$ is denoted as $$E_{\bar{e}}^{\bar{x}}$$ -Note that simultaneous substitution is different than sequential substitution. +A **selector** denotes a finite sequence of subscript expressions, each enclosed in brackets. $\epsilon$ denotes the empty selector. For example, variable $x$ is equivalently denoted as $x \circ \epsilon$ whereas for array $b$, $b[i]$ is equivalently denoted as $b \circ [i]$. -%%ANKI -Basic -Textual substitution is derived from what equivalence rule? -Back: The substitution rule. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What term refers to $x$ in textual substitution $E_e^x$? -Back: The reference. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What term refers to $e$ in textual substitution $E_e^x$? -Back: The expression. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What term refers to both $x$ and $e$ together in textual substitution $E_e^x$? -Back: The reference-expression pair. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What identifier is guaranteed to not occur freely in $E_e^x$? -Back: N/A. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What identifier is guaranteed to not occur freely in $E_{s(e)}^x$? -Back: $x$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -*Why* does $x$ not occur freely in $E_{s(e)}^x$? -Back: Because $s(e)$ evaluates to a constant proposition. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the role of $E$ in textual substitution $E_e^x$? -Back: It is the expression in which free occurrences of $x$ are replaced. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the role of $e$ in textual substitution $E_e^x$? -Back: It is the expression that is evaluated and substituted into $E$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the role of $x$ in textual substitution $E_e^x$? -Back: It is the identifier matching free occurrences in $E$ that are replaced. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -How is textual substitution $E_e^x$ interpreted as a function? -Back: As $E(e)$, where $E$ is a function of $x$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Why does Gries prefer notation $E_e^x$ over e.g. $E(e)$? -Back: The former indicates the identifier to replace. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What two scenarios ensure $E_e^x = E$ is an equivalence? -Back: $x = e$ or no free occurrences of $x$ exist in $E$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -If $x \neq e$, why might $E_e^x = E$ be an equivalence despite $x$ existing in $E$? -Back: The only occurrences of $x$ in $E$ may be bound. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is required for $E_e^x$ to be valid? -Back: Substitution must result in a syntactically valid expression. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the result of the following? $$(x < y \land (\forall i : 0 \leq i < n : b[i] < y))_z^x$$ -Back: $$(z < y \land (\forall i : 0 \leq i < n : b[i] < y))$$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the result of the following? $$(x < y \land (\forall i : 0 \leq i < n : b[i] < y))_z^y$$ -Back: $$(x < z \land (\forall i : 0 \leq i < n : b[i] < z))$$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the result of the following? $$(x < y \land (\forall i : 0 \leq i < n : b[i] < y))_z^i$$ -Back: $$(x < y \land (\forall i : 0 \leq i < n : b[i] < y))$$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -In textual substitution, what does e.g. $\bar{x}$ denote? -Back: A list of *distinct* identifiers. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the role of $E$ in textual substitution $E_{\bar{e}}^{\bar{x}}$? -Back: It is the expression in which free occurrences of $\bar{x}$ are replaced. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the role of $\bar{e}$ in textual substitution $E_{\bar{e}}^{\bar{x}}$? -Back: It is the expressions that are substituted into $E$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the role of $\bar{x}$ in textual substitution $E_{\bar{e}}^{\bar{x}}$? -Back: It is the distinct identifiers matching free occurrences in $E$ that are replaced. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -### Arrays - -An array can be seen as a function from the **domain** of the array to the subscripted values found in the array. We denote array subscript assignment similarly to state identifier assignment: $$(b; i{:}e)[j] = \begin{cases} i = j \rightarrow e \\ i \neq j \rightarrow b[j] \end{cases}$$ +**Selector update** syntax allows specifying a new value with previous subscripted values overridden. For instance, $(b; i{:}e)$ denotes $b$ with $b[i]$ now referring to $e$. More formally, for any $j \in \mathop{domain}(b)$, $$(b; i{:}e)[j] = \begin{cases} i = j \rightarrow e \\ i \neq j \rightarrow b[j] \end{cases}$$ %%ANKI Basic @@ -640,9 +461,7 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in END%% -### Selector Update Syntax - -A **selector** denotes a finite sequence of subscript expressions, each enclosed in brackets. $\epsilon$ denotes the empty selector. We can generalize the above to all variable types as follows: $$\begin{align*} (b; \epsilon{:}g) & = g \\ (b; [i] \circ s{:}e)[j] & = \begin{cases} i \neq j \rightarrow b[j] \\ i = j \rightarrow (b[j]; s{:}e) \end{cases} \end{align*}$$ +Generalizing further to all variable types $x$, $$\begin{align*} (x; \epsilon{:}e) & = e \\ (x; [i] {\circ} s{:}e)[j] & = \begin{cases} i \neq j \rightarrow x[j] \\ i = j \rightarrow (x[j]; s{:}e) \end{cases} \end{align*}$$ %%ANKI Basic @@ -654,8 +473,8 @@ END%% %%ANKI Basic -Given valid expression $(b; [i]{\circ}s{:}e)$, what can be said about $i$? -Back: $i$ is in the domain of $b$. +Given valid expression $(x; [i]{\circ}s{:}e)$, what can be said about $i$? +Back: $i$ is in the domain of $x$. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. END%% @@ -663,14 +482,14 @@ END%% %%ANKI Basic What is the base case of selector update syntax? -Back: $(b; \epsilon{:}g) = g$ +Back: $(x; \epsilon{:}e) = e$ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. END%% %%ANKI Basic -The null selector is usually denoted as what? +How is the null selector usually denoted? Back: $\epsilon$ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. @@ -679,7 +498,7 @@ END%% %%ANKI Basic The null selector is the identity element of what operation? -Back: Concatenation of sequences of subscripts. +Back: Subscript sequence concatenation. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. END%% @@ -702,7 +521,7 @@ END%% %%ANKI Basic -What assignment expression (i.e. using `:=`) is simpler but equivalent to $x := (x; \epsilon{:}e)$? +How is command $x := (x; \epsilon{:}e)$ more compactly rewritten? Back: $x := e$ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. @@ -772,6 +591,172 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in END%% +## Substitution + +**Textual substitution** refers to the replacement of a [[pred-logic#Identifiers|free]] identifier with an expression, introducing parentheses as necessary. This concept amounts to the [[#Equivalence Rules|Substitution Rule]] with different notation. + +%%ANKI +Basic +Textual substitution is derived from what equivalence rule? +Back: The substitution rule. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +### Simple + +If $x$ denotes a variable and $e$ an expression, substitution of $x$ by $e$ is denoted as $$\large{E_e^x}$$ + +%%ANKI +Basic +What term refers to $x$ in textual substitution $E_e^x$? +Back: The reference. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What term refers to $e$ in textual substitution $E_e^x$? +Back: The expression. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What term refers to both $x$ and $e$ together in textual substitution $E_e^x$? +Back: The reference-expression pair. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What identifier is guaranteed to not occur freely in $E_e^x$? +Back: N/A. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What identifier is guaranteed to not occur freely in $E_{s(e)}^x$? +Back: $x$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +*Why* does $x$ not occur freely in $E_{s(e)}^x$? +Back: Because $s(e)$ evaluates to a constant proposition. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the role of $E$ in textual substitution $E_e^x$? +Back: It is the expression in which free occurrences of $x$ are replaced. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the role of $e$ in textual substitution $E_e^x$? +Back: It is the expression that is evaluated and substituted into $E$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the role of $x$ in textual substitution $E_e^x$? +Back: It is the identifier matching free occurrences in $E$ that are replaced. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is textual substitution $E_e^x$ interpreted as a function? +Back: As $E(e)$, where $E$ is a function of $x$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Why does Gries prefer notation $E_e^x$ over e.g. $E(e)$? +Back: The former indicates the identifier to replace. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What two scenarios ensure $E_e^x = E$ is an equivalence? +Back: $x = e$ or no free occurrences of $x$ exist in $E$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +If $x \neq e$, why might $E_e^x = E$ be an equivalence despite $x$ existing in $E$? +Back: The only occurrences of $x$ in $E$ may be bound. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is required for $E_e^x$ to be valid? +Back: Substitution must result in a syntactically valid expression. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the result of the following? $$(x < y \land (\forall i : 0 \leq i < n : b[i] < y))_z^x$$ +Back: $$(z < y \land (\forall i : 0 \leq i < n : b[i] < y))$$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the result of the following? $$(x < y \land (\forall i : 0 \leq i < n : b[i] < y))_z^y$$ +Back: $$(x < z \land (\forall i : 0 \leq i < n : b[i] < z))$$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the result of the following? $$(x < y \land (\forall i : 0 \leq i < n : b[i] < y))_z^i$$ +Back: $$(x < y \land (\forall i : 0 \leq i < n : b[i] < y))$$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +### General + +We can generalize textual substitution to operate on a vector of reference-expression pairs, where each reference corresponds to some identifier concatenated with a selector. Let $\bar{x} = \langle x_1, \ldots, x_n \rangle$ denote a vector of identifiers concatenated with selectors and $\bar{e} = \langle e_1, \ldots, e_n \rangle$ denote a vector of expressions. Then textual substitition of $\bar{x}$ with $\bar{e}$ in expression $E$ is denoted as $$\large{E_{\bar{e}}^{\bar{x}}}$$ + +Substitution is defined recursively as follows: + +1. If each $x_i$ is a distinct identifier with a null selector, then $E_{\bar{e}}^{\bar{x}}$ is the simultaneous substitution of $\bar{x}$ with $\bar{e}$. +2. Adjacent reference-expression pairs may be permuted as long as they begin with different identifiers. That is, for all distinct $b$ and $c$, $$\Large{E_{\bar{e}, \,f, \,h, \,\bar{g}}^{\bar{x}, \,b, \,c, \,\bar{y}} = E_{\bar{x}, \,h, \,f, \,\bar{g}}^{\bar{x}, \,c, \,b, \,\bar{y}}}$$ +3. Multiple assignments to subparts of an object $b$ can be viewed as a single assignment to $b$. That is, provided $b$ does not begin any of the $x_i$, $$\Large{E_{e_1, \,\ldots, \,e_m, \,\bar{g}}^{b \circ s_1, \,\ldots, \,b \circ s_m, \,\bar{x}} = E_{(b; \,s_1{:}e_1; \,\cdots; \,s_m{:}e_m), \,\bar{g}}^{b, \,\bar{x}}}$$ + +Note that simultaneous substitution is different from sequential substitution. + +TODO + ### Theorems * $(E_u^x)_v^x = E_{u_v^x}^x$ @@ -933,7 +918,7 @@ END%% %%ANKI Basic When is $(E_{\bar{u}}^{\bar{x}})_{\bar{x}}^{\bar{u}} = E$ guaranteed to be an equivalence? -Back: When $\bar{x}$ and $\bar{u}$ are all distinct identifiers. +Back: When $\bar{x}$ and $\bar{u}$ refer to distinct identifiers. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. END%% diff --git a/notes/programming/pred-trans.md b/notes/programming/pred-trans.md index 63a68f0..6a1ade0 100644 --- a/notes/programming/pred-trans.md +++ b/notes/programming/pred-trans.md @@ -498,7 +498,7 @@ END%% ## Commands -### skip +### Skip For any predicate $R$, $wp(skip, R) = R$. @@ -525,7 +525,7 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in END%% -### abort +### Abort For any predicate $R$, $wp(abort, R) = F$. @@ -622,7 +622,9 @@ 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$$ +#### Simple + +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) \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 @@ -644,7 +646,7 @@ 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$ +Back: $wp(''x \coloneqq e'', R) = domain(e) \textbf{ cand } R_e^x$ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. END%% @@ -676,7 +678,7 @@ 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$ +Back: $wp(''x \coloneqq e'', R) = domain(e) \textbf{ cand } R_e^x$ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. END%% @@ -753,6 +755,10 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in END%% +#### General + +TODO + ## 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/index.md b/notes/set/index.md index d30ea7f..2f981fe 100644 --- a/notes/set/index.md +++ b/notes/set/index.md @@ -276,7 +276,7 @@ END%% %%ANKI Cloze -$\exists A \in B, uFx$ is equivalently written as $x \in$ {$\{v \mid \exists A \in B, uFv\}$}. +$\exists u \in A, uFx$ is equivalently written as $x \in$ {$\{v \mid \exists u \in A, uFv\}$}. Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977). END%%