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

Compare commits

base: r:1c1ffb989afceffebca3580bd6afebe97afc29fc
Branches Tags
r:main
r:c-declarations
r:daily
...
compare: r:df45254a666c0b7ffdbc37c6a8681b3560e69c88
Branches Tags
r:main
r:c-declarations
r:daily

2 Commits
1c1ffb989a ... df45254a66

Author SHA1 Message Date
Joshua Potter df45254a66 Notes on textual substitution. 2024-02-12 11:27:16 -07:00
Joshua Potter 3e012b49b5 More tags. ASCII and c-style strings. 2024-02-12 10:18:47 -07:00
18 changed files with 522 additions and 151 deletions
Show Stats Expand all files Collapse all files

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

@ -78,29 +78,29 @@
"bubble-sort.gif"
],
"File Hashes": {
"algorithms/index.md": "1583c07edea4736db27c38fe2b6c4c31",
"algorithms/index.md": "a5ff7313f71777f1f3536e27dd9894fa",
"algorithms/sorting/index.md": "2d5a18a3079d96fa9e3d4289181a8b6c",
"algorithms/sorting/insertion-sort.md": "d40da14992d8331a07cebe1c4cfa41d4",
"bash/index.md": "3b5296277f095acdf16655adcdf524af",
"bash/index.md": "3dfeb538d781e4645e3aaaf32beb1034",
"bash/prompts.md": "61cb877e68da040a15b85af76b1f68ba",
"bash/quoting.md": "b1d8869a91001f8b22f0cdc54d806f61",
"bash/robustness.md": "7ab094b95ba2bfa885adba8e9efedf68",
"bash/shebang.md": "9006547710f9a079a3666169fbeda7aa",
"c/escape-sequences.md": "0d6219ebb51f6f21e026de67603e25b8",
"c/index.md": "aa8a34c62e7bc284ff589e28609222dc",
"c/index.md": "a021c92f19831bdd2bca4cbf813882fe",
"gawk/index.md": "0a305a0477085fd2f4145536735ca94a",
"gawk/variables.md": "8c567c9e387f1bed8200cf28a7e28502",
"gawk/variables.md": "7408f450957ab007fbdbd687121da0d3",
"index.md": "e48e895feeed7046425bb2ee15419770",
"journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970",
"journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb",
"journal/2024-02-02.md": "a3b222daee8a50bce4cbac699efc7180",
"journal/2024-02-03.md": "c6d411f0e2e964270399dd3a99f48382",
"logic/index.md": "3084b41fe1451259a0cf3e54560c2e85",
"logic/index.md": "46cdc7a552900e99a7d2d0140971118c",
"logic/propositional.md": "e7dbb24674336beb44dc9ef4c9ae51ff",
"lua/index.md": "26632dae1f852519e2f1af11d65c34eb",
"lua/index.md": "fd3d0b66765f0e9df233e8e02ce33e94",
"nix/callPackage.md": "140a02e57cd01d646483e3c21d72243d",
"nix/index.md": "dd5ddd19e95d9bdbe020c68974d77a33",
"posix/index.md": "f7b1ae55f8f5e8f50f89738b1aca9111",
"nix/index.md": "4efc7fcc4ea22834ba595497e5fb715c",
"posix/index.md": "97b1b8ecb9a953e855a9acf0ab25b8c8",
"posix/signals.md": "2120ddd933fc0d57abb93c33f639afd8",
"templates/daily.md": "7866014e730e85683155207a02e367d8",
"posix/regexp.md": "43825a1b9ed0dd7eeb1b6fe35c928bfe",
@ -114,7 +114,7 @@
"_journal/2024-02-02.md": "a3b222daee8a50bce4cbac699efc7180",
"_journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb",
"_journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970",
"logic/equiv-trans.md": "dfe893e20684c4d37c6c439a8722f7a6",
"logic/equiv-trans.md": "76f2416d78d6f44e5a7d88b806da6be9",
"_journal/2024-02-07.md": "8d81cd56a3b33883a7706d32e77b5889",
"algorithms/loop-invariants.md": "cbefc346842c21a6cce5c5edce451eb2",
"algorithms/loop-invariant.md": "d883dfc997ee28a7a1e24b995377792b",
@ -124,7 +124,7 @@
"algorithms/sorting/selection-sort.md": "73a077a726afd376650d1bd9e2d0bed9",
"algorithms/index 1.md": "6fada1f3d5d3af64687719eb465a5b97",
"binary/hexadecimal.md": "813512cb38700a8cb8ecf8ee9d6c9343",
"binary/index.md": "a67b5d0c8ac53e076590f315cce22201",
"binary/index.md": "ecb99ff4935e17317bf51f3ba45c1e41",
"_journal/2024-02-09.md": "a798d35f0b2bd1da130f7ac766166109",
"c/types.md": "cf3e66e5aee58a94db3fdf0783908555",
"logic/quantification.md": "37655276de8da531ca2b12706a639224",
@ -144,9 +144,14 @@
"_journal/2024-02/2024-02-10.md": "562b01f60ea36a3c78181e39b1c02b9f",
"_journal/2024-02-11.md": "afee9f502b61e17de231cf2f824fbb32",
"binary/endianness.md": "29c0aea671aa25aead580e9431aba8cc",
"logic/normal-form.md": "d6a79aa850e9830def15e9012a774057",
"_journal/2024-02-12.md": "a04ed5a77c12319ab80ba29b13526b3b",
"_journal/2024-02/2024-02-11.md": "afee9f502b61e17de231cf2f824fbb32"
"logic/normal-form.md": "f8fd5ea205dfb7e331356b0574f0fe14",
"_journal/2024-02-12.md": "808cff0e8c1d9992ed65fed613afc98d",
"_journal/2024-02/2024-02-11.md": "afee9f502b61e17de231cf2f824fbb32",
"encoding/ascii.md": "c01e50f96d0493d94dc4d520c0b6bb71",
"encoding/index.md": "071cfa6a5152efeda127b684f420d438",
"c/strings.md": "38f9cf9e2325565589f62e191221a83a",
"logic/truth-tables.md": "7892ceaa416c9a65acc79ca1e6ff778f",
"logic/short-circuit.md": "26d300f407f14883022d0ef8dc4f7300"
},
"fields_dict": {
"Basic": [

1
notes/_journal/2024-02-12.md
View File

@ -11,3 +11,4 @@ title: "2024-02-12"
- [ ] Log Work Hours (Max 3 hours)
* Read 삼 년 고개 (Three-Years Hill).
* Notes on ASCII and C-style strings.

2
notes/algorithms/index.md
View File

@ -1,3 +1,5 @@
---
title: Algorithms
tags:
- algorithm
---

2
notes/bash/index.md
View File

@ -1,3 +1,5 @@
---
title: Bash
tags:
- bash
---

2
notes/binary/index.md
View File

@ -1,3 +1,5 @@
---
title: Binary
tags:
- binary
---

2
notes/c/index.md
View File

@ -1,3 +1,5 @@
---
title: C
tags:
- c
---

47
notes/c/strings.md Normal file
View File

@ -0,0 +1,47 @@
---
title: Strings
TARGET DECK: Obsidian::STEM
FILE TAGS: c
tags:
- c
---
## Overview
A contiguous sequence of characters terminated by the `NUL` character (refer to [[ascii|ASCII]]). Text data is said to be more platform-independent than [[endianness|binary]] data since it is unaffected by word size or byte ordering.
%%ANKI
Basic
What is a C-style string?
Back: A character array terminated with a `NUL` character.
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
<!--ID: 1707758281264-->
END%%
%%ANKI
Basic
What character terminates all C-style strings?
Back: `NUL`
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
<!--ID: 1707758281266-->
END%%
%%ANKI
Basic
What is the decimal value of `NUL` in ASCII encoding?
Back: `0`
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
<!--ID: 1707758281268-->
END%%
%%ANKI
Basic
Text is more platform-independent than binary because it is unaffected by what two properties?
Back: Word size and byte ordering.
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
<!--ID: 1707758281270-->
END%%
## References
* Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.

92
notes/encoding/ascii.md Normal file
View File

@ -0,0 +1,92 @@
---
title: ASCII
TARGET DECK: Obsidian::STEM
FILE TAGS: encoding::ascii
tags:
- encoding
- ascii
---
## Overview
A character encoding containing 128 code points, 95 of which are printable. Use the Unix command `ascii` to print out the following table:
```text
Dec Hex Dec Hex Dec Hex Dec Hex Dec Hex Dec Hex Dec Hex Dec Hex
0 00 NUL 16 10 DLE 32 20 48 30 0 64 40 @ 80 50 P 96 60 ` 112 70 p
1 01 SOH 17 11 DC1 33 21 ! 49 31 1 65 41 A 81 51 Q 97 61 a 113 71 q
2 02 STX 18 12 DC2 34 22 " 50 32 2 66 42 B 82 52 R 98 62 b 114 72 r
3 03 ETX 19 13 DC3 35 23 # 51 33 3 67 43 C 83 53 S 99 63 c 115 73 s
4 04 EOT 20 14 DC4 36 24 $ 52 34 4 68 44 D 84 54 T 100 64 d 116 74 t
5 05 ENQ 21 15 NAK 37 25 % 53 35 5 69 45 E 85 55 U 101 65 e 117 75 u
6 06 ACK 22 16 SYN 38 26 & 54 36 6 70 46 F 86 56 V 102 66 f 118 76 v
7 07 BEL 23 17 ETB 39 27 ' 55 37 7 71 47 G 87 57 W 103 67 g 119 77 w
8 08 BS 24 18 CAN 40 28 ( 56 38 8 72 48 H 88 58 X 104 68 h 120 78 x
9 09 HT 25 19 EM 41 29 ) 57 39 9 73 49 I 89 59 Y 105 69 i 121 79 y
10 0A LF 26 1A SUB 42 2A * 58 3A : 74 4A J 90 5A Z 106 6A j 122 7A z
11 0B VT 27 1B ESC 43 2B + 59 3B ; 75 4B K 91 5B [ 107 6B k 123 7B {
12 0C FF 28 1C FS 44 2C , 60 3C < 76 4C L 92 5C \ 108 6C l 124 7C |
13 0D CR 29 1D GS 45 2D - 61 3D = 77 4D M 93 5D ] 109 6D m 125 7D }
14 0E SO 30 1E RS 46 2E . 62 3E > 78 4E N 94 5E ^ 110 6E n 126 7E ~
15 0F SI 31 1F US 47 2F / 63 3F ? 79 4F O 95 5F _ 111 6F o 127 7F DEL
```
%%ANKI
Basic
What is a character encoding?
Back: The assignment of numbers to graphical characters.
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
<!--ID: 1707757786284-->
END%%
%%ANKI
Basic
How many code points are defined in ASCII?
Back: 128
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
<!--ID: 1707757786288-->
END%%
%%ANKI
Basic
How many *printable* code points are defined in ASCII?
Back: 95
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
<!--ID: 1707757786289-->
END%%
%%ANKI
Basic
What program can be used to print an ASCII table to the console?
Back: `ascii`
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
<!--ID: 1707757786291-->
END%%
%%ANKI
Basic
How many bits make up an ASCII character?
Back: `7`
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
<!--ID: 1707757786292-->
END%%
%%ANKI
Basic
What is the largest ASCII decimal value?
Back: `127`
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
<!--ID: 1707757786294-->
END%%
%%ANKI
Basic
What is the largest ASCII hexadecimal value?
Back: `0x7F`
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
<!--ID: 1707757786295-->
END%%
## References
* Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.

5
notes/encoding/index.md Normal file
View File

@ -0,0 +1,5 @@
---
title: Encoding
tags:
- encoding
---

30
notes/gawk/variables.md
View File

@ -213,6 +213,36 @@ Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 202
<!--ID: 1707618833558-->
END%%
%%ANKI
Cloze
Setting `FS` to {`""`} allows examining {each character of a record separately}.
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: 1707756447064-->
END%%
%%ANKI
Cloze
Setting `FS` to {`"\n"`} treats the {record as the single 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)
<!--ID: 1707756447067-->
END%%
%%ANKI
Basic
What value of `FS` ensures `$1 = $0`?
Back: `"\n"`
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: 1707756447069-->
END%%
%%ANKI
Basic
*Why* does `awk` support a CSV mode?
Back: Because CSV fields may contain commas and newlines.
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: 1707756447071-->
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)

210
notes/logic/equiv-trans.md
View File

@ -617,218 +617,158 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in
<!--ID: 1707316276203-->
END%%
## Normal Forms
## Textual Substitution
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)
)
$$
**Textual substitution** refers to the simultaneous replacement of a free identifier with an expression, introducing parentheses as necessary. This concept is just the [[#Equivalence Rules|Substitution Rule]] with different notation. For example, let $E$ and $e$ be expressions and $x$ an identifer. Then $$E_e^x$$ denotes the simultaneous replacement of all free occurrences of $x$ with $e$.
%%ANKI
Basic
What construct is used to prove every proposition can be written in DNF or CNF?
Back: Truth tables
Textual substitution is derived from what equivalence rule?
Back: The substitution rule.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707311868994-->
<!--ID: 1707762304123-->
END%%
%%ANKI
Basic
Where are $\land$ and $\lor$ found within a DNF proposition?
Back: $\lor$ separates disjuncts containing $\land$.
What is $E$'s role in textual substitution $E_e^x$?
Back: It is the expression that free occurrences of $x$ are replaced with $e$ in.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707311868998-->
<!--ID: 1707762304126-->
END%%
%%ANKI
Basic
What is DNF an acronym for?
Back: **D**isjunctive **N**ormal **F**orm.
What is $e$'s role in textual substitution $E_e^x$?
Back: It is the expression that free occurrences of $x$ in $E$ are substituted with.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707311869000-->
<!--ID: 1707762304127-->
END%%
%%ANKI
Basic
What is CNF an acronym for?
Back: **C**onjunctive **N**ormal **F**orm.
What is $x$'s role in textual substitution $E_e^x$?
Back: It is the identifier matching free occurrences in $E$ that are replaced with $e$.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707311869002-->
<!--ID: 1707762304129-->
END%%
%%ANKI
Basic
Where are $\land$ and $\lor$ found within a CNF proposition?
Back: $\land$ separates conjuncts containing $\lor$.
How is textual substitution $E_e^x$ interpreted as a function?
Back: As $E(e)$, where $E$ is a function of $x$.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707311869003-->
END%%
## Short-Circuit Evaluation
The $\textbf{cand}$ and $\textbf{cor}$ operator allows short-circuiting evaluation in the case of undefined ($U$) values.
%%ANKI
Basic
What truth values do short-circuit evaluation operators act on?
Back: $T$, $F$, and $U$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708622-->
<!--ID: 1707762304130-->
END%%
%%ANKI
Basic
What C operator corresponds to $\textbf{cand}$?
Back: `&&`
Why does Gries prefer notation $E_e^x$ over e.g. $E(e)$?
Back: The former indicates the identifier to replace.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
Tags: c
<!--ID: 1707316606004-->
<!--ID: 1707762304132-->
END%%
%%ANKI
Basic
Why is $\textbf{cand}$ named the way it is?
Back: It is short for **c**onditional **and**.
What two scenarios ensure $E_e^x = E$ is an equivalence?
Back: $x = e$ or no free occurrences of $x$ exist in $E$.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708625-->
<!--ID: 1707762304133-->
END%%
%%ANKI
Basic
How is $p \textbf{ cand } q$ written as a conditional?
Back: $\textbf{if } p \textbf{ then } q \textbf{ else } F$
Why might $E_e^x = E$ be an equivalence despite identifier $x$ existing in $E$?
Back: If the only occurrences of $x$ in $E$ are bound.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708627-->
<!--ID: 1707762304135-->
END%%
%%ANKI
Basic
When can $\textbf{cand}$ evaluate to a non-$U$ value despite being given a $U$ operand?
Back: $F \textbf{ cand } U = F$
What is required for $E_e^x$ to be valid?
Back: Substitution must result in a syntactically valid expression.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708628-->
<!--ID: 1707762304137-->
END%%
%%ANKI
Basic
What C operator corresponds to $\textbf{cor}$?
Back: `||`
What is the result of the following? $$(x < y \land (\forall i : 0 \leq i < n : b[i] < y))_z^x$$
Back: $$(z < y \land (\forall i : 0 \leq i < n : b[i] < y))$$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
Tags: c
<!--ID: 1707316606007-->
<!--ID: 1707762304139-->
END%%
%%ANKI
Basic
Why is $\textbf{cor}$ named the way it is?
Back: It is short for **c**onditional **or**.
What is the result of the following? $$(x < y \land (\forall i : 0 \leq i < n : b[i] < y))_z^y$$
Back: $$(x < z \land (\forall i : 0 \leq i < n : b[i] < z))$$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708630-->
<!--ID: 1707762304140-->
END%%
%%ANKI
Basic
How is $p \textbf{ cor } q$ written as a conditional?
Back: $\textbf{if } p \textbf{ then } T \textbf{ else } q$
What is the result of the following? $$(x < y \land (\forall i : 0 \leq i < n : b[i] < y))_z^i$$
Back: $$(x < y \land (\forall i : 0 \leq i < n : b[i] < y))$$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708632-->
<!--ID: 1707762304141-->
END%%
* $(E_u^x)_v^x = E_{u_v^x}^x$
* The only possible free occurrences of $x$ that may appear after the first of the sequential substitutions occur in $u$.
* If $y$ is not free in $E$, then $(E_u^x)_v^y = E_{u_v^y}^x$.
* $y$ may not be free in $E$ but substituting $x$ with $u$ can introduce a free occurrence. It doesn't matter if we perform the substitution first or second though.
%%ANKI
Basic
How do we simplify $(E_u^x)_v^x$?
Back: As $E_{u_v^x}^x$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707762304143-->
END%%
%%ANKI
Basic
When can $\textbf{cor}$ evaluate to a non-$U$ value despite being given a $U$ operand?
Back: $T \textbf{ cor } U = T$
How is $E_{u_v^x}^x$ rewritten as sequential substitution?
Back: As $(E_u^x)_v^x$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708633-->
END%%
* Associative Laws
* $E1 \textbf{ cand } (E2 \textbf{ cand } E3) = (E1 \textbf{ cand } E2) \textbf{ cand } E3$
* $E1 \textbf{ cor } (E2 \textbf{ cor } E3) = (E1 \textbf{ cor } E2) \textbf{ cor } E3$
%%ANKI
Basic
Which of the short-circuit logical operators do the commutative laws apply to?
Back: Neither of them.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708635-->
<!--ID: 1707762304145-->
END%%
%%ANKI
Basic
Which of the short-circuit logical operators do the associative laws apply to?
Back: $\textbf{cand}$ and $\textbf{cor}$
Why is $(E_u^x)_v^x = E_{u_v^x}^x$ an equivalence?
Back: After the first substitution, the only possible free occurrences of $x$ are in $u$.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708636-->
END%%
* Distributive Laws
* $E1 \textbf{ cand } (E2 \textbf{ cor } E3) = (E1 \textbf{ cand } E2) \textbf{ cor } (E1 \textbf{ cand } E3)$
* $E1 \textbf{ cor } (E2 \textbf{ cand } E3) = (E1 \textbf{ cor } E2) \textbf{ cand } (E1 \textbf{ cor } E3)$
%%ANKI
Basic
What is the distributive law of e.g. $\textbf{cor}$ over $\textbf{cand}$?
Back: $E1 \textbf{ cor } (E2 \textbf{ cand } E3) = (E1 \textbf{ cor } E2) \textbf{ cand } (E1 \textbf{ cor } E3)$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708638-->
END%%
* De Morgan's Laws
* $\neg (E1 \textbf{ cand } E2) = \neg E1 \textbf{ cor } \neg E2$
* $\neg (E1 \textbf{ cor } E2) = \neg E1 \textbf{ cand } \neg E2$
%%ANKI
Basic
Which of the short-circuit logical operators do De Morgan's Laws apply to?
Back: $\textbf{cand}$ and $\textbf{cor}$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708640-->
<!--ID: 1707762304146-->
END%%
%%ANKI
Basic
What is De Morgan's Law of e.g. $\textbf{cor}$?
Back: $\neg (E1 \textbf{ cor } E2) = \neg E1 \textbf{ cand } \neg E2$
In what two scenarios is $(E_u^x)_v^y = E_{u_v^y}^x$ always an equivalence?
Back: $x = y$ or $y$ is not free in $E$.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708642-->
<!--ID: 1707762304148-->
END%%
Gries lists other "Laws" but they don't seem as important to note here. What's worth noting is that the other [[#Equivalence Schemas]] listed above still apply if we can limit operands to just $T$ and $F$.
%%ANKI
Basic
If $x \neq y$, when is $(E_u^x)_v^y = E_{u_v^y}^x$?
Back: When $y$ is not free in $E$.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707762304150-->
END%%
%%ANKI
Basic
Why should $y$ not be free in $E$ for $(E_u^x)_v^y = E_{u_v^y}^x$ to be an equivalence?
Back: If it were, a $v$ would exist in the LHS that doesn't in the RHS.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707762304152-->
END%%
## References

2
notes/logic/index.md
View File

@ -1,3 +1,5 @@
---
title: Logic
tags:
- logic
---

4
notes/logic/normal-form.md
View File

@ -10,8 +10,8 @@ tags:
An object is said to be in **normal form** if it cannot be reduced any further. Examples of normal form include:
* [[equiv-trans#Normal Forms|Conjunctive Normal Form]]
* [[equiv-trans#Normal Forms|Disjunctive Normal Form]]
* [[truth-tables|Conjunctive Normal Form]]
* [[truth-tables|Disjunctive Normal Form]]
* [[quantification#Identifiers|Prenex Normal Form]]
%%ANKI

143
notes/logic/short-circuit.md Normal file
View File

@ -0,0 +1,143 @@
---
title: Short-Circuit
TARGET DECK: Obsidian::STEM
FILE TAGS: logic
tags:
- logic
---
## Overview
The $\textbf{cand}$ and $\textbf{cor}$ operator allows short-circuiting evaluation in the case of undefined ($U$) values.
%%ANKI
Basic
What truth values do short-circuit evaluation operators act on?
Back: $T$, $F$, and $U$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708622-->
END%%
%%ANKI
Basic
What C operator corresponds to $\textbf{cand}$?
Back: `&&`
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
Tags: c
<!--ID: 1707316606004-->
END%%
%%ANKI
Basic
Why is $\textbf{cand}$ named the way it is?
Back: It is short for **c**onditional **and**.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708625-->
END%%
%%ANKI
Basic
How is $p \textbf{ cand } q$ written as a conditional?
Back: $\textbf{if } p \textbf{ then } q \textbf{ else } F$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708627-->
END%%
%%ANKI
Basic
When can $\textbf{cand}$ evaluate to a non-$U$ value despite being given a $U$ operand?
Back: $F \textbf{ cand } U = F$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708628-->
END%%
%%ANKI
Basic
What C operator corresponds to $\textbf{cor}$?
Back: `||`
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
Tags: c
<!--ID: 1707316606007-->
END%%
%%ANKI
Basic
Why is $\textbf{cor}$ named the way it is?
Back: It is short for **c**onditional **or**.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708630-->
END%%
%%ANKI
Basic
How is $p \textbf{ cor } q$ written as a conditional?
Back: $\textbf{if } p \textbf{ then } T \textbf{ else } q$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708632-->
END%%
%%ANKI
Basic
When can $\textbf{cor}$ evaluate to a non-$U$ value despite being given a $U$ operand?
Back: $T \textbf{ cor } U = T$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708633-->
END%%
* Associative Laws
* $E1 \textbf{ cand } (E2 \textbf{ cand } E3) = (E1 \textbf{ cand } E2) \textbf{ cand } E3$
* $E1 \textbf{ cor } (E2 \textbf{ cor } E3) = (E1 \textbf{ cor } E2) \textbf{ cor } E3$
%%ANKI
Basic
Which of the short-circuit logical operators do the commutative laws apply to?
Back: Neither of them.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708635-->
END%%
%%ANKI
Basic
Which of the short-circuit logical operators do the associative laws apply to?
Back: $\textbf{cand}$ and $\textbf{cor}$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708636-->
END%%
* Distributive Laws
* $E1 \textbf{ cand } (E2 \textbf{ cor } E3) = (E1 \textbf{ cand } E2) \textbf{ cor } (E1 \textbf{ cand } E3)$
* $E1 \textbf{ cor } (E2 \textbf{ cand } E3) = (E1 \textbf{ cor } E2) \textbf{ cand } (E1 \textbf{ cor } E3)$
%%ANKI
Basic
What is the distributive law of e.g. $\textbf{cor}$ over $\textbf{cand}$?
Back: $E1 \textbf{ cor } (E2 \textbf{ cand } E3) = (E1 \textbf{ cor } E2) \textbf{ cand } (E1 \textbf{ cor } E3)$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708638-->
END%%
* De Morgan's Laws
* $\neg (E1 \textbf{ cand } E2) = \neg E1 \textbf{ cor } \neg E2$
* $\neg (E1 \textbf{ cor } E2) = \neg E1 \textbf{ cand } \neg E2$
%%ANKI
Basic
Which of the short-circuit logical operators do De Morgan's Laws apply to?
Back: $\textbf{cand}$ and $\textbf{cor}$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708640-->
END%%
%%ANKI
Basic
What is De Morgan's Law of e.g. $\textbf{cor}$?
Back: $\neg (E1 \textbf{ cor } E2) = \neg E1 \textbf{ cand } \neg E2$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707317708642-->
END%%
Gries lists other "Laws" but they don't seem as important to note here. What's worth noting is that the other [[equiv-trans#Equivalence Schemas|equivalence schemas]] still apply if we can limit operands to just $T$ and $F$.
## References
* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

92
notes/logic/truth-tables.md Normal file
View File

@ -0,0 +1,92 @@
---
title: Truth Tables
TARGET DECK: Obsidian::STEM
FILE TAGS: logic
tags:
- logic
---
## Overview
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.
<!--ID: 1707311868994-->
END%%
%%ANKI
Basic
Where are $\land$ and $\lor$ found within a DNF proposition?
Back: $\lor$ separates disjuncts containing $\land$.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707311868998-->
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.
<!--ID: 1707311869000-->
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.
<!--ID: 1707311869002-->
END%%
%%ANKI
Basic
Where are $\land$ and $\lor$ found within a CNF proposition?
Back: $\land$ separates conjuncts containing $\lor$.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707311869003-->
END%%
## References
* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

2
notes/lua/index.md
View File

@ -1,3 +1,5 @@
---
title: Lua
tags:
- lua
---

2
notes/nix/index.md
View File

@ -1,3 +1,5 @@
---
title: Nix
tags:
- nix
---

2
notes/posix/index.md
View File

@ -1,3 +1,5 @@
---
title: POSIX
tags:
- posix
---