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

Merge 2023-02-03 (#3) 

Science of programming and `awk`.

Reviewed-on: #3
Co-authored-by: Joshua Potter <jrpotter2112@gmail.com>
Co-committed-by: Joshua Potter <jrpotter2112@gmail.com>
daily
Joshua Potter 2024-02-04 00:20:31 +00:00 committed by jrpotter
parent 5425627df1
commit 5d4313023a
13 changed files with 602 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -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"
]
}
}
}

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

@ -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).
<!--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
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).
<!--ID: 1706925787146-->
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.

18
notes/bash/prompts.md
View File

@ -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
<!--ID: 1706882670149-->
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
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
<!--ID: 1706882670158-->
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:
* `find -execdir` performs this prefixing automatically on all found files.

8
notes/bash/robustness.md
View File

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

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
FILE TAGS: linux::cli gawk
tags:
- linux
- cli
- gawk
---
@ -198,39 +196,12 @@ Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 202
<!--ID: 1706883732944-->
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)
<!--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
* 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

6
notes/nix/callPackage.md
View File

@ -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)
<!--ID: 1706828138592-->
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)
<!--ID: 1706828138594-->
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)
* 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)