diff --git a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json index de477aa..d305375 100644 --- a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json +++ b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json @@ -64,20 +64,33 @@ "daily/2024-01-31.md": "72e343cef8d56e169cac7b360a88fcf0", "posix/index.md": "f7b1ae55f8f5e8f50f89738b1aca9111", "posix/signals.md": "2120ddd933fc0d57abb93c33f639afd8", - "gawk.md": "c79a09e1772da1d4f2cd296b7370ecab", + "gawk.md": "20ed75ec33b5e08933c81aac01eb64b5", "bash/index.md": "3b5296277f095acdf16655adcdf524af", "bash/shebang.md": "9006547710f9a079a3666169fbeda7aa", - "bash/robustness.md": "de97cd77aae047b5eea27440b43c9c42", + "bash/robustness.md": "a1d0d334939b54cca4bdfd2fd8ca27f0", "journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb", "journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970", "bash/quoting.md": "b1d8869a91001f8b22f0cdc54d806f61", - "nix/callPackage.md": "5ef6bc5d1a549c55d43ebb4d48c64427", + "nix/callPackage.md": "59796c480e2856fa7491f62ceb7e3c9c", "nix/index.md": "dd5ddd19e95d9bdbe020c68974d77a33", "journal/2024-02-02.md": "e2acbe75752d9c39875553223e34fb0d", "bash/prompts.md": "64bd3cd3c2feb9edb68ad8dc5ba65a35", "algorithms/sorting/index.md": "cd189e1a2cf32b5656b16aaf9f488874", "algorithms/sorting/insertion-sort.md": "c78c9983f87cdc4198f82803d418967f", "algorithms/index.md": "1583c07edea4736db27c38fe2b6c4c31" + "logic/propositional.md": "2e79b758dd161cc377f18cd1fa845285", + "logic/index.md": "d41d8cd98f00b204e9800998ecf8427e", + "journal/2024-02-03.md": "1359532c63e14251da04181fb0873d66", + "bash/prompts.md": "61cb877e68da040a15b85af76b1f68ba", + "algorithms/sorting/index.md": "3dea2ae728a19fa2d877711fa319ed87", + "algorithms/sorting/insertion-sort.md": "c78c9983f87cdc4198f82803d418967f", + "algorithms/index.md": "1583c07edea4736db27c38fe2b6c4c31", + "c/escape-sequences.md": "07f0811b0fff14f54f78abc33f2e6606", + "journal/2024-02-03.md": "0c5632b15b5f981bc3efe66c498f8add", + "lua/index.md": "d41d8cd98f00b204e9800998ecf8427e", + "c/index.md": "d41d8cd98f00b204e9800998ecf8427e", + "gawk/variables.md": "4482c297e7f4f5987f42f1926a880ca7", + "gawk/index.md": "0263448c8ae1ecfc0eacc4788f8402e9" }, "fields_dict": { "Basic": [ @@ -124,4 +137,4 @@ "Reference" ] } -} \ No newline at end of file +} diff --git a/notes/algorithms/sorting/index.md b/notes/algorithms/sorting/index.md index 51d8b6c..cf52005 100644 --- a/notes/algorithms/sorting/index.md +++ b/notes/algorithms/sorting/index.md @@ -9,7 +9,36 @@ tags: ## Overview -Let $n \geq 0$ and $S = \langle a_1, a_2, \ldots, a_n \rangle$ be a sequence. The **sorting problem** refers to permuting **keys** $a_1, a_2, \ldots, a_n$ into a new sequence $\langle a_1', a_2', \ldots, a_n' \rangle$ such that $a_1' \leq a_2' \leq \cdots \leq a_n'$. +Let $n \geq 0$. The **sorting problem** refers to permuting **records** $a_1, a_2, \ldots, a_n$ into a new sequence $\langle a_1', a_2', \ldots, a_n' \rangle$ such that $key(a_1') \leq key(a_2') \leq \cdots \leq key(a_n')$. + +%%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). + +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). + +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). + +END%% + +%%ANKI +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). + +END%% %%ANKI Basic @@ -26,6 +55,7 @@ Back: One in which only a constant number of input values are ever stored outsid Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009). END%% + ## Structural Comparison The #Elixir documentation makes a point that there exist two types of comparisons between data types.[^structural] The first is **structural** in which comparisons are made on the underlying data structures used to describe the data types. The second is **semantic** which focuses on making the comparison with respect to what the data types represent. diff --git a/notes/bash/prompts.md b/notes/bash/prompts.md index 0c763be..a50e7fa 100644 --- a/notes/bash/prompts.md +++ b/notes/bash/prompts.md @@ -8,7 +8,7 @@ tags: ## Overview -According to Robbins a POSIX-compliant shell (like Bash) generally has the primary and secondary prompts denoted with `$` and `>` respectively. +According to Robbins a POSIX-compliant shell (like Bash) generally has the primary and secondary prompts denoted with `$` and `>` respectively. Adjust these values using environment variables `$PS1` and `PS2` respectively. %%ANKI Basic @@ -18,6 +18,14 @@ Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 20 END%% +%%ANKI +Basic +What environment variable controls Bash's primary prompt? +Back: `$$PS1` +Reference: Cooper, Mendel. “Advanced Bash-Scripting Guide,” n.d., 916. + +END%% + %%ANKI Basic What symbol is usually used to denote the secondary prompt? @@ -26,6 +34,14 @@ Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 20 END%% +%%ANKI +Basic +What environment variable controls Bash's secondary prompt? +Back: `$$PS2` +Reference: Cooper, Mendel. “Advanced Bash-Scripting Guide,” n.d., 916. + +END%% + Paths supplied to commands are typically "sanitized" by prefixing the path name with `./`. This is mentioned in a few different places: * `find -execdir` performs this prefixing automatically on all found files. diff --git a/notes/bash/robustness.md b/notes/bash/robustness.md index ffbc400..d0d5688 100644 --- a/notes/bash/robustness.md +++ b/notes/bash/robustness.md @@ -9,7 +9,7 @@ tags: ## Overview -An interesting point Robbins discusses in his introduction to [[gawk]] is this idea of command robustness. He states that: +An interesting point Robbins discusses in his introduction to [[gawk/index|gawk]] is this idea of command robustness. He states that: > A self-contained shell script is more reliable because there are no other files to misplace. @@ -56,6 +56,12 @@ It's interesting to think what else can be used as a measure of a command's robu * What happens if I run the command twice in a row? * Whether a program acts atomically * Is it possible intermediate files are left that affect subsequent runs? +* The presence of timeouts + * Perhaps a program waits a specified amount of time before input is available. The command's success is now externally determined. +* Locale-aware functionality + * Consider for instance [[gawk/index|gawk]]'s `\u` [[escape-sequences|sequence]] which targets characters in the current locale's character set as opposed to specifically Unicode. + +The above scenarios are what makes something like [[nix/index|nix]] so compelling. ## References diff --git a/notes/c/escape-sequences.md b/notes/c/escape-sequences.md new file mode 100644 index 0000000..c4fced6 --- /dev/null +++ b/notes/c/escape-sequences.md @@ -0,0 +1,148 @@ +--- +title: Escape Sequences +TARGET DECK: Obsidian::STEM +FILE TAGS: c +tags: + - c +--- + +## Overview + +C has a standard for processing different escape sequences. Many languages built with C in mind parse these escape sequences in a similar way. + +* `\ooo`: Consists of one to three octal digits. + * [[bash/index|Bash]] supports this sequence as `$'\ooo'`. + * [[gawk/index|gawk]] supports this sequence directly. + * [[lua/index|Lua]] does not support this kind of escape sequence. Instead, it has a *decimal* escape sequence `\ddd`. + +%%ANKI +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). + +END%% + +%%ANKI +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). + +END%% + +%%ANKI +Basic +What alternative does Lua provide to C's `\ooo` sequence? +Back: `\ddd`, a *decimal* escape sequence. +Reference: Roberto Ierusalimschy, _Programming in Lua_, Fourth edition (Rio de Janeiro: Lua.org, 2016). +Tags: lua + +END%% + +%%ANKI +Basic +How are C escape sequences exposed in bash? +Back: Using ANSI-C quoting, i.e. `$$'string'`. +Reference: Mendel Cooper, “Advanced Bash-Scripting Guide,” n.d., 916. +Tags: bash + +END%% + +* `\xhh`: Consists of one or more hexadecimal digits. The `x` prefix is required to distinguish from octal escape sequences. + * [[bash/index|Bash]] supports this sequence as `$'\xhh'`. One or two digits is supported. + * [[gawk/index|gawk]] limits processing to two digits. + * Robbins states that using more than two hexadecimal digits can produce undefined results. + * [[Lua/index|Lua]] requires *exactly* two digits in its hex escape sequence. + +%%ANKI +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). + +END%% + +%%ANKI +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). + +END%% + +%%ANKI +Basic +What footgun does C's `\x` sequence expose? +Back: Using more than two hexadecimal digits can produce undefined results. +Reference: 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). + +END%% + +* `\uhhhh`: Introduced in C11 to represent Unicode code points. *Must* have exactly four hexadecimal characters specified with `0` leading padding if necessary. + * [[bash/index|Bash]] supports this sequence as `$'uhhhh'`. One to four hex digits is supported. + * [[gawk/index|gawk]] consolidates C's `\u` and `\U` sequence marker into just `\u`, capable of handling one to eight digits. Furthermore, `gawk` uses `\u` to designate the current locale's character set, *not* Unicode directly. Often times this is some Unicode-based locale though. + * [[lua/index|Lua]] consolidates C's `\u` and `\U` sequence markers into `\u{h...h}`, capable of handling one or more hexadecimal digits. The curly braces are required. + +%%ANKI +Basic +What two ways are C escape sequences for unicode denoted? +Back: As `\uhhhh` or `\Uhhhhhhhh`. +Reference: Jens Gustedt, _Modern C_ (Shelter Island, NY: Manning Publications Co, 2020). +Tags: unicode + +END%% + +%%ANKI +Basic +In C, `\u` allows specifying how many hexadecimal digits? +Back: Exactly four. +Reference: Jens Gustedt, _Modern C_ (Shelter Island, NY: Manning Publications Co, 2020). +Tags: unicode + +END%% + +%%ANKI +Basic +In what standard were C's `\u` and `\U` escape sequences introduced? +Back: C11. +Reference: Jens Gustedt, _Modern C_ (Shelter Island, NY: Manning Publications Co, 2020). +Tags: unicode + +END%% + +%%ANKI +Cloze +`\u` in C designates a character in {Unicode}. In `gawk` it designates a character in {the current locale's character set}. +Reference: 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). +Tags: unicode gawk + +END%% + +* `\Uhhhhhhhh`: Introduced in C11 to represent larger unicode code points. *Must* have exactly eight hexadecimal characters specified with `0` leading padding if necessary. + +%%ANKI +Basic +In C, `\U` allows specifying how many hexadecimal digits? +Back: Exactly eight. +Reference: Jens Gustedt, _Modern C_ (Shelter Island, NY: Manning Publications Co, 2020). +Tags: unicode + +END%% + +%%ANKI +Basic +Why does C have both `\u` and `\U`? +Back: `\U` accommodates for larger code point values. +Reference: Jens Gustedt, _Modern C_ (Shelter Island, NY: Manning Publications Co, 2020). +Tags: unicode + +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). +* 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/c/index.md b/notes/c/index.md new file mode 100644 index 0000000..e69de29 diff --git a/notes/gawk.md b/notes/gawk/index.md similarity index 83% rename from notes/gawk.md rename to notes/gawk/index.md index c3da461..757e25a 100644 --- a/notes/gawk.md +++ b/notes/gawk/index.md @@ -3,8 +3,6 @@ title: GAWK TARGET DECK: Obsidian::STEM FILE TAGS: linux::cli gawk tags: - - linux - - cli - gawk --- @@ -198,39 +196,12 @@ Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 202 END%% -## Variables +## Exit Status -Variables are defined like `var=val`. They can be specified in two different places: +On success, `gawk` exits with status code `EXIT_SUCCESS`. On failure, with status code `EXIT_FAILURE`. On fatal error, `gawk` exists with status code `2`. #c -1. Via the `-v` command line flag. Using this allows accessing the variable value from within a `BEGIN` rule. -2. In the file list. Using this allows accessing the variable value in all subsequent file processing. +You can specify a custom exit status by using the `exit` statement from within the `awk` program. -%%ANKI -Basic -Where in an `awk` invocation can variables be assigned? -Back: As a `-v` argument or in the file list. -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 -The `-v` flag was introduced to accommodate what functionality? -Back: Accessing variables from a `BEGIN` rule. -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 -Describe what the following command does in in a single sentence: -```bash -$ awk 'program' pass=1 data pass=2 data -``` -Back: Evaluates `'program'` against the `data` file twice with a different value of `pass` on each run. -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/gawk/variables.md b/notes/gawk/variables.md new file mode 100644 index 0000000..ce0a4e4 --- /dev/null +++ b/notes/gawk/variables.md @@ -0,0 +1,53 @@ +--- +title: GAWK +TARGET DECK: Obsidian::STEM +FILE TAGS: linux::cli gawk +tags: + - gawk +--- + +## Variables + +Variables are defined like `var=val`. They can be specified in two different places: + +1. Via the `-v` command line flag. Using this allows accessing the variable value from within a `BEGIN` rule. +2. In the file list. Using this allows accessing the variable value in all subsequent file processing. + +%%ANKI +Basic +Where in an `awk` invocation can variables be assigned? +Back: As a `-v` argument or in the file list. +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 +The `-v` flag was introduced to accommodate what functionality? +Back: Accessing variables from a `BEGIN` rule. +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 +Describe what the following command does in in a single sentence: +```bash +$ awk 'program' pass=1 data pass=2 data +``` +Back: Evaluates `'program'` against the `data` file twice with a different value of `pass` on each run. +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 `stdin` specified in `awk`'s file list? +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%% + +## 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/journal/2024-02-03.md b/notes/journal/2024-02-03.md new file mode 100644 index 0000000..1105160 --- /dev/null +++ b/notes/journal/2024-02-03.md @@ -0,0 +1,16 @@ +--- +title: "2024-02-03" +--- + +- [x] Anki Flashcards +- [x] KoL +- [x] Sheet Music (10 min.) +- [ ] OGS (1 Life & Death Problem) +- [x] Korean (Read 1 Story) +- [ ] Interview Prep (1 Practice Problem) +- [ ] Log Work Hours (Max 3 hours) + +* Spent time consolidating how different escape sequences behave across languages (`awk`, Bash, C, and Lua). +* Read 호랑이와 곶감 (The Tiger and the Dried Persimmon). +* Started practicing "One Summer's Day" by Joe Hisaishi, arranged by Torbjørn Brandrud. +* Re-reading "The Science of Programming" by David Gries. Finished reading chapters 1 and 2, but working on chapter 2 problems and notes. \ No newline at end of file diff --git a/notes/logic/index.md b/notes/logic/index.md new file mode 100644 index 0000000..e69de29 diff --git a/notes/logic/propositional.md b/notes/logic/propositional.md new file mode 100644 index 0000000..0dc725f --- /dev/null +++ b/notes/logic/propositional.md @@ -0,0 +1,307 @@ +--- +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/lua/index.md b/notes/lua/index.md new file mode 100644 index 0000000..e69de29 diff --git a/notes/nix/callPackage.md b/notes/nix/callPackage.md index 54682c9..9f7f742 100644 --- a/notes/nix/callPackage.md +++ b/notes/nix/callPackage.md @@ -90,7 +90,7 @@ callPackage = callPackageWith pkgs; %%ANKI Basic What two functions is `callPackage` implemented on top of? -Back: `callPackageWith` and `lib.makeOverridable`. +Back: `callPackageWith` and `makeOverridable`. Reference: Yin, Ryan. “NixOS and Flakes Book.” Nix, February 1, 2024. [https://github.com/ryan4yin/nixos-and-flakes-book](https://github.com/ryan4yin/nixos-and-flakes-book) END%% @@ -98,7 +98,7 @@ END%% %%ANKI Basic What is the purpose of `callPackage`? -Back: It calls package functions with arguments automatic supplied if not overridden. +Back: It calls package functions with arguments automatically supplied if not overridden. Reference: Yin, Ryan. “NixOS and Flakes Book.” Nix, February 1, 2024. [https://github.com/ryan4yin/nixos-and-flakes-book](https://github.com/ryan4yin/nixos-and-flakes-book) END%% @@ -113,4 +113,4 @@ END%% ## Reference -* Yin, Ryan. “NixOS and Flakes Book.” Nix, February 1, 2024. [https://github.com/ryan4yin/nixos-and-flakes-book](https://github.com/ryan4yin/nixos-and-flakes-book) \ No newline at end of file +* Yin, Ryan. “NixOS and Flakes Book.” Nix, February 1, 2024. [https://github.com/ryan4yin/nixos-and-flakes-book](https://github.com/ryan4yin/nixos-and-flakes-book)