From 8530fbf45ba4d1ac86ebb3239c1062f34ce7a589 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sat, 20 Jul 2024 12:29:22 -0600 Subject: [PATCH] Additional notes on assignment and textual substitution. --- .../plugins/obsidian-to-anki-plugin/data.json | 6 +- notes/_journal/2024-07-20.md | 4 +- notes/logic/equiv-trans.md | 172 +++++++++++++++++- notes/programming/pred-trans.md | 115 +++++++++++- 4 files changed, 285 insertions(+), 12 deletions(-) diff --git a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json index f3fff0c..6dba2cc 100644 --- a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json +++ b/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": { diff --git a/notes/_journal/2024-07-20.md b/notes/_journal/2024-07-20.md index d9b3414..f9c93a7 100644 --- a/notes/_journal/2024-07-20.md +++ b/notes/_journal/2024-07-20.md @@ -8,4 +8,6 @@ title: "2024-07-20" - [ ] Sheet Music (10 min.) - [ ] Korean (Read 1 Story) -* Begin notes on [[hashing/index#Random Hashing|random hashing]] and, more specifically, [[hashing/index#Universal Hashing|universal hashing]]. \ No newline at end of file +* 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". \ No newline at end of file diff --git a/notes/logic/equiv-trans.md b/notes/logic/equiv-trans.md index 4a23e9e..56d61ee 100644 --- a/notes/logic/equiv-trans.md +++ b/notes/logic/equiv-trans.md @@ -591,6 +591,30 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in 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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. 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. @@ -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. END%% diff --git a/notes/programming/pred-trans.md b/notes/programming/pred-trans.md index 6a1ade0..7f3b7bc 100644 --- a/notes/programming/pred-trans.md +++ b/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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +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. + +END%% ## Bibliography