Notes on textual substitution.

notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json

@@ -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",
+    "nix/index.md": "4efc7fcc4ea22834ba595497e5fb715c",
-    "posix/index.md": "f7b1ae55f8f5e8f50f89738b1aca9111",
+    "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",
+    "logic/normal-form.md": "f8fd5ea205dfb7e331356b0574f0fe14",
-    "_journal/2024-02-12.md": "a04ed5a77c12319ab80ba29b13526b3b",
+    "_journal/2024-02-12.md": "808cff0e8c1d9992ed65fed613afc98d",
-    "_journal/2024-02/2024-02-11.md": "afee9f502b61e17de231cf2f824fbb32"
+    "_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": [

notes/_journal/2024-02-12.md

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

notes/algorithms/index.md

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

notes/bash/index.md

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

notes/binary/index.md

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

notes/c/index.md

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

notes/c/strings.md

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

notes/encoding/ascii.md

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

notes/encoding/index.md

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

notes/gawk/variables.md

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

notes/logic/equiv-trans.md

@@ -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.
+**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$.
-
-$$\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?
+Textual substitution is derived from what equivalence rule?
-Back: Truth tables
+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?
+What is $E$'s role in textual substitution $E_e^x$?
-Back: $\lor$ separates disjuncts containing $\land$.
+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?
+What is $e$'s role in textual substitution $E_e^x$?
-Back: **D**isjunctive **N**ormal **F**orm.
+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?
+What is $x$'s role in textual substitution $E_e^x$?
-Back: **C**onjunctive **N**ormal **F**orm.
+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?
+How is textual substitution $E_e^x$ interpreted as a function?
-Back: $\land$ separates conjuncts containing $\lor$.
+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-->
+<!--ID: 1707762304130-->
-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-->
 END%%
 
 %%ANKI
 Basic
-What C operator corresponds to $\textbf{cand}$?
+Why does Gries prefer notation $E_e^x$ over e.g. $E(e)$?
-Back: `&&`
+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: 1707762304132-->
-<!--ID: 1707316606004-->
 END%%
 
 %%ANKI
 Basic
-Why is $\textbf{cand}$ named the way it is?
+What two scenarios ensure $E_e^x = E$ is an equivalence?
-Back: It is short for **c**onditional **and**.
+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?
+Why might $E_e^x = E$ be an equivalence despite identifier $x$ existing in $E$?
-Back: $\textbf{if } p \textbf{ then } q \textbf{ else } F$ 
+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?
+What is required for $E_e^x$ to be valid?
-Back: $F \textbf{ cand } U = F$
+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}$?
+What is the result of the following? $$(x < y \land (\forall i : 0 \leq i < n : b[i] < y))_z^x$$
-Back: `||`
+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: 1707762304139-->
-<!--ID: 1707316606007-->
 END%%
 
 %%ANKI
 Basic
-Why is $\textbf{cor}$ named the way it is?
+What is the result of the following? $$(x < y \land (\forall i : 0 \leq i < n : b[i] < y))_z^y$$
-Back: It is short for **c**onditional **or**.
+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?
+What is the result of the following? $$(x < y \land (\forall i : 0 \leq i < n : b[i] < y))_z^i$$
-Back: $\textbf{if } p \textbf{ then } T \textbf{ else } q$ 
+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?
+How is $E_{u_v^x}^x$ rewritten as sequential substitution?
-Back: $T \textbf{ cor } U = T$
+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-->
+<!--ID: 1707762304145-->
-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?
+Why is $(E_u^x)_v^x = E_{u_v^x}^x$ an equivalence?
-Back: $\textbf{cand}$ and $\textbf{cor}$
+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-->
+<!--ID: 1707762304146-->
-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}$?
+In what two scenarios is $(E_u^x)_v^y = E_{u_v^y}^x$ always an equivalence?
-Back: $\neg (E1 \textbf{ cor } E2) = \neg E1 \textbf{ cand } \neg E2$
+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
 

notes/logic/index.md

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

notes/logic/normal-form.md

@@ -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]]
+* [[truth-tables|Conjunctive Normal Form]]
-* [[equiv-trans#Normal Forms|Disjunctive Normal Form]]
+* [[truth-tables|Disjunctive Normal Form]]
 * [[quantification#Identifiers|Prenex Normal Form]]
 
 %%ANKI

notes/logic/short-circuit.md

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

notes/logic/truth-tables.md

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

notes/lua/index.md

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

notes/nix/index.md

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

notes/posix/index.md

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