Additional notes on assignment and textual substitution.

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

@@ -183,7 +183,7 @@
     "_journal/2024-02-02.md": "a3b222daee8a50bce4cbac699efc7180",
     "_journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb",
     "_journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970",
-    "logic/equiv-trans.md": "34c29b7686b373916e247f700be488b9",
+    "logic/equiv-trans.md": "d05cbd53c1c18ffd36f9117479bbc1fd",
     "_journal/2024-02-07.md": "8d81cd56a3b33883a7706d32e77b5889",
     "algorithms/loop-invariants.md": "cbefc346842c21a6cce5c5edce451eb2",
     "algorithms/loop-invariant.md": "3b390e720f3b2a98e611b49a0bb1f5a9",
@@ -447,7 +447,7 @@
     "_journal/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b",
     "_journal/2024-05/2024-05-12.md": "ca9f3996272152ef89924bb328efd365",
     "git/remotes.md": "cbe2cd867f675f156e7fe71ec615890d",
-    "programming/pred-trans.md": "ea5555291f8cdd3974ac09ea7b120a16",
+    "programming/pred-trans.md": "78abe68030d68e5b253564920ee85cfb",
     "set/axioms.md": "063955bf19c703e9ad23be2aee4f1ab7",
     "_journal/2024-05-14.md": "f6ece1d6c178d57875786f87345343c5",
     "_journal/2024-05/2024-05-13.md": "71eb7924653eed5b6abd84d3a13b532b",
@@ -618,7 +618,7 @@
     "abstract-rewriting-systems/normal-form.md": "2fff9a1d85bca0a2941a54b0084a0309",
     "_journal/2024-07-19.md": "ced9d4c4759468885d85efa0b87b7823",
     "_journal/2024-07/2024-07-18.md": "237918b58424435959cbc949d01e7932",
