r
/
notebook
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Prep for general textual substitution and assignment.

c-declarations
Joshua Potter 2024-07-20 09:41:15 -06:00
parent 992dff94f4
commit 2ab913f70e
9 changed files with 421 additions and 211 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json
View File

@ -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": [

11
notes/_journal/2024-07-20.md Normal file
View File

@ -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]].

0
notes/_journal/2024-07-19.md → notes/_journal/2024-07/2024-07-19.md
View File

4
notes/algorithms/order-growth.md
View File

@ -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).
<!--ID: 1709519002359-->
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).
<!--ID: 1709519002420-->
END%%

1
notes/combinatorics/permutations.md
View File

@ -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).
<!--ID: 1721475697031-->
END%%
%%ANKI

213
notes/hashing/index.md
View File

@ -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 (
<!--ID: 1720891800649-->
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
<!--ID: 1721482558926-->
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
<!--ID: 1721482558932-->
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
<!--ID: 1721482558937-->
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
<!--ID: 1721482558943-->
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
<!--ID: 1721482558948-->
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
<!--ID: 1721482558957-->
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
<!--ID: 1721482558964-->
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
<!--ID: 1721482558970-->
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
<!--ID: 1721482558977-->
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
<!--ID: 1721482558983-->
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
<!--ID: 1721482558988-->
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
<!--ID: 1721482558992-->
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
<!--ID: 1721482559002-->
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
<!--ID: 1721482559008-->
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
<!--ID: 1721482559014-->
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
<!--ID: 1721482559021-->
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
<!--ID: 1721482559031-->
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
<!--ID: 1721482559043-->
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
<!--ID: 1721482559053-->
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
<!--ID: 1721482559059-->
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
<!--ID: 1721482559064-->
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
<!--ID: 1721482559069-->
END%%
## Bibliography
* Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022).
* 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).

369
notes/logic/equiv-trans.md
View File

@ -224,190 +224,11 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in
<!--ID: 1707316276203-->
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.
<!--ID: 1707762304123-->
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.
<!--ID: 1707939006275-->
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.
<!--ID: 1707939006283-->
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.
<!--ID: 1707939006288-->
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.
<!--ID: 1707937867036-->
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.
<!--ID: 1707937867039-->
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.
<!--ID: 1707937867042-->
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.
<!--ID: 1708347042194-->
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.
<!--ID: 1708347042199-->
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.
<!--ID: 1708347042203-->
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.
<!--ID: 1707762304130-->
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.
<!--ID: 1707762304132-->
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.
<!--ID: 1707762304133-->
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.
<!--ID: 1707762304135-->
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.
<!--ID: 1707762304137-->
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.
<!--ID: 1707762304139-->
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.
<!--ID: 1707762304140-->
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.
<!--ID: 1707762304141-->
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.
<!--ID: 1707937867046-->
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.
<!--ID: 1707762304126-->
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.
<!--ID: 1707762304127-->
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.
<!--ID: 1707762304129-->
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
<!--ID: 1714336860005-->
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.
<!--ID: 1714395640893-->
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.
<!--ID: 1714395640901-->
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.
<!--ID: 1714395640904-->
@ -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.
<!--ID: 1714395640907-->
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.
<!--ID: 1714395640917-->
@ -772,6 +591,172 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in
<!--ID: 1714395640953-->
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.
<!--ID: 1707762304123-->
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.
<!--ID: 1707939006275-->
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.
<!--ID: 1707939006283-->
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.
<!--ID: 1707939006288-->
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.
<!--ID: 1707937867036-->
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.
<!--ID: 1707937867039-->
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.
<!--ID: 1707937867042-->
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.
<!--ID: 1708347042194-->
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.
<!--ID: 1708347042199-->
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.
<!--ID: 1708347042203-->
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.
<!--ID: 1707762304130-->
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.
<!--ID: 1707762304132-->
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.
<!--ID: 1707762304133-->
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.
<!--ID: 1707762304135-->
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.
<!--ID: 1707762304137-->
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.
<!--ID: 1707762304139-->
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.
<!--ID: 1707762304140-->
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.
<!--ID: 1707762304141-->
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.
<!--ID: 1707939006297-->
END%%

16
notes/programming/pred-trans.md
View File

@ -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
<!--ID: 1716810300113-->
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.
<!--ID: 1720447926794-->
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.
<!--ID: 1720447926813-->
END%%
@ -753,6 +755,10 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in
<!--ID: 1720447926858-->
END%%
#### General
TODO
## Bibliography
* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

2
notes/set/index.md
View File

@ -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).
<!--ID: 1720369624735-->
END%%