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

Merge 2023-02-03 #3

Merged
jrpotter merged 7 commits from daily into main 2024-02-04 00:20:32 +00:00
Conversation 0 Commits 7 Files Changed 13
13 changed files with 602 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -64,20 +64,33 @@
"daily/2024-01-31.md": "72e343cef8d56e169cac7b360a88fcf0", "daily/2024-01-31.md": "72e343cef8d56e169cac7b360a88fcf0",
"posix/index.md": "f7b1ae55f8f5e8f50f89738b1aca9111", "posix/index.md": "f7b1ae55f8f5e8f50f89738b1aca9111",
"posix/signals.md": "2120ddd933fc0d57abb93c33f639afd8", "posix/signals.md": "2120ddd933fc0d57abb93c33f639afd8",
"gawk.md": "c79a09e1772da1d4f2cd296b7370ecab", "gawk.md": "20ed75ec33b5e08933c81aac01eb64b5",
"bash/index.md": "3b5296277f095acdf16655adcdf524af", "bash/index.md": "3b5296277f095acdf16655adcdf524af",
"bash/shebang.md": "9006547710f9a079a3666169fbeda7aa", "bash/shebang.md": "9006547710f9a079a3666169fbeda7aa",
"bash/robustness.md": "de97cd77aae047b5eea27440b43c9c42", "bash/robustness.md": "a1d0d334939b54cca4bdfd2fd8ca27f0",
"journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb", "journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb",
"journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970", "journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970",
"bash/quoting.md": "b1d8869a91001f8b22f0cdc54d806f61", "bash/quoting.md": "b1d8869a91001f8b22f0cdc54d806f61",
"nix/callPackage.md": "5ef6bc5d1a549c55d43ebb4d48c64427", "nix/callPackage.md": "59796c480e2856fa7491f62ceb7e3c9c",
"nix/index.md": "dd5ddd19e95d9bdbe020c68974d77a33", "nix/index.md": "dd5ddd19e95d9bdbe020c68974d77a33",
"journal/2024-02-02.md": "e2acbe75752d9c39875553223e34fb0d", "journal/2024-02-02.md": "e2acbe75752d9c39875553223e34fb0d",
"bash/prompts.md": "64bd3cd3c2feb9edb68ad8dc5ba65a35", "bash/prompts.md": "64bd3cd3c2feb9edb68ad8dc5ba65a35",
"algorithms/sorting/index.md": "cd189e1a2cf32b5656b16aaf9f488874", "algorithms/sorting/index.md": "cd189e1a2cf32b5656b16aaf9f488874",
"algorithms/sorting/insertion-sort.md": "c78c9983f87cdc4198f82803d418967f", "algorithms/sorting/insertion-sort.md": "c78c9983f87cdc4198f82803d418967f",
"algorithms/index.md": "1583c07edea4736db27c38fe2b6c4c31" "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": { "fields_dict": {
"Basic": [ "Basic": [

32
notes/algorithms/sorting/index.md
View File

@ -9,7 +9,36 @@ tags:
## Overview ## 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).
<!--ID: 1706981319280-->
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).
<!--ID: 1706981319310-->
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).
<!--ID: 1706981319317-->
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).
<!--ID: 1706981319324-->
END%%
%%ANKI %%ANKI
Basic 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). Reference: Thomas H. Cormen et al., _Introduction to Algorithms_, 3rd ed (Cambridge, Mass: MIT Press, 2009).
<!--ID: 1706925787146--> <!--ID: 1706925787146-->
END%% END%%
## Structural Comparison ## 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. 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.

18
notes/bash/prompts.md
View File

@ -8,7 +8,7 @@ tags:
## Overview ## 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 %%ANKI
Basic Basic
@ -18,6 +18,14 @@ Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 20
<!--ID: 1706882670149--> <!--ID: 1706882670149-->
END%% END%%
%%ANKI
Basic
What environment variable controls Bash's primary prompt?
Back: `$$PS1`
Reference: Cooper, Mendel. “Advanced Bash-Scripting Guide,” n.d., 916.
<!--ID: 1706973587222-->
END%%
%%ANKI %%ANKI
Basic Basic
What symbol is usually used to denote the secondary prompt? What symbol is usually used to denote the secondary prompt?
@ -26,6 +34,14 @@ Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 20
<!--ID: 1706882670158--> <!--ID: 1706882670158-->
END%% END%%
%%ANKI
Basic
What environment variable controls Bash's secondary prompt?
Back: `$$PS2`
Reference: Cooper, Mendel. “Advanced Bash-Scripting Guide,” n.d., 916.
<!--ID: 1706973587232-->
END%%
Paths supplied to commands are typically "sanitized" by prefixing the path name with `./`. This is mentioned in a few different places: 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. * `find -execdir` performs this prefixing automatically on all found files.

