diff --git a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json index 10bbf8a..602ba69 100644 --- a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json +++ b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json @@ -114,7 +114,9 @@ "nearly-complete-tree.png", "non-nearly-complete-tree.png", "perfect-tree.png", - "non-complete-tree.png" + "non-complete-tree.png", + "max-heap-tree.png", + "max-heap-array.png" ], "File Hashes": { "algorithms/index.md": "3ac071354e55242919cc574eb43de6f8", @@ -153,7 +155,7 @@ "_journal/2024-02-02.md": "a3b222daee8a50bce4cbac699efc7180", "_journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb", "_journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970", - "logic/equiv-trans.md": "5d68be4120e7f79e12c35fafeddaf1a1", + "logic/equiv-trans.md": "63515dfd471653bc0c8bc4eca66ccaf8", "_journal/2024-02-07.md": "8d81cd56a3b33883a7706d32e77b5889", "algorithms/loop-invariants.md": "cbefc346842c21a6cce5c5edce451eb2", "algorithms/loop-invariant.md": "3b390e720f3b2a98e611b49a0bb1f5a9", @@ -201,7 +203,7 @@ "_journal/2024-02/2024-02-14.md": "aa009f9569e175a8104b0537ebcc5520", "_journal/2024-02-16.md": "5cc129254afd553829be3364facd23db", "_journal/2024-02/2024-02-15.md": "16cb7563d404cb543719b7bb5037aeed", - "algebra/floor-ceiling.md": "ffffdd893398da842be2e4337c16bbf7", + "algebra/floor-ceiling.md": "412e4fdc424cb17fd818688857c4b5b3", "algebra/index.md": "90b842eb694938d87c7c68779a5cacd1", "algorithms/binary-search.md": "8533a05ea372e007ab4e8a36fd2772a9", "_journal/2024-02-17.md": "7c37cb10515ed3d2f5388eaf02a67048", @@ -245,7 +247,7 @@ "filesystems/cas.md": "d41c0d2e943adecbadd10a03fd1e4274", "git/objects.md": "c6b7e6a26666386790d25d4ece38175d", "git/index.md": "83d2d95fc549d9e8436946c7bd058d15", - "encoding/integer.md": "73c42283ff8c3a1d4efb9f9644a4cf3b", + "encoding/integer.md": "2ab21152b9468f547ebee496e03bc410", "_journal/2024-02-29.md": "f610f3caed659c1de3eed5f226cab508", "_journal/2024-02/2024-02-28.md": "7489377c014a2ff3c535d581961b5b82", "_journal/2024-03-01.md": "a532486279190b0c12954966cbf8c3fe", @@ -315,7 +317,7 @@ "x86-64/declarations.md": "75bc7857cf2207a40cd7f0ee056af2f2", "x86-64/instructions.md": "d783bad8dd77748fb412715541cb844d", "git/refs.md": "954fc69004aa65b358ec5ce07c1435ce", - "set/trees.md": "6c1a245f6b25838c519f5c9bcf96c369", + "set/trees.md": "0d21b947917498f107da140cc9fb93a7", "_journal/2024-03-24.md": "1974cdb9fc42c3a8bebb8ac76d4b1fd6", "_journal/2024-03/2024-03-23.md": "ad4e92cc2bf37f174a0758a0753bf69b", "_journal/2024-03/2024-03-22.md": "a509066c9cd2df692549e89f241d7bd9", @@ -371,7 +373,19 @@ "_journal/2024-04/2024-04-23.md": "20514052da91b06b979cacb3da758837", "_journal/2024-04-25.md": "10c98531cb90a6bc940ea7ae3342f98b", "_journal/2024-04/2024-04-24.md": "4cb04e0dea56e0b471fc0e428471a390", - "algorithms/heaps.md": "4235ec90b6e251fc992906e0f1fe69e7" + "algorithms/heaps.md": "b12c70ec85e514ce912821d133d116d4", + "_journal/2024-04-26.md": "3ce37236a9e09e74b547a4f7231df5f0", + "_journal/2024-04/2024-04-25.md": "5a81123af29f8ebf0a0d28f820a3a52e", + "_journal/2024-04-28.md": "46726bf76a594b987c63ba8b9b6d13d3", + "_journal/2024-04/2024-04-27.md": "b0f3753821c232bf819b00fb49415bd0", + "_journal/2024-04/2024-04-26.md": "3ce37236a9e09e74b547a4f7231df5f0", + "algorithms/sorting/heapsort.md": "e0d368882a8f33d2f42bd3ead4e3914d", + "_journal/2024-04-29.md": "7888f4e9497c9d8bd6f4aa759d9abc4d", + "_journal/2024-04/2024-04-28.md": "b34a9fe3bccb1f224b96ca00e78ad061", + "programming/assertions.md": "bdef9b934d8db94169d6befbc02f33d2", + "programming/text-sub.md": "003b8c32ae2f6767cb0d900f85196e67", + "programming/equiv-trans.md": "fbadd593688e364ea92f74f23e54bcfc", + "programming/index.md": "bb082325e269a95236aa6aff9307fe59" }, "fields_dict": { "Basic": [ diff --git a/notes/_journal/2024-04-29.md b/notes/_journal/2024-04-29.md new file mode 100644 index 0000000..8655198 --- /dev/null +++ b/notes/_journal/2024-04-29.md @@ -0,0 +1,14 @@ +--- +title: "2024-04-29" +--- + +- [x] Anki Flashcards +- [x] KoL +- [ ] Sheet Music (10 min.) +- [ ] Go (1 Life & Death Problem) +- [ ] Korean (Read 1 Story) +- [ ] Interview Prep (1 Practice Problem) +- [x] Log Work Hours (Max 3 hours) + +* Notes on chapter 5.3 of "The Science of Programming". Covered nested arrays. +* Read chapter 6 of "The Science of Programming". Still need to convert into notes though. \ No newline at end of file diff --git a/notes/_journal/2024-04/2024-04-26.md b/notes/_journal/2024-04/2024-04-26.md new file mode 100644 index 0000000..71f36fd --- /dev/null +++ b/notes/_journal/2024-04/2024-04-26.md @@ -0,0 +1,11 @@ +--- +title: "2024-04-26" +--- + +- [x] Anki Flashcards +- [x] KoL +- [ ] Sheet Music (10 min.) +- [ ] Go (1 Life & Death Problem) +- [ ] Korean (Read 1 Story) +- [ ] Interview Prep (1 Practice Problem) +- [x] Log Work Hours (Max 3 hours) \ No newline at end of file diff --git a/notes/_journal/2024-04/2024-04-27.md b/notes/_journal/2024-04/2024-04-27.md new file mode 100644 index 0000000..ac0207c --- /dev/null +++ b/notes/_journal/2024-04/2024-04-27.md @@ -0,0 +1,14 @@ +--- +title: "2024-04-27" +--- + +- [x] Anki Flashcards +- [x] KoL +- [ ] Sheet Music (10 min.) +- [ ] Go (1 Life & Death Problem) +- [ ] Korean (Read 1 Story) +- [ ] Interview Prep (1 Practice Problem) +- [ ] Log Work Hours (Max 3 hours) + +* Hide-and-Seek Application + * Finished most game logic. Began working on theming. \ No newline at end of file diff --git a/notes/_journal/2024-04/2024-04-28.md b/notes/_journal/2024-04/2024-04-28.md new file mode 100644 index 0000000..e8b7a44 --- /dev/null +++ b/notes/_journal/2024-04/2024-04-28.md @@ -0,0 +1,18 @@ +--- +title: "2024-04-28" +--- + +- [x] Anki Flashcards +- [x] KoL +- [ ] Sheet Music (10 min.) +- [ ] Go (1 Life & Death Problem) +- [ ] Korean (Read 1 Story) +- [ ] Interview Prep (1 Practice Problem) +- [x] Log Work Hours (Max 3 hours) + +* Hide-and-Seek Application + * Added booting and teardown game server logic. + * Begin theming according to Fort Collins vendor guidelines. +* Notes on chapter 5.2 in "The Science of Programming". +* Notes on floor/ceiling identities associated with complete $k$-ary trees. +* Start adding notes/flashcards on heaps and heapsort. \ No newline at end of file diff --git a/notes/algebra/floor-ceiling.md b/notes/algebra/floor-ceiling.md index 8bfdfe5..d33bc59 100644 --- a/notes/algebra/floor-ceiling.md +++ b/notes/algebra/floor-ceiling.md @@ -157,7 +157,7 @@ END%% %%ANKI Basic What C operator corresponds to ceiling division? -Back: None. +Back: N/A. Reference: Ronald L. Graham, Donald Ervin Knuth, and Oren Patashnik, *Concrete Mathematics: A Foundation for Computer Science*, 2nd ed (Reading, Mass: Addison-Wesley, 1994). END%% @@ -352,6 +352,136 @@ Reference: Ronald L. Graham, Donald Ervin Knuth, and Oren Patashnik, *Concrete M END%% +## Identities + +For integers $x$ and $y > 0$, $$\begin{align*} \left\lfloor \frac{x}{y} \right\rfloor & = \left\lceil \frac{x}{y} - \frac{y - 1}{y} \right\rceil \\ \left\lceil \frac{x}{y} \right\rceil & = \left\lfloor \frac{x}{y} + \frac{y - 1}{y} \right\rfloor \end{align*}$$ + +%%ANKI +Basic +If $n$ is even, what integer value does $\lfloor n / 2 \rfloor$ evaluate to? +Back: $n / 2$ +Reference: Ronald L. Graham, Donald Ervin Knuth, and Oren Patashnik, *Concrete Mathematics: A Foundation for Computer Science*, 2nd ed (Reading, Mass: Addison-Wesley, 1994). + +END%% + +%%ANKI +Basic +If $n$ is odd, what integer value does $\lfloor n / 2 \rfloor$ evaluate to? +Back: $(n - 1) / 2$ +Reference: Ronald L. Graham, Donald Ervin Knuth, and Oren Patashnik, *Concrete Mathematics: A Foundation for Computer Science*, 2nd ed (Reading, Mass: Addison-Wesley, 1994). + +END%% + +%%ANKI +Basic +If $n$ is even, what integer value does $\lceil n / 2 \rceil$ evaluate to? +Back: $n / 2$ +Reference: Ronald L. Graham, Donald Ervin Knuth, and Oren Patashnik, *Concrete Mathematics: A Foundation for Computer Science*, 2nd ed (Reading, Mass: Addison-Wesley, 1994). + +END%% + +%%ANKI +Basic +If $n$ is odd, what integer value does $\lceil n / 2 \rceil$ evaluate to? +Back: $(n + 1) / 2$ +Reference: Ronald L. Graham, Donald Ervin Knuth, and Oren Patashnik, *Concrete Mathematics: A Foundation for Computer Science*, 2nd ed (Reading, Mass: Addison-Wesley, 1994). + +END%% + +%%ANKI +Basic +Given integers $x$ and $y > 0$, what value of $Bias$ satisfies the following identity? $$\left\lceil \frac{x}{y} \right\rceil = \left\lfloor \frac{x}{y} + Bias \right\rfloor$$ +Back: $(y - 1) / y$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Given integers $x$ and $y > 0$, what value of $Bias$ satisfies the following identity? $$\left\lceil \frac{x}{y} \right\rceil = \left\lfloor \frac{x + Bias}{y} \right\rfloor$$ +Back: $(y - 1)$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Given integers $x$ and $y > 0$, what operator satisfies the following identity? $$\left\lceil \frac{x}{y} \right\rceil = \left\lfloor \frac{x}{y} \;\square\; \frac{y - 1}{y} \right\rfloor$$ +Back: $+$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +What intuition explains why the following identity holds for integers $x$ and $y > 0$? $$\left\lceil \frac{x}{y} \right\rceil = \left\lfloor \frac{x}{y} + \frac{y - 1}{y} \right\rfloor$$ +Back: $(y - 1) / y$ only affects the RHS if and only if $x / y$ is not an integer. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Given integers $x$ and $y > 0$, what value of $Bias$ satisfies the following identity? $$\left\lfloor \frac{x}{y} \right\rfloor = \left\lceil \frac{x}{y} - Bias \right\rceil$$ +Back: $(y - 1) / y$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Given integers $x$ and $y > 0$, what value of $Bias$ satisfies the following identity? $$\left\lfloor \frac{x}{y} \right\rfloor = \left\lceil \frac{x - Bias}{y} \right\rceil$$ +Back: $(y - 1)$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +Given integers $x$ and $y > 0$, what operator satisfies the following identity? $$\left\lfloor \frac{x}{y} \right\rfloor = \left\lceil \frac{x}{y} \;\square\; \frac{y - 1}{y} \right\rceil$$ +Back: $-$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +What intuition explains why the following identity holds for integers $x$ and $y > 0$? $$\left\lfloor \frac{x}{y} \right\rfloor = \left\lceil \frac{x}{y} - \frac{y - 1}{y} \right\rceil$$ +Back: $(y - 1) / y$ only affects the RHS if and only if $x / y$ is not an integer. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Cloze +For any integer $n$, floor expression {$\lfloor n / 2 \rfloor$} is equal to ceiling expression {$\lceil (n - 1) / 2 \rceil$}. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Cloze +For any integer $n$, ceiling expression {$\lceil n / 2 \rceil$} is equal to floor expression {$\lfloor (n + 1) / 2 \rfloor$}. +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +What identity generalizes the following? $$\left\lfloor \frac{n}{2} \right\rfloor = \left\lceil \frac{n - 1}{2} \right\rceil$$ +Back: $$\left\lfloor \frac{n}{d} \right\rfloor = \left\lceil \frac{n - (d - 1)}{d} \right\rceil$$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +What identity generalizes the following? $$\left\lceil \frac{n}{2} \right\rceil = \left\lfloor \frac{n + 1}{2} \right\rfloor$$ +Back: $$\left\lceil \frac{n}{d} \right\rceil = \left\lfloor \frac{n + (d - 1)}{d} \right\rfloor$$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + ## Bibliography * Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. diff --git a/notes/algorithms/heaps.md b/notes/algorithms/heaps.md index 556c59e..b9713f2 100644 --- a/notes/algorithms/heaps.md +++ b/notes/algorithms/heaps.md @@ -9,4 +9,144 @@ tags: ## Overview -TODO \ No newline at end of file +The **binary heap** data structure is an array object that can be viewed as a [[trees#Positional Trees|complete binary tree]]. + +%%ANKI +Cloze +A binary heap is an {array} that can be viewed as a {binary tree}. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +Is the following a valid binary heap? +![[perfect-tree.png]] +Back: Yes. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +Is the following a valid binary heap? +![[complete-tree.png]] +Back: Yes. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +Is the following a valid binary heap? +![[non-complete-tree.png]] +Back: No. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +Why can't the following be a binary heap? +![[non-complete-tree.png]] +Back: A heap is equivalently viewed as a *complete* binary tree. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +What two sizes are associated with binary heaps? +Back: The number of valid elements and the size of the underlying array. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +What are the two kinds of binary heaps? +Back: Max-heaps and min-heaps. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +What is the max-heap property? +Back: Every parent node is greater than or equal to its children in value. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +Where is the largest element of a max-heap? +Back: At the root. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +Where is the smallest element of a max-heap? +Back: At the leaves. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +What is the min-heap property? +Back: Every parent node is less than or equal to its children in value. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +Where is the smallest element of a min-heap? +Back: At the root. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +Where is the largest element of a min-heap? +Back: At the leaves. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +How is the following binary heap viewed as an array? +![[max-heap-tree.png]] +Back: +![[max-heap-array.png]] +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +How is the following binary heap instead viewed as a binary tree? +![[max-heap-array.png]] +Back: +![[max-heap-tree.png]] +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +What kind of binary heap is the following? +![[max-heap-array.png]] +Back: A max-heap. +Reference: Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +## Bibliography + +* Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). \ No newline at end of file diff --git a/notes/algorithms/images/heapsort.gif b/notes/algorithms/images/heapsort.gif new file mode 100644 index 0000000..2f780bf Binary files /dev/null and b/notes/algorithms/images/heapsort.gif differ diff --git a/notes/algorithms/images/max-heap-array.png b/notes/algorithms/images/max-heap-array.png new file mode 100644 index 0000000..e99f4f1 Binary files /dev/null and b/notes/algorithms/images/max-heap-array.png differ diff --git a/notes/algorithms/images/max-heap-tree.png b/notes/algorithms/images/max-heap-tree.png new file mode 100644 index 0000000..e95f27a Binary files /dev/null and b/notes/algorithms/images/max-heap-tree.png differ diff --git a/notes/algorithms/sorting/heapsort.md b/notes/algorithms/sorting/heapsort.md new file mode 100644 index 0000000..7d6015d --- /dev/null +++ b/notes/algorithms/sorting/heapsort.md @@ -0,0 +1,64 @@ +--- +title: Heapsort +TARGET DECK: Obsidian::STEM +FILE TAGS: algorithm::sorting +tags: + - algorithm + - sorting +--- + +## Overview + +Property | Value +----------- | -------- +Best Case | - +Worst Case | - +Avg. Case | - +Aux. Memory | - +Stable | - +Adaptive | - + +![[heapsort.gif]] + +```c +inline int left_child(int i) { return (i << 1) + 1; } +inline int right_child(int i) { return (i << 1) + 2; } + +void max_heapify(int n, int H[static n], int i) { + while (true) { + int lc = left_child(i); + int rc = right_child(i); + int next = i; + + if (lc < n && H[next] < H[lc]) { + next = lc; + } + if (rc < n && H[next] < H[rc]) { + next = rc; + } + if (next == i) { + return; + } + swap(H, i, next); + i = next; + } +} + +void build_max_heap(int n, int H[static n]) { + for (int i = n / 2 - 1; i >= 0; --i) { + max_heapify(n, H, i); + } +} + +void heapsort(int n, int H[static n]) { + build_max_heap(n, H); + while (n > 1) { + swap(A, 0, --n); + max_heapify(n, A, 0); + } +} +``` + +## Bibliography + +* Thomas H. Cormen et al., Introduction to Algorithms, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). \ No newline at end of file diff --git a/notes/encoding/integer.md b/notes/encoding/integer.md index 0220934..80acaa2 100644 --- a/notes/encoding/integer.md +++ b/notes/encoding/integer.md @@ -2114,6 +2114,67 @@ Tags: c17 END%% +%%ANKI +Basic +Assuming no overflow, rewrite expression `x >> k` to instead yield $\lceil x / 2^k \rceil$. +Back: `(x + (1 << k) - 1) >> k` +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. +Tags: c17 + +END%% + +%%ANKI +Basic +Assuming no overflow, what is the result of `(x + (1 << k) - 1) >> k`? +Back: $\lceil x / 2^k \rceil$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. +Tags: c17 + +END%% + +%%ANKI +Basic +What value of $Bias$ satisfies the following identity? $$\left\lceil \frac{x}{2^k} \right\rceil = \left\lfloor \frac{x}{2^k} + Bias \right\rfloor$$ +Back: $(2^k - 1) / 2^k$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +What value of $Bias$ satisfies the following identity? $$\left\lceil \frac{x}{2^k} \right\rceil = \left\lfloor \frac{x + Bias}{2^k} \right\rfloor$$ +Back: $2^k - 1$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. + +END%% + +%%ANKI +Basic +What floor/ceiling identity does expression `(x + (1 << k) - 1) >> k` exploit? +Back: $$\left\lceil \frac{x}{y} \right\rceil = \left\lfloor \frac{x + y - 1}{y} \right\rfloor$$ +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. +Tags: c17 + +END%% + +%%ANKI +Basic +In two's-complement, how do we use `>>` to perform integer division of `x > 0` by $2^k$? +Back: `x >> k` +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. +Tags: c17 + +END%% + +%%ANKI +Basic +In two's-complement, how do we use `>>` to perform integer division of `x < 0` by $2^k$? +Back: `(x + (1 << k) - 1) >> k` +Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. +Tags: c17 + +END%% + ## Bibliography * Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. diff --git a/notes/programming/assertions.md b/notes/programming/assertions.md new file mode 100644 index 0000000..4aa21f8 --- /dev/null +++ b/notes/programming/assertions.md @@ -0,0 +1,16 @@ +--- +title: Assertions +TARGET DECK: Obsidian::STEM +FILE TAGS: programming::assertions +tags: + - assertions + - programming +--- + +## Overview + +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/programming/equiv-trans.md b/notes/programming/equiv-trans.md new file mode 100644 index 0000000..f71af50 --- /dev/null +++ b/notes/programming/equiv-trans.md @@ -0,0 +1,547 @@ +--- +title: Equivalence Transformation +TARGET DECK: Obsidian::STEM +FILE TAGS: programming::equiv-trans +tags: + - equiv-trans + - logic + - programming +--- + +## Overview + +**Equivalence-transformation** refers to a class of calculi for [[propositional|propositional logic]] derived from negation ($\neg$), conjunction ($\land$), disjunction ($\lor$), implication ($\Rightarrow$), and equality ($=$). Gries covers two in "The Science of Programming": a system of evaluation and a formal system. The system of evaluation mirrors how a computer processes instructions, at least in an abstract sense. The formal system serves as a theoretical framework for reasoning about propositions and their transformations without resorting to "lower-level" operations like substitution. + +%%ANKI +Basic +Who is the author of "The Science of Programming"? +Back: David Gries +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What are constant propositions? +Back: Propositions that contain only constants as operands. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Cloze +Gries replaces logical operator {$\Leftrightarrow$} in favor of {$=$}. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How does Lean define propositional equality? +Back: Expressions `a` and `b` are propositionally equal iff `a = b` is true. +Reference: Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. +Tags: lean + +END%% + +%%ANKI +Basic +How does Lean define `propext`? +Back: +```lean +axiom propext {a b : Prop} : (a ↔ b) → (a = b) +``` +Reference: Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. +Tags: lean + +END%% + +%%ANKI +Basic +What Lean theorem justifies Gries' choice of $=$ over $\Leftrightarrow$? +Back: `propext` +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +Tags: lean + +END%% + +%%ANKI +Basic +Is $(b \land c)$ well-defined in $\{(b, T), (c, F)\}$? +Back: Yes. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Is $(b \lor d)$ well-defined in $\{(b, T), (c, F)\}$? +Back: No. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What proposition represents states $\{(b, T)\}$ and $\{(c, F)\}$? +Back: $b \lor \neg c$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What set of states does $a \land b$ represent? +Back: The set containing just state $\{(a, T), (b, T)\}$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is sloppy about phrase "the states in $b \lor \neg c$"? +Back: $b \lor \neg c$ is not a set but a representation of a set (of states). +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the weakest proposition? +Back: $T$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What set of states does $T$ represent? +Back: The set of all states. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the strongest proposition? +Back: $F$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What set of states does $F$ represent? +Back: The set of no states. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What does a proposition *represent*? +Back: The set of states in which it is true. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +When is $p$ stronger than $q$? +Back: When $p \Rightarrow q$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +When is $p$ weaker than $q$? +Back: When $q \Rightarrow p$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +A proposition is well-defined with respect to what? +Back: A state to evaluate against. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Why is $b \land c$ stronger than $b \lor c$? +Back: The former represents a subset of the states the latter represents. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is a state? +Back: A function mapping identifiers to values. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What are the two calculi Gries describes equivalence-transformation with? +Back: A formal system and a system of evaluation. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +## Equivalence Schemas + +A proposition is said to be a **tautology** if it evaluates to $T$ in every state it is well-defined in. We say propositions $E1$ and $E2$ are **equivalent** if $E1 = E2$ is a tautology. In this case, we say $E1 = E2$ is an **equivalence**. + +%%ANKI +Basic +What does it mean for a proposition to be a tautology? +Back: That the proposition is true in every state it is well-defined in. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is tautology $e$ written equivalently with a quantifier? +Back: For free identifiers $i_1, \ldots, i_n$ in $e$, as $\forall (i_1, \ldots, i_n), e$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +The term "equivalent" refers to a comparison between what two objects? +Back: Expressions. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What does it mean for two propositions to be equivalent? +Back: Given propositions $E1$ and $E2$, it means $E1 = E2$ is a tautology. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is an equivalence? +Back: Given propositions $E1$ and $E2$, tautology $E1 = E2$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +* Commutative Laws + * $(E1 \land E2) = (E2 \land E1)$ + * $(E1 \lor E2) = (E2 \lor E1)$ + * $(E1 = E2) = (E2 = E1)$ + +%%ANKI +Basic +Which of the basic logical operators do the commutative laws apply to? +Back: $\land$, $\lor$, and $=$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What do the commutative laws allow us to do? +Back: Reorder operands. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the commutative law of e.g. $\land$? +Back: $E1 \land E2 = E2 \land E1$ + +END%% + +* Associative Laws + * $E1 \land (E2 \land E3) = (E1 \land E2) \land E3$ + * $E1 \lor (E2 \lor E3) = (E1 \lor E2) \lor E3$ + +%%ANKI +Basic +Which of the basic logical operators do the associative laws apply to? +Back: $\land$ and $\lor$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What do the associative laws allow us to do? +Back: Remove parentheses. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the associative law of e.g. $\land$? +Back: $E1 \land (E2 \land E3) = (E1 \land E2) \land E3$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +* Distributive Laws + * $E1 \lor (E2 \land E3) = (E1 \lor E2) \land (E1 \lor E3)$ + * $E1 \land (E2 \lor E3) = (E1 \land E2) \lor (E1 \land E3)$ + +%%ANKI +Basic +Which of the basic logical operators do the distributive laws apply to? +Back: $\land$ and $\lor$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What do the distributive laws allow us to do? +Back: "Factor" propositions. +Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the distributive law of e.g. $\land$ over $\lor$? +Back: $E1 \land (E2 \lor E3) = (E1 \land E2) \lor (E1 \land E3)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +* De Morgan's Laws + * $\neg (E1 \land E2) = \neg E1 \lor \neg E2$ + * $\neg (E1 \lor E2) = \neg E1 \land \neg E2$ + +%%ANKI +Basic +Which of the basic logical operators do De Morgan's Laws apply to? +Back: $\neg$, $\land$, and $\lor$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is De Morgan's Law of e.g. $\land$? +Back: $\neg (E1 \land E2) = \neg E1 \lor \neg E2$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +* Law of Negation + * $\neg (\neg E1) = E1$ + +%%ANKI +Basic +What does the Law of Negation say? +Back: $\neg (\neg E1) = E1$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +* Law of the Excluded Middle + * $E1 \lor \neg E1 = T$ + +%%ANKI +Basic +Which of the basic logical operators does the Law of the Excluded Middle apply to? +Back: $\lor$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What does the Law of the Excluded Middle say? +Back: $E1 \lor \neg E1 = T$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Which equivalence schema is "refuted" by sentence, "This sentence is false." +Back: Law of the Excluded Middle +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +* Law of Contradiction + * $E1 \land \neg E1 = F$ + +%%ANKI +Basic +Which of the basic logical operators does the Law of Contradiction apply to? +Back: $\land$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What does the Law of Contradiction say? +Back: $E1 \land \neg E1 = F$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Cloze +The Law of {1:the Excluded Middle} is to {2:$\lor$} whereas the Law of {2:Contradiction} is to {1:$\land$}. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +Gries lists other "Laws" but they don't seem as important to note here. + +%%ANKI +Basic +How is $\Rightarrow$ written in terms of other logical operators? +Back: $p \Rightarrow q$ is equivalent to $\neg p \lor q$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is $\Leftrightarrow$/$=$ written in terms of other logical operators? +Back: $p \Leftrightarrow q$ is equivalent to $(p \Rightarrow q) \land (q \Rightarrow p)$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What distinguishes an equality from an equivalence? +Back: An equivalence is an equality that is also a tautology. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +## Equivalence Rules + +* Rule of Substitution + * Let $P(r)$ be a predicate and $E1 = E2$ be an equivalence. Then $P(E1) = P(E2)$ is an equivalence. +* Rule of Transitivity + * Let $E1 = E2$ and $E2 = E3$ be equivalences. Then $E1 = E3$ is an equivalence. + +%%ANKI +Basic +What two inference rules make up the equivalence-transformation formal system? +Back: Substitution and transitivity. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Which of the two inference rules that make up the equivalence-transformation formal system is redundant? +Back: Transitivity. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What does the rule of substitution say in the system of evaluation? +Back: Let $P(r)$ be a predicate and $E1 = E2$ be an equivalence. Then $P(E1) = P(E2)$ is an equivalence. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is the rule of substitution written as an inference rule (in standard form)? +Back: +$$ +\begin{matrix} +E1 = E2 \\ +\hline P(E1) = P(E2) +\end{matrix} +$$ + +END%% + +%%ANKI +Basic +What does the rule of transitivity state in the system of evaluation? +Back: Let $E1 = E2$ and $E2 = E3$. Then $E1 = E3$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is the rule of transitivity written as an inference rule (in standard form)? +Back: +$$ +\begin{matrix} +E1 = E2, E2 = E3 \\ +\hline E1 = E3 +\end{matrix} +$$ + +END%% + +%%ANKI +Cloze +The system of evaluation has {equivalences} whereas the formal system has {theorems}. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is a "theorem" in the equivalence-transformation formal system? +Back: An equivalence derived from the axioms and inference rules. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is e.g. the Law of Implication proven in the system of evaluation? +Back: With truth tables +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is e.g. the Law of Implication proven in the formal system? +Back: It isn't. It is an axiom. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Cloze +The system of evaluation and formal system are connected by the following biconditional: {$e$ is a tautology} iff {$e = T$ is a theorem}. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Cloze +The {1:system of evaluation} is to {2:"$e$ is a tautology"} whereas the {2:formal system} is to {1:"$e = T$ is a theorem"}. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +## Bibliography + +* Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. +* 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/programming/index.md b/notes/programming/index.md new file mode 100644 index 0000000..15df7ec --- /dev/null +++ b/notes/programming/index.md @@ -0,0 +1,5 @@ +--- +title: Programming +tags: + - programming +--- diff --git a/notes/logic/equiv-trans.md b/notes/programming/text-sub.md similarity index 62% rename from notes/logic/equiv-trans.md rename to notes/programming/text-sub.md index af95a82..bdf507c 100644 --- a/notes/logic/equiv-trans.md +++ b/notes/programming/text-sub.md @@ -1,547 +1,13 @@ --- -title: Equivalence Transformation +title: Textual Substitution TARGET DECK: Obsidian::STEM -FILE TAGS: logic::equiv-trans +FILE TAGS: programming::text-sub tags: - - logic - - equiv-trans + - programming + - text-sub --- - ## Overview -**Equivalence-transformation** refers to a class of calculi for [[propositional|propositional logic]] derived from negation ($\neg$), conjunction ($\land$), disjunction ($\lor$), implication ($\Rightarrow$), and equality ($=$). Gries covers two in "The Science of Programming": a system of evaluation and a formal system. The system of evaluation mirrors how a computer processes instructions, at least in an abstract sense. The formal system serves as a theoretical framework for reasoning about propositions and their transformations without resorting to "lower-level" operations like substitution. - -%%ANKI -Basic -Who is the author of "The Science of Programming"? -Back: David Gries -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What are constant propositions? -Back: Propositions that contain only constants as operands. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Cloze -Gries replaces logical operator {$\Leftrightarrow$} in favor of {$=$}. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -How does Lean define propositional equality? -Back: Expressions `a` and `b` are propositionally equal iff `a = b` is true. -Reference: Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. -Tags: lean - -END%% - -%%ANKI -Basic -How does Lean define `propext`? -Back: -```lean -axiom propext {a b : Prop} : (a ↔ b) → (a = b) -``` -Reference: Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. -Tags: lean - -END%% - -%%ANKI -Basic -What Lean theorem justifies Gries' choice of $=$ over $\Leftrightarrow$? -Back: `propext` -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. -Tags: lean - -END%% - -%%ANKI -Basic -Is $(b \land c)$ well-defined in $\{(b, T), (c, F)\}$? -Back: Yes. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Is $(b \lor d)$ well-defined in $\{(b, T), (c, F)\}$? -Back: No. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What proposition represents states $\{(b, T)\}$ and $\{(c, F)\}$? -Back: $b \lor \neg c$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What set of states does $a \land b$ represent? -Back: The set containing just state $\{(a, T), (b, T)\}$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is sloppy about phrase "the states in $b \lor \neg c$"? -Back: $b \lor \neg c$ is not a set but a representation of a set (of states). -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the weakest proposition? -Back: $T$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What set of states does $T$ represent? -Back: The set of all states. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the strongest proposition? -Back: $F$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What set of states does $F$ represent? -Back: The set of no states. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What does a proposition *represent*? -Back: The set of states in which it is true. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -When is $p$ stronger than $q$? -Back: When $p \Rightarrow q$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -When is $p$ weaker than $q$? -Back: When $q \Rightarrow p$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -A proposition is well-defined with respect to what? -Back: A state to evaluate against. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Why is $b \land c$ stronger than $b \lor c$? -Back: The former represents a subset of the states the latter represents. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is a state? -Back: A function mapping identifiers to values. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What are the two calculi Gries describes equivalence-transformation with? -Back: A formal system and a system of evaluation. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -## Equivalence Schemas - -A proposition is said to be a **tautology** if it evaluates to $T$ in every state it is well-defined in. We say propositions $E1$ and $E2$ are **equivalent** if $E1 = E2$ is a tautology. In this case, we say $E1 = E2$ is an **equivalence**. - -%%ANKI -Basic -What does it mean for a proposition to be a tautology? -Back: That the proposition is true in every state it is well-defined in. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -How is tautology $e$ written equivalently with a quantifier? -Back: For free identifiers $i_1, \ldots, i_n$ in $e$, as $\forall (i_1, \ldots, i_n), e$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -The term "equivalent" refers to a comparison between what two objects? -Back: Expressions. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What does it mean for two propositions to be equivalent? -Back: Given propositions $E1$ and $E2$, it means $E1 = E2$ is a tautology. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is an equivalence? -Back: Given propositions $E1$ and $E2$, tautology $E1 = E2$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -* Commutative Laws - * $(E1 \land E2) = (E2 \land E1)$ - * $(E1 \lor E2) = (E2 \lor E1)$ - * $(E1 = E2) = (E2 = E1)$ - -%%ANKI -Basic -Which of the basic logical operators do the commutative laws apply to? -Back: $\land$, $\lor$, and $=$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What do the commutative laws allow us to do? -Back: Reorder operands. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the commutative law of e.g. $\land$? -Back: $E1 \land E2 = E2 \land E1$ - -END%% - -* Associative Laws - * $E1 \land (E2 \land E3) = (E1 \land E2) \land E3$ - * $E1 \lor (E2 \lor E3) = (E1 \lor E2) \lor E3$ - -%%ANKI -Basic -Which of the basic logical operators do the associative laws apply to? -Back: $\land$ and $\lor$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What do the associative laws allow us to do? -Back: Remove parentheses. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the associative law of e.g. $\land$? -Back: $E1 \land (E2 \land E3) = (E1 \land E2) \land E3$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -* Distributive Laws - * $E1 \lor (E2 \land E3) = (E1 \lor E2) \land (E1 \lor E3)$ - * $E1 \land (E2 \lor E3) = (E1 \land E2) \lor (E1 \land E3)$ - -%%ANKI -Basic -Which of the basic logical operators do the distributive laws apply to? -Back: $\land$ and $\lor$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What do the distributive laws allow us to do? -Back: "Factor" propositions. -Reference: Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the distributive law of e.g. $\land$ over $\lor$? -Back: $E1 \land (E2 \lor E3) = (E1 \land E2) \lor (E1 \land E3)$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -* De Morgan's Laws - * $\neg (E1 \land E2) = \neg E1 \lor \neg E2$ - * $\neg (E1 \lor E2) = \neg E1 \land \neg E2$ - -%%ANKI -Basic -Which of the basic logical operators do De Morgan's Laws apply to? -Back: $\neg$, $\land$, and $\lor$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is De Morgan's Law of e.g. $\land$? -Back: $\neg (E1 \land E2) = \neg E1 \lor \neg E2$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -* Law of Negation - * $\neg (\neg E1) = E1$ - -%%ANKI -Basic -What does the Law of Negation say? -Back: $\neg (\neg E1) = E1$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -* Law of the Excluded Middle - * $E1 \lor \neg E1 = T$ - -%%ANKI -Basic -Which of the basic logical operators does the Law of the Excluded Middle apply to? -Back: $\lor$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What does the Law of the Excluded Middle say? -Back: $E1 \lor \neg E1 = T$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Which equivalence schema is "refuted" by sentence, "This sentence is false." -Back: Law of the Excluded Middle -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -* Law of Contradiction - * $E1 \land \neg E1 = F$ - -%%ANKI -Basic -Which of the basic logical operators does the Law of Contradiction apply to? -Back: $\land$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What does the Law of Contradiction say? -Back: $E1 \land \neg E1 = F$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Cloze -The Law of {1:the Excluded Middle} is to {2:$\lor$} whereas the Law of {2:Contradiction} is to {1:$\land$}. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -Gries lists other "Laws" but they don't seem as important to note here. - -%%ANKI -Basic -How is $\Rightarrow$ written in terms of other logical operators? -Back: $p \Rightarrow q$ is equivalent to $\neg p \lor q$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -How is $\Leftrightarrow$/$=$ written in terms of other logical operators? -Back: $p \Leftrightarrow q$ is equivalent to $(p \Rightarrow q) \land (q \Rightarrow p)$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What distinguishes an equality from an equivalence? -Back: An equivalence is an equality that is also a tautology. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -## Equivalence Rules - -* Rule of Substitution - * Let $P(r)$ be a predicate and $E1 = E2$ be an equivalence. Then $P(E1) = P(E2)$ is an equivalence. -* Rule of Transitivity - * Let $E1 = E2$ and $E2 = E3$ be equivalences. Then $E1 = E3$ is an equivalence. - -%%ANKI -Basic -What two inference rules make up the equivalence-transformation formal system? -Back: Substitution and transitivity. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Which of the two inference rules that make up the equivalence-transformation formal system is redundant? -Back: Transitivity. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What does the rule of substitution say in the system of evaluation? -Back: Let $P(r)$ be a predicate and $E1 = E2$ be an equivalence. Then $P(E1) = P(E2)$ is an equivalence. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -How is the rule of substitution written as an inference rule (in standard form)? -Back: -$$ -\begin{matrix} -E1 = E2 \\ -\hline P(E1) = P(E2) -\end{matrix} -$$ - -END%% - -%%ANKI -Basic -What does the rule of transitivity state in the system of evaluation? -Back: Let $E1 = E2$ and $E2 = E3$. Then $E1 = E3$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -How is the rule of transitivity written as an inference rule (in standard form)? -Back: -$$ -\begin{matrix} -E1 = E2, E2 = E3 \\ -\hline E1 = E3 -\end{matrix} -$$ - -END%% - -%%ANKI -Cloze -The system of evaluation has {equivalences} whereas the formal system has {theorems}. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is a "theorem" in the equivalence-transformation formal system? -Back: An equivalence derived from the axioms and inference rules. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -How is e.g. the Law of Implication proven in the system of evaluation? -Back: With truth tables -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -How is e.g. the Law of Implication proven in the formal system? -Back: It isn't. It is an axiom. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Cloze -The system of evaluation and formal system are connected by the following biconditional: {$e$ is a tautology} iff {$e = T$ is a theorem}. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Cloze -The {1:system of evaluation} is to {2:"$e$ is a tautology"} whereas the {2:formal system} is to {1:"$e = T$ is a theorem"}. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -## Textual Substitution - **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. @@ -721,172 +187,6 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in END%% -### Theorems - -* $(E_u^x)_v^x = E_{u_v^x}^x$ - * The only possible free occurrences of $x$ that may appear after the first of the sequential substitutions occur in $u$. - -%%ANKI -Basic -How do we simplify $(E_u^x)_v^x$? -Back: As $E_{u_v^x}^x$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -How is $E_{u_v^x}^x$ rewritten as sequential substitution? -Back: As $(E_u^x)_v^x$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Why is $(E_u^x)_v^x = E_{u_v^x}^x$ an equivalence? -Back: After the first substitution, the only possible free occurrences of $x$ are in $u$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -* If $y$ is not free in $E$, then $(E_u^x)_v^y = E_{u_v^y}^x$. - * $y$ may not be free in $E$ but substituting $x$ with $u$ can introduce a free occurrence. It doesn't matter if we perform the substitution first or second though. - -%%ANKI -Basic -In what two scenarios is $(E_u^x)_v^y = E_{u_v^y}^x$ always an equivalence? -Back: $x = y$ or $y$ is not free 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 y$, when is $(E_u^x)_v^y = E_{u_v^y}^x$? -Back: When $y$ is not free in $E$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Why should $y$ not be free in $E$ for $(E_u^x)_v^y = E_{u_v^y}^x$ to be an equivalence? -Back: If it were, a $v$ would exist in the LHS that doesn't in the RHS. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -How does Gries denote state $s$ with identifer $x$ set to value $v$? -Back: $(s; x{:}v)$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -How is $(s; x{:}v)$ written instead using set-theoretical notation? -Back: $(s - \{\langle x, s(x) \rangle\}) \cup \{\langle x, v \rangle\}$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Execution of `x := e` in state $s$ terminates in what new state? -Back: $(s; x{:}s(e))$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Given state $s$, what statement does $(s; x{:}s(e))$ derive from? -Back: `x := e` -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What missing value guarantees state $s$ satisfies equivalence $s = (s; x{:}\_)$? -Back: $s(x)$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Given state $s$, why is it that $s = (s; x{:}s(x))$? -Back: Evaluating $x$ in state $s$ yields $s(x)$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -* $s(E_e^x) = s(E_{s(e)}^x)$ - * Substituting $x$ with $e$ and then evaluating is the same as substituting $x$ with the evaluation of $e$. - -%%ANKI -Basic -How can we simplify $s(E_{s(e)}^x)$? -Back: As $s(E_e^x)$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Given state $s$, what equivalence relates $E_e^x$ with $E_{s(e)}^x$? -Back: $s(E_e^x) = s(E_{s(e)}^x)$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -* Let $s$ be a state and $s' = (s; x{:}s(e))$. Then $s'(E) = s(E_e^x)$. - -%%ANKI -Cloze -Let $s$ be a state and $s' = (${$s; x{:}s(e)$}$)$. Then $s'(${$E$}$) = s(${$E_e^x$}$)$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -If $s' = (s; x{:}s(e))$, then $s'(E) = s(E_e^x)$. Why do we not say $s' = (s; x{:}e)$ instead? -Back: The value of a state's identifier must always be a constant proposition. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -How do you define $s'$ such that $s(E_e^x) = s'(E)$? -Back: $s' = (s; x{:}s(e))$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Given defined value $v \neq s(x)$, when is $s(E) = (s; x{:}v)(E)$? -Back: When $x$ is not free in $E$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -* Given identifiers $\bar{x}$ and fresh identifiers $\bar{u}$, $(E_{\bar{u}}^{\bar{x}})_{\bar{x}}^{\bar{u}} = E$. - -%%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. -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}$$ @@ -1074,7 +374,368 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in END%% +%%ANKI +Basic +Given array $b$, what terminology does Gries use to describe $i{:}j$ in e.g. $b[i{:}j]$? +Back: A section. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given array $b$, how many elements are in section $b[i{:}j]$? +Back: $j - i + 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$ and fixed $j$, what is the largest possible value of $i$ in $b[i{:}j]$? +Back: $j + 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$, how many elements are in $b[j{+}1{:}j]$? +Back: $0$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given array $b$, what is $b[1{:}5] = x$ an abbreviation for? +Back: $\forall i, 1 \leq i \leq 5 \Rightarrow b[i] = x$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given array $b$, what is $b[1{:}k{-}1] < x < b[k{:}n{-}1]$ an abbreviation for? +Back: $(\forall i, 1 \leq i < k \Rightarrow b[i] < x) \land (\forall i, k \leq i < n \Rightarrow x < b[i])$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +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*}$$ + +%%ANKI +Basic +What is a selector? +Back: A finite sequence of subscript expressions. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +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$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given valid expression $(b; [i]{\circ}s{:}e))$, what is the type of $b$? +Back: A function. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given valid expression $(b; \epsilon{\circ}s{:}e))$, what is the type of $b$? +Back: A scalar or function. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the base case of selector update syntax? +Back: Updates involving the null selector. +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? +Back: $\epsilon$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +The nuil selector is the identity element of what operation? +Back: Concatenation of sequences of subscripts. +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 := e$ rewritten with a selector? +Back: $x \circ \epsilon := e$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is $x \circ \epsilon := e$ rewritten using selector update syntax? +Back: $x := (x; \epsilon{:}e)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What assignment expression (i.e. using `:=`) is simpler but equivalent to $x := (x; \epsilon{:}e)$? +Back: $x := e$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What two assignments (i.e. using `:=`) are used to prove $e = (x; \epsilon{:}e)$? +Back: $x := e$ and $x \circ \epsilon := e$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How do assignments $x := e$ and $x \circ \epsilon := e$ prove $e = (x; \epsilon{:}e)$? +Back: The assignments have the same effect and the latter can be written as $x := (x; \epsilon{:}e)$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b$ be an array. How is $b[i][j] := e$ rewritten using selector update syntax? +Back: $(b; [i][j]{:}e)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b$ be an array. What does $(b; \epsilon{:}g)$ evaluate to? +Back: $g$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b$ be an array and $i = j$. What does $(b; [i]{\circ}s{:}e)[j]$ evaluate to? +Back: $(b[j]; s{:}e)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b$ be an array and $i \neq j$. What does $(b; [i]{\circ}s{:}e)[j]$ evaluate to? +Back: $b[j]$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Maintaining selector update syntax, how is $(c; 1{:}3)[1]$ rewritten with a selector? +Back: $(c; [1]{:}3)[1]$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Maintaining selector update syntax, how is $(c; 1{:}3)[1]$ rewritten with $[1]$ commuted as leftward as possible? +Back: $(c[1]; \epsilon{:}3)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +## Theorems + +* $(E_u^x)_v^x = E_{u_v^x}^x$ + * The only possible free occurrences of $x$ that may appear after the first of the sequential substitutions occur in $u$. + +%%ANKI +Basic +How do we simplify $(E_u^x)_v^x$? +Back: As $E_{u_v^x}^x$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is $E_{u_v^x}^x$ rewritten as sequential substitution? +Back: As $(E_u^x)_v^x$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Why is $(E_u^x)_v^x = E_{u_v^x}^x$ an equivalence? +Back: After the first substitution, the only possible free occurrences of $x$ are in $u$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +* If $y$ is not free in $E$, then $(E_u^x)_v^y = E_{u_v^y}^x$. + * $y$ may not be free in $E$ but substituting $x$ with $u$ can introduce a free occurrence. It doesn't matter if we perform the substitution first or second though. + +%%ANKI +Basic +In what two scenarios is $(E_u^x)_v^y = E_{u_v^y}^x$ always an equivalence? +Back: $x = y$ or $y$ is not free 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 y$, when is $(E_u^x)_v^y = E_{u_v^y}^x$? +Back: When $y$ is not free in $E$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Why should $y$ not be free in $E$ for $(E_u^x)_v^y = E_{u_v^y}^x$ to be an equivalence? +Back: If it were, a $v$ would exist in the LHS that doesn't in the RHS. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How does Gries denote state $s$ with identifer $x$ set to value $v$? +Back: $(s; x{:}v)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is $(s; x{:}v)$ written instead using set-theoretical notation? +Back: $(s - \{\langle x, s(x) \rangle\}) \cup \{\langle x, v \rangle\}$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Execution of `x := e` in state $s$ terminates in what new state? +Back: $(s; x{:}s(e))$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given state $s$, what statement does $(s; x{:}s(e))$ derive from? +Back: `x := e` +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What missing value guarantees state $s$ satisfies equivalence $s = (s; x{:}\_)$? +Back: $s(x)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given state $s$, why is it that $s = (s; x{:}s(x))$? +Back: Evaluating $x$ in state $s$ yields $s(x)$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +* $s(E_e^x) = s(E_{s(e)}^x)$ + * Substituting $x$ with $e$ and then evaluating is the same as substituting $x$ with the evaluation of $e$. + +%%ANKI +Basic +How can we simplify $s(E_{s(e)}^x)$? +Back: As $s(E_e^x)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given state $s$, what equivalence relates $E_e^x$ with $E_{s(e)}^x$? +Back: $s(E_e^x) = s(E_{s(e)}^x)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +* Let $s$ be a state and $s' = (s; x{:}s(e))$. Then $s'(E) = s(E_e^x)$. + +%%ANKI +Cloze +Let $s$ be a state and $s' = (${$s; x{:}s(e)$}$)$. Then $s'(${$E$}$) = s(${$E_e^x$}$)$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +If $s' = (s; x{:}s(e))$, then $s'(E) = s(E_e^x)$. Why do we not say $s' = (s; x{:}e)$ instead? +Back: The value of a state's identifier must always be a constant proposition. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How do you define $s'$ such that $s(E_e^x) = s'(E)$? +Back: $s' = (s; x{:}s(e))$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given defined value $v \neq s(x)$, when is $s(E) = (s; x{:}v)(E)$? +Back: When $x$ is not free in $E$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +* Given identifiers $\bar{x}$ and fresh identifiers $\bar{u}$, $(E_{\bar{u}}^{\bar{x}})_{\bar{x}}^{\bar{u}} = E$. + +%%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. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + ## Bibliography -* Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. * 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/trees.md b/notes/set/trees.md index e157c51..900100b 100644 --- a/notes/set/trees.md +++ b/notes/set/trees.md @@ -960,7 +960,7 @@ END%% %%ANKI Basic What does it mean for a $k$-ary tree to be complete? -Back: The last level is not filled but all leaves have the same depth and are leftmost arranged. +Back: All levels, except maybe the last, are filled. All leaves have the same depth and are leftmost arranged. Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). END%% @@ -989,6 +989,86 @@ Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition END%% +%%ANKI +Basic +How many internal nodes are in a complete $k$-ary tree of $n$ nodes? +Back: $\lceil (n - 1) / k \rceil$ +Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +What value of $k$ is used in the following description of a complete $k$-ary tree? +$$\begin{array}{c|c|c} +n & \text{external} & \text{internal} \\ +\hline +1 & 1 & 0 \\ +2 & 1 & 1 \\ +3 & 2 & 1 \\ +4 & 3 & 1 \\ +5 & 4 & 1 \\ +6 & 4 & 2 \\ +7 & 5 & 2 \\ +8 & 6 & 2 +\end{array}$$ +Back: $4$ +Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +What value of $k$ is used in the following description of a complete $k$-ary tree? +$$\begin{array}{c|c|c} +n & \text{external} & \text{internal} \\ +\hline +1 & 1 & 0 \\ +2 & 1 & 1 \\ +3 & 2 & 1 \\ +4 & 2 & 2 \\ +5 & 3 & 2 \\ +6 & 3 & 3 \\ +7 & 4 & 3 \\ +8 & 4 & 4 +\end{array}$$ +Back: $2$ +Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +When does the number of external nodes increment in a growing $k$-ary tree? +Back: When the next node added already has a sibling. +Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +When does the number of external nodes remain static in a growing $k$-ary tree? +Back: When the next node added has no sibling. +Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +When does the number of internal nodes increment in a growing $k$-ary tree? +Back: When the next node added has no sibling. +Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + +%%ANKI +Basic +When does the number of internal nodes remain static in a growing $k$-ary tree? +Back: When the next node added already has a sibling. +Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + #### Binary Trees A **binary tree** $T$ is a structure defined on a finite set of nodes that either @@ -1165,7 +1245,7 @@ Is the following a perfect binary tree? ![[perfect-tree.png]] Back: Yes. Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). - + END%% %%ANKI @@ -1174,7 +1254,7 @@ Is the following a complete binary tree? ![[perfect-tree.png]] Back: Yes. Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). - + END%% %%ANKI @@ -1183,7 +1263,7 @@ Is the following a full binary tree? ![[perfect-tree.png]] Back: Yes. Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). - + END%% %%ANKI @@ -1192,7 +1272,7 @@ Is the following a perfect binary tree? ![[complete-tree.png]] Back: No. Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). - + END%% %%ANKI @@ -1201,7 +1281,7 @@ Is the following a complete binary tree? ![[complete-tree.png]] Back: Yes. Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). - + END%% %%ANKI @@ -1210,7 +1290,7 @@ Is the following a full binary tree? ![[complete-tree.png]] Back: No. Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). - + END%% %%ANKI @@ -1219,7 +1299,7 @@ Is the following a perfect binary tree? ![[non-complete-tree.png]] Back: No. Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). - + END%% %%ANKI @@ -1228,7 +1308,7 @@ Is the following a complete binary tree? ![[non-complete-tree.png]] Back: No. Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). - + END%% %%ANKI @@ -1237,7 +1317,7 @@ Is the following a full binary tree? ![[non-complete-tree.png]] Back: No. Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). - + END%% %%ANKI @@ -1366,6 +1446,14 @@ Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition END%% +%%ANKI +Basic +How many internal nodes are in a complete binary tree of $n$ nodes? +Back: $\lceil (n - 1) / 2 \rceil = \lfloor n / 2 \rfloor$ +Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, Fourth edition (Cambridge, Massachusett: The MIT Press, 2022). + +END%% + ## Bibliography * “Binary Tree,” in _Wikipedia_, March 13, 2024, [https://en.wikipedia.org/w/index.php?title=Binary_tree&oldid=1213529508#Types_of_binary_trees](https://en.wikipedia.org/w/index.php?title=Binary_tree&oldid=1213529508#Types_of_binary_trees).