-    "_journal/2024-07-20.md": "aa70e639c362764a930c2fa71e030768",
+    "_journal/2024-07-20.md": "d8685729effc374e4ece1e618c2fdad3",
     "_journal/2024-07/2024-07-19.md": "e9fe4569f88e1ba9393292bcf092edfc"
   },
   "fields_dict": {

notes/_journal/2024-07-20.md

@@ -9,3 +9,5 @@ title: "2024-07-20"
 - [ ] Korean (Read 1 Story)
 
 * Begin notes on [[hashing/index#Random Hashing|random hashing]] and, more specifically, [[hashing/index#Universal Hashing|universal hashing]].
+* Notes on generalized [[equiv-trans#General|textual substitution]] and [[pred-trans#General|assignment]].
+* Finished chapter 9 "Assignment Command" of "The Science of Programming".

notes/logic/equiv-trans.md

@@ -591,6 +591,30 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in
 <!--ID: 1714395640953-->
 END%%
 
+%%ANKI
+Basic
+Consider selector update syntax. Is precedence left-to-right or right-to-left?
+Back: Right-to-left.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721497014090-->
+END%%
+
+%%ANKI
+Basic
+What does it mean for selector update syntax to have right-to-left precedence?
+Back: Rightmost selectors overwrite duplicate selectors.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721497014094-->
+END%%
+
+%%ANKI
+Basic
+How is $(b; s_1{:}e_1; s_2{:}e_2; s_1{:}e_3)$ simplified?
+Back: As $(b; s_2{:}e_2; s_1{:}e_3)$.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721497014098-->
+END%%
+
 ## Substitution
 
 **Textual substitution** refers to the replacement of a [[pred-logic#Identifiers|free]] identifier with an expression, introducing parentheses as necessary. This concept amounts to the [[#Equivalence Rules|Substitution Rule]] with different notation.
@@ -751,16 +775,150 @@ Substitution is defined recursively as follows:
 
 1. If each $x_i$ is a distinct identifier with a null selector, then $E_{\bar{e}}^{\bar{x}}$ is the simultaneous substitution of $\bar{x}$ with $\bar{e}$.
 2. Adjacent reference-expression pairs may be permuted as long as they begin with different identifiers. That is, for all distinct $b$ and $c$, $$\Large{E_{\bar{e}, \,f, \,h, \,\bar{g}}^{\bar{x}, \,b, \,c, \,\bar{y}} = E_{\bar{x}, \,h, \,f, \,\bar{g}}^{\bar{x}, \,c, \,b, \,\bar{y}}}$$
-3. Multiple assignments to subparts of an object $b$ can be viewed as a single assignment to $b$. That is, provided $b$ does not begin any of the $x_i$, $$\Large{E_{e_1, \,\ldots, \,e_m, \,\bar{g}}^{b \circ s_1, \,\ldots, \,b \circ s_m, \,\bar{x}} = E_{(b; \,s_1{:}e_1; \,\cdots; \,s_m{:}e_m), \,\bar{g}}^{b, \,\bar{x}}}$$
+3. Multiple assignments to subparts of an object $b$ can be viewed as a single assignment to $b$. That is, provided $b$ does not begin any of the $x_i$, $$\Large{E_{e_1, \,\ldots, \,e_m, \,\bar{g}}^{b \,\circ\, s_1, \,\ldots, \,b \,\circ\, s_m, \,\bar{x}} = E_{(b; \,s_1{:}e_1; \,\cdots; \,s_m{:}e_m), \,\bar{g}}^{b, \,\bar{x}}}$$
 
 Note that simultaneous substitution is different from sequential substitution.
 
-TODO
+%%ANKI
+Basic
+Consider $E_{\bar{e}}^{\bar{x}}$. What is each $x_i$ in $\bar{x}$?
+Back: An identifier concatenated with a selector.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721495879842-->
+END%%
+
+%%ANKI
+Basic
+Consider $E_{\bar{e}}^{\bar{x}}$. What is each $e_i$ in $\bar{e}$?
+Back: An expression.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721495879845-->
+END%%
+
+%%ANKI
+Basic
+What is the base case in the evaluation of $E_{\bar{e}}^{\bar{x}}$?
+Back: If $\bar{x}$ are distinct identifiers with null selectors, direct simultaneous substitution.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721495879846-->
+END%%
+
+%%ANKI
+Basic
+Which of $E_{\bar{e}}^{\bar{x}}$'s reference-expression pairs may be moved?
+Back: Adjacent pairs with distinct identifiers.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721495879847-->
+END%%
+
+%%ANKI
+Basic
+When is $b_1 \circ s_1$ and $b_2 \circ s_2$ said to have distinct identifiers?
+Back: When $b_1 \neq b_2$.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721495879848-->
+END%%
+
+%%ANKI
+Basic
+When is $b_1 \circ s_1$ and $b_2 \circ s_2$ said to have distinct selectors?
+Back: When $s_1 \neq s_2$.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721495879850-->
+END%%
+
+%%ANKI
+Basic
+Suppose $x$ and $y$ are distinct. Is the following a tautology? $$\large{E_{e_1, e_2}^{x, y} = E_{e_2, e_1}^{y, x}}$$
+Back: Yes.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721495879851-->
+END%%
+
+%%ANKI
+Basic
+When is the following a tautology? $$\large{E_{e_1, e_2}^{x, y} = E_{e_2, e_1}^{y, x}}$$
+Back: When $x$ and $y$ refer to distinct identifiers.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721495879852-->
+END%%
+
+%%ANKI
+Basic
+Suppose $x = y$. When is the following a tautology? $$\large{E_{e_1, e_2}^{x, y} = E_{e_2, e_1}^{x, y}}$$
+Back: When $e_1 = e_2$.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721495879853-->
+END%%
+
+%%ANKI
+Basic
+Suppose $x$, $y$, and $z$ are distinct. What is the result of a single evaluation step? $$\large{E_{e_1, e_2, e_3}^{x, y, z}}$$
+Back: N/A.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721495879854-->
+END%%
+
+%%ANKI
+Basic
+Suppose $x \neq y$. What is the result of a single evaluation step? $$\large{E_{e_1, e_2, e_3}^{x, y, x}}$$
+Back: $$\large{E_{e_1, e_3, e_2}^{x, x, y}}$$
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721495879855-->
+END%%
+
+%%ANKI
+Basic
+Suppose $x \neq y$. What is the result of a single evaluation step? $$\large{E_{e_1, e_3, e_2}^{x, x, y}}$$
+Back: $$\large{E_{(x; \,\epsilon{:}e_1; \,\epsilon{:}e_3), e_2}^{x, y}}$$
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721495879856-->
+END%%
+
+%%ANKI
+Basic
+Suppose $x \neq y$. What is the result of a single evaluation step? $$\large{E_{(x; \,\epsilon{:}e_1; \,\epsilon{:}e_3), e_2}^{x, y}}$$
+Back: $$\large{E_{e_3, e_2}^{x, y}}$$
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721495879857-->
+END%%
+
+%%ANKI
+Basic
+Suppose $x \neq y$. *Why* isn't the following a tautology? $$\large{E_{e_1, e_2, e_3}^{x, y, x}} = E_{(x; \epsilon{:}e_1), e_2, e_3}^{x, y, x}$$
+Back: N/A. It is.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721495879858-->
+END%%
+
+%%ANKI
+Basic
+Suppose $x \neq y$. *Why* isn't the following a tautology? $$\large{E_{e_1, e_2, e_3, e_4}^{x, x, y, x}} = E_{(x; \epsilon{:}e_1; \epsilon{:}e_2), e_3, e_4}^{x, y, x}$$
+Back: Because not every $x$ was made adjacent before grouping.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721495879859-->
+END%%
+
+%%ANKI
+Basic
+Consider array $b$ and $i \in \mathop{domain}(b)$. What is the result of a single evaluation step? $$\large{E_{e}^{b[i]}}$$
+Back: $$\large{E_{(b; [i]{:}e)}^{b}}$$
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721495879860-->
+END%%
+
+%%ANKI
+Basic
+Consider identifier $x$, array $b$ and $i \in \mathop{domain}(b)$. What is the result of a single evaluation step? $$\large{E_{b[i]}^{x}}$$
+Back: N/A.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721495879861-->
+END%%
 
 ### Theorems
 
 * $(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$.
+	* The only possible free occurrences of $x$ that may appear after the first of the substitutions occur in $u$.
 
 %%ANKI
 Basic
@@ -780,13 +938,13 @@ END%%
 
 %%ANKI
 Basic
-Why is $(E_u^x)_v^x = E_{u_v^x}^x$ an equivalence?
+*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: 1707762304146-->
 END%%
 
-* If $y$ is not free in $E$, then $(E_u^x)_v^y = E_{u_v^y}^x$.
+* If $y \not\in FV(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
@@ -807,7 +965,7 @@ 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?
+Why does $y \not\in FV(E)$ ensure $(E_u^x)_v^y = E_{u_v^y}^x$ is 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-->
@@ -918,7 +1076,7 @@ END%%
 %%ANKI
 Basic
 When is $(E_{\bar{u}}^{\bar{x}})_{\bar{x}}^{\bar{u}} = E$ guaranteed to be an equivalence?
-Back: When $\bar{x}$ and $\bar{u}$ refer to distinct identifiers.
+Back: When $\bar{x}$ and $\bar{u}$ refer to distinct identifiers (concatenated with selectors).
 Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
 <!--ID: 1707939006297-->
 END%%

notes/programming/pred-trans.md

@@ -622,6 +622,14 @@ END%%
 
 ### Assignment
 
+%%ANKI
+Basic
+What equivalence transformation rule is assignment related to?
+Back: Substitution.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721497014026-->
+END%%
+
 #### Simple
 
 The assignment command has form $x \coloneqq e$, provided the types of $x$ and $e$ are the same. This command is read as "$x$ becomes $e$" and is defined as $$wp(''x \coloneqq e'', R) = domain(e) \textbf{ cand } R_e^x$$
@@ -757,7 +765,112 @@ END%%
 
 #### General
 
-TODO
+The multiple assignment command has form $$x_1 \circ s_1, \cdots, x_n \circ s_n \coloneqq e_1, \cdots, e_n$$
+where each $x_i$ is an identifier, each $s_i$ is a [[equiv-trans#Selectors|selector]], and each expression $e_i$ has the same type as $x_i \circ s_i$. We denote this assignment more compactly as $\bar{x} \coloneqq \bar{e}$. We define multiple assignment as $$wp(''\bar{x} \coloneqq \bar{e}'', R) = domain(\bar{e}) \textbf{ cand } R_{\bar{e}}^\bar{x}$$
+
+%%ANKI
+Basic
+How is $x \coloneqq e$ expressed in more general form $x_1 \circ s_1, \ldots, x_n \circ s_n \coloneqq e_1, \ldots, e_n$?
+Back: As $x \circ \epsilon \coloneqq e$.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721497014033-->
+END%%
+
+%%ANKI
+Basic
+How is $b[i] \coloneqq e$ expressed in more general form $x_1 \circ s_1, \ldots, x_n \circ s_n \coloneqq e_1, \ldots, e_n$?
+Back: As $b \circ [i] \coloneqq e$.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721497014038-->
+END%%
+
+%%ANKI
+Basic
+Consider assignment command $\bar{x} \coloneqq \bar{e}$. In what order must $\bar{e}$ be evaluated?
+Back: In any order.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721497014043-->
+END%%
+
+%%ANKI
+Basic
+Consider assignment command $\bar{x} \coloneqq \bar{e}$. In what order must assignment be performed?
+Back: Left-to-right.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721497014047-->
+END%%
+
+%%ANKI
+Basic
+*Why* must assignment in $\bar{x} \coloneqq \bar{e}$ happen left-to-right?
+Back: Because update selector syntax has right-to-left precedence.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721497014051-->
+END%%
+
+%%ANKI
+Basic
+Consider assignment command $\bar{x} \coloneqq \bar{e}$. When can assignment be performed in any order?
+Back: When the identifiers in $\bar{x}$ are distinct.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721497014055-->
+END%%
+
+%%ANKI
+Basic
+The general assignment command has what form?
+Back: $\bar{x} \coloneqq \bar{e}$
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721497014059-->
+END%%
+
+%%ANKI
+Basic
+How is assignment "$\bar{x} \coloneqq \bar{e}$" defined in terms of $wp$?
+Back: $wp(''\bar{x} \coloneqq \bar{e}'', R) = domain(\bar{e}) \textbf{ cand } R_{\bar{e}}^{\bar{x}}$
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721497014064-->
+END%%
+
+%%ANKI
+Basic
+In the $wp$ definition of "$\bar{x} \coloneqq \bar{e}$", what does $domain(\bar{e})$ refer to?
+Back: A predicate that holds if each member of $\bar{e}$ is well-defined.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721497014068-->
+END%%
+
+%%ANKI
+Basic
+In the $wp$ definition of "$\bar{x} \coloneqq \bar{e}$", $domain(\bar{e})$ must exclude which states?
+Back: Those in which evaluation of any member of $\bar{e}$ would be undefined.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721497014072-->
+END%%
+
+%%ANKI
+Basic
+What assumption is made when defining assignment as "$wp(''\bar{x} \coloneqq \bar{e}'', R) = R_{\bar{e}}^{\bar{x}}$"?
+Back: $domain(\bar{e})$, i.e. evaluation of each member of $\bar{e}$ is well-defined.
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721497014076-->
+END%%
+
+%%ANKI
+Basic
+How is definition "$wp(''\bar{x} \coloneqq \bar{e}'', R) = R_{\bar{e}}^{\bar{x}}$" more completely stated?
+Back: $wp(''\bar{x} \coloneqq \bar{e}'', R) = domain(\bar{e}) \textbf{ cand } R_{\bar{e}}^{\bar{x}}$
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721497014081-->
+END%%
+
+%%ANKI
+Basic
+Given $\bar{e} = \langle e_1, \ldots, e_n \rangle$, how is $\mathop{domain}(\bar{e})$ defined in predicate logic?
+Back: $\forall i, 1 \leq i \leq n \Rightarrow \mathop{domain}(e_i)$
+Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
+<!--ID: 1721497014085-->
+END%%
 
 ## Bibliography