8
notes/bash/robustness.md
View File

@ -9,7 +9,7 @@ tags:
## Overview ## 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. > 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? * What happens if I run the command twice in a row?
* Whether a program acts atomically * Whether a program acts atomically
* Is it possible intermediate files are left that affect subsequent runs? * 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 ## References

148
notes/c/escape-sequences.md Normal file
View File

@ -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).
<!--ID: 1706975891805-->
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).
<!--ID: 1706975891810-->
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
<!--ID: 1706975891813-->
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
<!--ID: 1706975891817-->
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).
<!--ID: 1706975891820-->
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).
<!--ID: 1706975891824-->
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).
<!--ID: 1706975891828-->
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
<!--ID: 1706975891832-->
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
<!--ID: 1706975891835-->
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
<!--ID: 1706975891839-->
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
<!--ID: 1706976541399-->
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
<!--ID: 1706975891843-->
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
<!--ID: 1706976705750-->
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).

0
notes/c/index.md Normal file
View File

35
notes/gawk.md → notes/gawk/index.md
View File

@ -3,8 +3,6 @@ title: GAWK
TARGET DECK: Obsidian::STEM TARGET DECK: Obsidian::STEM
FILE TAGS: linux::cli gawk FILE TAGS: linux::cli gawk
tags: tags:
- linux
- cli
- gawk - gawk
--- ---
@ -198,39 +196,12 @@ Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 202
<!--ID: 1706883732944--> <!--ID: 1706883732944-->
END%% 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. You can specify a custom exit status by using the `exit` statement from within the `awk` program.
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)
<!--ID: 1706885111450-->
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)
<!--ID: 1706885111454-->
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)
<!--ID: 1706885111457-->
END%%
## References ## 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) * 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)

53
notes/gawk/variables.md Normal file
View File

@ -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)
<!--ID: 1706885111450-->
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)
<!--ID: 1706885111454-->
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)
<!--ID: 1706885111457-->
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)
<!--ID: 1706973587236-->
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)

16
notes/journal/2024-02-03.md Normal file
View File

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

0
notes/logic/index.md Normal file
View File

307
notes/logic/propositional.md Normal file
View File

@ -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.
<!--ID: 1706994861286-->
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.
<!--ID: 1706994861289-->
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.
<!--ID: 1706994861291-->
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.
<!--ID: 1706994861295-->
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
<!--ID: 1706994861298-->
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
<!--ID: 1706994861300-->
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
<!--ID: 1706994861302-->
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.
<!--ID: 1706994861304-->
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.
<!--ID: 1706994861306-->
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.
<!--ID: 1706994861308-->
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.
<!--ID: 1706994861310-->
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.
<!--ID: 1706994861312-->
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.
<!--ID: 1706994861314-->
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.
<!--ID: 1706994861316-->
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.
<!--ID: 1706994861318-->
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.
<!--ID: 1706994861320-->
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.
<!--ID: 1706994861323-->
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
<!--ID: 1706994861325-->
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
<!--ID: 1706994861327-->
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
<!--ID: 1706994861329-->
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
<!--ID: 1706994861331-->
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
<!--ID: 1706994861333-->
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.
<!--ID: 1706994861335-->
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.
<!--ID: 1706994861337-->
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.
<!--ID: 1706994861339-->
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.
<!--ID: 1706994861341-->
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.
<!--ID: 1706994861343-->
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.
<!--ID: 1706994861346-->
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.
<!--ID: 1706994861348-->
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.
<!--ID: 1706994861350-->
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.
<!--ID: 1706994861352-->
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.
<!--ID: 1706994861354-->
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.
<!--ID: 1706994861356-->
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.
<!--ID: 1706994861358-->
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.
<!--ID: 1706994861360-->
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.

0
notes/lua/index.md Normal file
View File

4
notes/nix/callPackage.md
View File

@ -90,7 +90,7 @@ callPackage = callPackageWith pkgs;
%%ANKI %%ANKI
Basic Basic
What two functions is `callPackage` implemented on top of? 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) 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)
<!--ID: 1706828138592--> <!--ID: 1706828138592-->
END%% END%%
@ -98,7 +98,7 @@ END%%
%%ANKI %%ANKI
Basic Basic
What is the purpose of `callPackage`? 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) 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)
<!--ID: 1706828138594--> <!--ID: 1706828138594-->
END%% END%%