diff --git a/notes/.obsidian/app.json b/notes/.obsidian/app.json index 6abe4c1..f1c28e2 100644 --- a/notes/.obsidian/app.json +++ b/notes/.obsidian/app.json @@ -1,3 +1,4 @@ { - "alwaysUpdateLinks": true + "alwaysUpdateLinks": true, + "spellcheck": false } \ No newline at end of file diff --git a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json index 2c9b638..227fdef 100644 --- a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json +++ b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json @@ -75,16 +75,16 @@ "Added Media": [], "File Hashes": { "algorithms/index.md": "1583c07edea4736db27c38fe2b6c4c31", - "algorithms/sorting/index.md": "3dea2ae728a19fa2d877711fa319ed87", - "algorithms/sorting/insertion-sort.md": "c78c9983f87cdc4198f82803d418967f", + "algorithms/sorting/index.md": "7b3b43d63ab2143e1314bb1b4e8392d2", + "algorithms/sorting/insertion-sort.md": "6ad645860c9c281eb8eb06c93135746f", "bash/index.md": "3b5296277f095acdf16655adcdf524af", "bash/prompts.md": "61cb877e68da040a15b85af76b1f68ba", "bash/quoting.md": "b1d8869a91001f8b22f0cdc54d806f61", "bash/robustness.md": "7ab094b95ba2bfa885adba8e9efedf68", "bash/shebang.md": "9006547710f9a079a3666169fbeda7aa", - "c/escape-sequences.md": "07f0811b0fff14f54f78abc33f2e6606", + "c/escape-sequences.md": "0d6219ebb51f6f21e026de67603e25b8", "c/index.md": "aa8a34c62e7bc284ff589e28609222dc", - "gawk/index.md": "0263448c8ae1ecfc0eacc4788f8402e9", + "gawk/index.md": "d23f281fcfef7169a1ab68b974359c5b", "gawk/variables.md": "4482c297e7f4f5987f42f1926a880ca7", "index.md": "e48e895feeed7046425bb2ee15419770", "journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970", @@ -92,16 +92,26 @@ "journal/2024-02-02.md": "a3b222daee8a50bce4cbac699efc7180", "journal/2024-02-03.md": "c6d411f0e2e964270399dd3a99f48382", "logic/index.md": "3084b41fe1451259a0cf3e54560c2e85", - "logic/propositional.md": "45aee8bf688aa8fef4b136145085d38a", + "logic/propositional.md": "e7dbb24674336beb44dc9ef4c9ae51ff", "lua/index.md": "26632dae1f852519e2f1af11d65c34eb", "nix/callPackage.md": "59796c480e2856fa7491f62ceb7e3c9c", "nix/index.md": "dd5ddd19e95d9bdbe020c68974d77a33", "posix/index.md": "f7b1ae55f8f5e8f50f89738b1aca9111", "posix/signals.md": "2120ddd933fc0d57abb93c33f639afd8", "templates/daily.md": "7866014e730e85683155207a02e367d8", - "posix/regexp.md": "d7effae06677d559b15180ce30f1d306", + "posix/regexp.md": "2529451da41c81b891ea8ce82cca549e", "journal/2024-02-04.md": "e2b5678fc53d7284b71ed6820c02b954", - "gawk/regexp.md": "2dbc2548ed9212ddac8e8f66d979b5b7" + "gawk/regexp.md": "dbd5f9f85a2658b304a635a47379e871", + "_templates/daily.md": "7866014e730e85683155207a02e367d8", + "_journal/2024-02-05.md": "f8505abd415c50fd97c81fd6153a6d4f", + "_journal/2024-02-06.md": "1ea415f3c3f5be17f796b9a0d4df565f", + "_journal/2024-02-04.md": "f77a3c5f3ce7969120f226738836dc92", + "_journal/2024-02-03.md": "c6d411f0e2e964270399dd3a99f48382", + "_journal/2024-02-02.md": "a3b222daee8a50bce4cbac699efc7180", + "_journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb", + "_journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970", + "logic/equiv-trans.md": "82a3376977bc5579fba5f9201c9f2c14", + "_journal/2024-02-07.md": "9197386e8caaf9502f12fdc10d68fa9f" }, "fields_dict": { "Basic": [ diff --git a/notes/_journal/2024-02-04.md b/notes/_journal/2024-02-04.md index 2dc9240..4fe9747 100644 --- a/notes/_journal/2024-02-04.md +++ b/notes/_journal/2024-02-04.md @@ -2,10 +2,12 @@ title: "2024-02-04" --- -- [ ] Anki Flashcards +- [x] Anki Flashcards - [x] KoL - [ ] Sheet Music (10 min.) - [ ] OGS (1 Life & Death Problem) - [ ] Korean (Read 1 Story) - [ ] Interview Prep (1 Practice Problem) -- [ ] Log Work Hours (Max 3 hours) \ No newline at end of file +- [ ] Log Work Hours (Max 3 hours) + +* Today was spent primarily traveling. \ No newline at end of file diff --git a/notes/_journal/2024-02-05.md b/notes/_journal/2024-02-05.md new file mode 100644 index 0000000..00f4f18 --- /dev/null +++ b/notes/_journal/2024-02-05.md @@ -0,0 +1,14 @@ +--- +title: "2024-02-04" +--- + +- [x] Anki Flashcards +- [ ] KoL +- [ ] Sheet Music (10 min.) +- [ ] OGS (1 Life & Death Problem) +- [ ] Korean (Read 1 Story) +- [ ] Interview Prep (1 Practice Problem) +- [ ] Log Work Hours (Max 3 hours) + +* Today was spent mostly hanging out with Brittany and Katie. +* I spent a brief amount of time thinking about the equivalence-transformation system described by Gries. \ No newline at end of file diff --git a/notes/_journal/2024-02-06.md b/notes/_journal/2024-02-06.md index 8e23145..e04baf3 100644 --- a/notes/_journal/2024-02-06.md +++ b/notes/_journal/2024-02-06.md @@ -8,6 +8,7 @@ title: "2024-02-06" - [ ] OGS (1 Life & Death Problem) - [ ] Korean (Read 1 Story) - [ ] Interview Prep (1 Practice Problem) -- [ ] Log Work Hours (Max 3 hours) +- [x] Log Work Hours (Max 3 hours) -* \ No newline at end of file +* Continued reading about `awk` regular expressions. Finished Chapter 3 of "GAWK: Effective AWK Programming". +* Translated more notes on equivalence-transformation. \ No newline at end of file diff --git a/notes/_journal/2024-02-07.md b/notes/_journal/2024-02-07.md new file mode 100644 index 0000000..a54d5b4 --- /dev/null +++ b/notes/_journal/2024-02-07.md @@ -0,0 +1,13 @@ +--- +title: "2024-02-07" +--- + +- [x] Anki Flashcards +- [x] KoL +- [ ] Sheet Music (10 min.) +- [ ] OGS (1 Life & Death Problem) +- [ ] Korean (Read 1 Story) +- [ ] Interview Prep (1 Practice Problem) +- [ ] Log Work Hours (Max 3 hours) + +* Read section 4.1 of "GAWK: Effective AWK Programming". \ No newline at end of file diff --git a/notes/algorithms/sorting/index.md b/notes/algorithms/sorting/index.md index cf52005..5658d4f 100644 --- a/notes/algorithms/sorting/index.md +++ b/notes/algorithms/sorting/index.md @@ -14,21 +14,21 @@ Let $n \geq 0$. The **sorting problem** refers to permuting **records** $a_1, a_ %%ANKI Cloze In the sorting problem, a "{record}" refers to {the entries being sorted}. -Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009). +Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). END%% %%ANKI Cloze In the sorting problem, a "{key}" refers to {the value records are sorted by}. -Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009). +Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). END%% %%ANKI Cloze In the sorting problem, "{satellite data}" refers to {the non-key values of records}. -Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009). +Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). END%% @@ -36,7 +36,7 @@ END%% Basic What term does Cormen et al. use to describe the record value used for sorting? Back: Keys. -Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009). +Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). END%% @@ -44,7 +44,7 @@ END%% Basic What makes a sorting algorithm stable? Back: "Equal" values are ordered the same in the output as they are in the input. -Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009). +Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). END%% @@ -52,7 +52,7 @@ END%% Basic What is an in place sorting algorithm? Back: One in which only a constant number of input values are ever stored outside the array. -Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009). +Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). END%% @@ -93,7 +93,7 @@ END%% ## References -* Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009). +* Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). * “Kernel — Elixir v1.16.1,” accessed February 2, 2024, [https://hexdocs.pm/elixir/1.16/Kernel.html#module-structural-comparison](https://hexdocs.pm/elixir/1.16/Kernel.html#module-structural-comparison). [^structural]: [Structural Comparison](https://hexdocs.pm/elixir/1.16/Kernel.html#module-structural-comparison) \ No newline at end of file diff --git a/notes/algorithms/sorting/insertion-sort.md b/notes/algorithms/sorting/insertion-sort.md index 63762a2..a28d82e 100644 --- a/notes/algorithms/sorting/insertion-sort.md +++ b/notes/algorithms/sorting/insertion-sort.md @@ -24,7 +24,7 @@ Insertion sort works by advancing an index `i` through an array `A[1..n]` such t Basic What is insertion sort's best case runtime? Back: $O(n)$ -Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009). +Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). END%% @@ -32,7 +32,7 @@ END%% Basic What input value does insertion sort perform best on? Back: An already sorted array. -Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009). +Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). END%% @@ -40,7 +40,7 @@ END%% Basic What is insertion sort's worst case runtime? Back: $O(n^2)$ -Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009). +Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). END%% @@ -48,7 +48,7 @@ END%% Basic What input value does insertion sort perform worst on? Back: An array in reverse-sorted order. -Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009). +Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). END%% @@ -56,7 +56,7 @@ END%% Basic Is insertion sort in place? Back: Yes -Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009). +Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). END%% @@ -64,7 +64,7 @@ END%% Basic Is insertion sort stable? Back: Yes -Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009). +Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). END%% @@ -85,7 +85,7 @@ void insertion_sort(const int n, int A[static n]) { Basic What loop invariant is maintained in insertion sort? Back: `A[1..i]` is in sorted order. -Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009). +Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). END%% @@ -99,7 +99,7 @@ If you repeat this process for every card in the deck, your left hand will event Basic What analogy does Cormen et al. use to explain insertion sort? Back: Sorting a shuffled deck of playing cards. -Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009). +Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). END%% @@ -107,10 +107,10 @@ END%% Basic What invariant does the left hand maintain in Cormen et al.'s insertion sort analogy? Back: It contains all drawn cards in sorted order. -Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009). +Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). END%% ## References -* Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009). +* Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). diff --git a/notes/c/escape-sequences.md b/notes/c/escape-sequences.md index c4fced6..392b17d 100644 --- a/notes/c/escape-sequences.md +++ b/notes/c/escape-sequences.md @@ -19,7 +19,7 @@ C has a standard for processing different escape sequences. Many languages built Basic How are C escape sequences for octal digits denoted? Back: As `\ooo`. -Reference: Brian W. Kernighan and Dennis M. Ritchie, _The C Programming Language_, 2nd ed (Englewood Cliffs, N.J: Prentice Hall, 1988). +Reference: Brian W. Kernighan and Dennis M. Ritchie, *The C Programming Language*, 2nd ed (Englewood Cliffs, N.J: Prentice Hall, 1988). END%% @@ -27,7 +27,7 @@ END%% Basic In C, `\ooo` allows specifying how many octal digits? Back: One to three. -Reference: Brian W. Kernighan and Dennis M. Ritchie, _The C Programming Language_, 2nd ed (Englewood Cliffs, N.J: Prentice Hall, 1988). +Reference: Brian W. Kernighan and Dennis M. Ritchie, *The C Programming Language*, 2nd ed (Englewood Cliffs, N.J: Prentice Hall, 1988). END%% @@ -59,7 +59,7 @@ END%% Basic How are C escape sequences for hexadecimal digits denoted? Back: As `\xhh`. -Reference: Brian W. Kernighan and Dennis M. Ritchie, _The C Programming Language_, 2nd ed (Englewood Cliffs, N.J: Prentice Hall, 1988). +Reference: Brian W. Kernighan and Dennis M. Ritchie, *The C Programming Language*, 2nd ed (Englewood Cliffs, N.J: Prentice Hall, 1988). END%% @@ -67,7 +67,7 @@ END%% Basic In C, `\x` allows specifying how many hexadecimal digits? Back: One or more. -Reference: Brian W. Kernighan and Dennis M. Ritchie, _The C Programming Language_, 2nd ed (Englewood Cliffs, N.J: Prentice Hall, 1988). +Reference: Brian W. Kernighan and Dennis M. Ritchie, *The C Programming Language*, 2nd ed (Englewood Cliffs, N.J: Prentice Hall, 1988). END%% @@ -142,7 +142,7 @@ END%% ## References * Arnold D. Robbins, “GAWK: Effective AWK Programming,” October 2023, [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf). -* Brian W. Kernighan and Dennis M. Ritchie, _The C Programming Language_, 2nd ed (Englewood Cliffs, N.J: Prentice Hall, 1988). +* Brian W. Kernighan and Dennis M. Ritchie, *The C Programming Language*, 2nd ed (Englewood Cliffs, N.J: Prentice Hall, 1988). * Jens Gustedt, _Modern C_ (Shelter Island, NY: Manning Publications Co, 2020). * Mendel Cooper, “Advanced Bash-Scripting Guide,” n.d., 916. * Roberto Ierusalimschy, _Programming in Lua_, Fourth edition (Rio de Janeiro: Lua.org, 2016). \ No newline at end of file diff --git a/notes/gawk/index.md b/notes/gawk/index.md index 757e25a..0a60b0a 100644 --- a/notes/gawk/index.md +++ b/notes/gawk/index.md @@ -119,12 +119,89 @@ Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 202 END%% -**Targets** are specified as `$n` where `n` is a placeholder for the `n`th whitespace-separated **field**s of the input line. For example, `$1` refers to the first field of the input line. `$0` is a special target referring to the entire list of arguments, i.e. the entire line. +`awk` reads in files in units called **records**. Each record is automatically broken up into chunks called **fields**. By default, a record corresponds to a single line. `$0` would then refer to the entire line and `$1` would refer to the first field of this line. + +%%ANKI +Basic +In `awk`, what does a "record" refer to? +Back: The unit that input is read in. +Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) + +END%% + +%%ANKI +Basic +What is the default record separator? +Back: The newline character. +Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) + +END%% + +%%ANKI +Cloze +The {`RS`} variable is used to change the {record separator}. +Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) + +END%% + +%%ANKI +Cloze +If `RS` is a string with {more than one character}, it is treated as a {regexp}. +Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) + +END%% + +%%ANKI +Cloze +The {`RT`} variable matches the {input characters that matched `RS`}. +Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) + +END%% + +%%ANKI +Basic +Barring the final record, when is `RT` always equal to `RS`? +Back: When `RS` is a string containing a single character. +Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) + +END%% + +%%ANKI +Basic +What value of `RS` may `gawk` not process correctly? +Back: A regexp with optional trailing part, e.g. `AB(XYZ)?`. +Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) + +END%% + +%%ANKI +Basic +What implementation detail inspires avoiding `RS = "\0"`? +Back: Most `awk` implementations store strings internally as C-style strings? +Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) + +END%% + +%%ANKI +Basic +What equivalent assignment do most `awk` implementations interpret `RS = "\0"` as? +Back: `RS = ""` +Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) + +END%% + +%%ANKI +Basic +In `awk`, what does a "field" refer to? +Back: A specific part of a record. +Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) + +END%% %%ANKI Basic What is `$0` a placeholder for? -Back: The entire input line. +Back: An entire record. Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) END%% @@ -132,7 +209,7 @@ END%% %%ANKI Basic What is `$1` a placeholder for? -Back: The first field of the input line. +Back: The first field of a record. Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) END%% @@ -159,7 +236,7 @@ Describe what the following command does in in a single sentence: ```bash $ awk 'NF > 0' data ``` -Back: Prints every line of `data` with at least one field. +Back: Prints every record in `data` with at least one field. Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) END%% @@ -170,7 +247,7 @@ Describe what the following command does in in a single sentence: ```bash $ awk 'END { print NR }' data ``` -Back: Prints the number of lines in `data`. +Back: Prints the number of records in `data`. Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) END%% @@ -181,7 +258,7 @@ Describe what the following command does in in a single sentence: ```bash $ awk 'NR % 2 == 0' data ``` -Back: Prints every even-numbered line in `data`. +Back: Prints every even-numbered record in `data`. Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) END%% diff --git a/notes/gawk/regexp.md b/notes/gawk/regexp.md index 8218a95..02034a9 100644 --- a/notes/gawk/regexp.md +++ b/notes/gawk/regexp.md @@ -20,6 +20,64 @@ $ awk '$1 ~ /li/' data `awk`'s implementation of regexps are a superset of [[posix/regexp|POSIX EREs]]. +%%ANKI +Basic +What is the result of the following? +```bash +$ echo aaaabcd | awk '{ sub(/a+/, ""); print }' +``` +Back: `bcd` +Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) + +END%% + +%%ANKI +Cloze +In `awk`, `/.../` is to a {regexp} constant whereas `"..."` is to a {string} constant. +Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) + +END%% + +%%ANKI +Basic +How are string constants processed differently from regexp constants? +Back: The string constant is scanned twice. +Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) + +END%% + +%%ANKI +Basic +What term describes a regexp that isn't a regexp constant? +Back: A dynamic regexp. +Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) + +END%% + +%%ANKI +Basic +How is `*` escaped in a regexp constant? +Back: `/\*/` +Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) + +END%% + +%%ANKI +Basic +How is `*` escaped in a string constant (dynamic regexp)? +Back: `"\\*"` +Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) + +END%% + +%%ANKI +Basic +Why is it recommended to avoid using `^`/`$` in `RS`? +Back: These anchors match the beginning/end of a string, not of a line. +Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) + +END%% + ## References * Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) \ No newline at end of file diff --git a/notes/logic/equiv-trans.md b/notes/logic/equiv-trans.md new file mode 100644 index 0000000..bb18bfb --- /dev/null +++ b/notes/logic/equiv-trans.md @@ -0,0 +1,650 @@ +--- +title: Equivalence Transformation +TARGET DECK: Obsidian::STEM +FILE TAGS: logic::equiv-trans +tags: + - logic + - equiv-trans +--- + +## Overview + +**Equivalence-transformation** refers to a class of calculi for manipulating propositions 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 the constant propositions? +Back: $T$ and $F$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What are the basic propositional logical operators? +Back: $\neg$, $\land$, $\lor$, $\Rightarrow$, and $\Leftrightarrow$/$=$ +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 +What name is given to $\land$ operands? +Back: Conjuncts +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What name is given to $\lor$ operands? +Back: Disjuncts +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What name is given to operand $a$ in $a \Rightarrow b$? +Back: The antecedent +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What name is given to operand $b$ in $a \Rightarrow b$? +Back: The consequent +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +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 C operator corresponds to $\neg$? +Back: `!` +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +Tags: c + +END%% + +%%ANKI +Basic +What C operator corresponds to $\land$? +Back: There isn't one. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +Tags: c + +END%% + +%%ANKI +Basic +What C operator corresponds to $\lor$? +Back: There isn't one. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +Tags: c + +END%% + +%%ANKI +Basic +What C operator corresponds to $\Rightarrow$? +Back: There isn't one. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +Tags: c + +END%% + +%%ANKI +Basic +What C operator corresponds to $\Leftrightarrow$? +Back: `==` +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. +Tags: c + +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 +The term "equivalent" refers to a comparison between what two objects? +Back: Propositions. +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: $\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%% + +## 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 +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%% + +## Normal Forms + +Every proposition can be written in **disjunctive normal form** (DNF) and **conjunctive normal form** (CNF). This is evident with the use of truth tables. To write a proposition in DNF, write its corresponding truth table and $\lor$ each row that evaluates to $T$. To write the same proposition in CNF, apply $\lor$ to each row that evaluates to $F$ and negate it. + +$$\neg (a \Rightarrow b) \Leftrightarrow c$$ + +It's truth table looks like + +$$\begin{array}{c|c|c|c|c|c} +\neg & (a & \Rightarrow & b) & \Leftrightarrow & c \\ +\hline +F & T & T & T & F & T \\ +F & T & T & T & T & F \\ +T & T & F & F & T & T \\ +T & T & F & F & F & F \\ +F & F & T & T & F & T \\ +F & F & T & T & T & F \\ +F & F & T & F & F & T \\ +F & F & T & F & T & F +\end{array}$$ + +and it's DNF looks like + +$$ +(a \land b \land \neg c) \lor +(a \land \neg b \land c) \lor +(\neg a \land b \land \neg c) \lor +(\neg a \land \neg b \land \neg c) +$$ + +It's CNF results from applying De Morgan's Law to the truth table's "complement": + +$$ +\neg( + (a \land b \land c) \lor + (a \land \neg b \land \neg c) \lor + (\neg a \land b \land c) \lor + (\neg a \land \neg b \land c) +) +$$ + +%%ANKI +Basic +What construct is used to prove every proposition can be written in DNF or CNF? +Back: Truth tables +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Where are $\land$ and $\lor$ found within a proposition in DNF? +Back: $\lor$ separates disjuncts containing $\land$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is DNF an acronym for? +Back: **D**isjunctive **N**ormal **F**orm. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is CNF an acronym for? +Back: **C**onjunctive **N**ormal **F**orm. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Where are $\land$ and $\lor$ found within a proposition in CNF? +Back: $\land$ separates conjuncts containing $\lor$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +## References + +* 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/logic/propositional.md b/notes/logic/propositional.md deleted file mode 100644 index 0dc725f..0000000 --- a/notes/logic/propositional.md +++ /dev/null @@ -1,307 +0,0 @@ ---- -title: Propositional Logic -TARGET DECK: Obsidian::STEM -FILE TAGS: logic::0-order -tags: - - logic - - 0-order ---- - -## Overview - -Propositional logic (or `0`-order logic) refers to the manipulation of **propositions** using the following five logical operators: $\neg$, $\land$, $\lor$, $\Rightarrow$, $\Leftrightarrow$. - -%%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 the constant propositions? -Back: $T$ and $F$ -Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What are the five propositional logical operators? -Back: $\neg$, $\land$, $\lor$, $\Rightarrow$, and $\Leftrightarrow$ -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 -What name is given to $\land$ operands? -Back: Conjuncts -Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What name is given to $\lor$ operands? -Back: Disjuncts -Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What name is given to operand $a$ in $a \Rightarrow b$? -Back: The antecedent -Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What name is given to operand $b$ in $a \Rightarrow b$? -Back: The consequent -Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What does the evaluation model of propositional logic refer to? -Back: An interpretation of propositional logic that associates values to identifiers. -Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Evaluation model. 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 is necessary to determine if a proposition is well-defined? -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 -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 -Evaluation model. What does it mean for a proposition to be a tautology? -Back: A 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 -What C operator corresponds to $\neg$? -Back: `!` -Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. -Tags: c - -END%% - -%%ANKI -Basic -What C operator corresponds to $\land$? -Back: There isn't one. -Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. -Tags: c - -END%% - -%%ANKI -Basic -What C operator corresponds to $\lor$? -Back: There isn't one. -Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. -Tags: c - -END%% - -%%ANKI -Basic -What C operator corresponds to $\Rightarrow$? -Back: There isn't one. -Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. -Tags: c - -END%% - -%%ANKI -Basic -What C operator corresponds to $\Leftrightarrow$? -Back: `=` -Reference: Gries, David. _The Science of Programming_. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. -Tags: c - -END%% - -%%ANKI -Basic -Evaluation model. 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 -Evaluation model. 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 -Evaluation model. 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 -Evaluation model. What is sloppy about phrase "the states in $b \lor \neg c$"? -Back: $b \lor \neg c$ is not a set. -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 -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 -Evaluation model. 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 -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%% - -## References - -* 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/posix/regexp.md b/notes/posix/regexp.md index 98dc519..1dccdc1 100644 --- a/notes/posix/regexp.md +++ b/notes/posix/regexp.md @@ -8,7 +8,38 @@ tags: ## Overview -The following ERE (**E**xtended **R**egular **E**xpression) operators were defined to achieve consistency between programs like `grep`, `sed`, and `awk`. +The following ERE (**E**xtended **R**egular **E**xpression) operators were defined to achieve consistency between programs like `grep`, `sed`, and `awk`. In POSIX, regexps are greedy. + +%%ANKI +Cloze +Regular expressions are either {greedy} or {lazy}. +Reference: “POSIX Basic Regular Expressions,” accessed February 4, 2024, [https://en.wikibooks.org/wiki/Regular_Expressions/POSIX_Basic_Regular_Expressions](https://en.wikibooks.org/wiki/Regular_Expressions/POSIX_Basic_Regular_Expressions). + +END%% + +%%ANKI +Basic +Are POSIX regexps greedy or lazy? +Back: Greedy. +Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) + +END%% + +%%ANKI +Basic +What does it mean for a regexp to be greedy? +Back: The regexp matches as many characters as it can. +Reference: “POSIX Basic Regular Expressions,” accessed February 4, 2024, [https://en.wikibooks.org/wiki/Regular_Expressions/POSIX_Basic_Regular_Expressions](https://en.wikibooks.org/wiki/Regular_Expressions/POSIX_Basic_Regular_Expressions). + +END%% + +%%ANKI +Basic +What does it mean for a regexp to be lazy? +Back: The regexp matches as few characters as it can. +Reference: “POSIX Basic Regular Expressions,” accessed February 4, 2024, [https://en.wikibooks.org/wiki/Regular_Expressions/POSIX_Basic_Regular_Expressions](https://en.wikibooks.org/wiki/Regular_Expressions/POSIX_Basic_Regular_Expressions). + +END%% %%ANKI Basic @@ -94,7 +125,7 @@ END%% %%ANKI Cloze -The {`$`} operator matches {the ending position of a string}. +The {`$$`} operator matches {the ending position of a string}. Reference: “POSIX Basic Regular Expressions,” accessed February 4, 2024, [https://en.wikibooks.org/wiki/Regular_Expressions/POSIX_Basic_Regular_Expressions](https://en.wikibooks.org/wiki/Regular_Expressions/POSIX_Basic_Regular_Expressions). END%%