diff --git a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json index dd4a2e1..5d3e676 100644 --- a/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json +++ b/notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json @@ -172,7 +172,7 @@ "_journal/2024-02-02.md": "a3b222daee8a50bce4cbac699efc7180", "_journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb", "_journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970", - "logic/equiv-trans.md": "45215c676406f1201c23e1c34c01c67f", + "logic/equiv-trans.md": "d6d9c7dacac07540ddc20608c8a805e5", "_journal/2024-02-07.md": "8d81cd56a3b33883a7706d32e77b5889", "algorithms/loop-invariants.md": "cbefc346842c21a6cce5c5edce451eb2", "algorithms/loop-invariant.md": "3b390e720f3b2a98e611b49a0bb1f5a9", @@ -466,7 +466,7 @@ "programming/λ-Calculus.md": "bf36bdaf85abffd171bb2087fb8228b2", "_journal/2024-05-23.md": "9d9106a68197adcee42cd19c69d2f840", "_journal/2024-05/2024-05-22.md": "3c29eec25f640183b0be365e7a023750", - "programming/lambda-calculus.md": "2d68babe42439dc5daa318ec3f28881f", + "programming/lambda-calculus.md": "151797fa3c012f1971d6a33eeea19274", "_journal/2024-05-25.md": "04e8e1cf4bfdbfb286effed40b09c900", "_journal/2024-05/2024-05-24.md": "86132f18c7a27ebc7a3e4a07f4867858", "_journal/2024-05/2024-05-23.md": "d0c98b484b1def3a9fd7262dcf2050ad", @@ -479,7 +479,7 @@ "git/merge-conflicts.md": "cb7d4d373639f75f6647be60f3fe97f3", "_journal/2024-05-28.md": "0f6aeb5ec126560acdc2d8c5c6570337", "_journal/2024-05/2024-05-27.md": "e498d5154558ebcf7261302403ea8016", - "_journal/2024-05-29.md": "566571bac8f4945bde6bc4483e3d6bc6", + "_journal/2024-05-29.md": "aee3f3766659789d7dfb63dd247844cc", "_journal/2024-05/2024-05-28.md": "28297d2a418f591ebc15c74fa459ddd9" }, "fields_dict": { diff --git a/notes/_journal/2024-05-29.md b/notes/_journal/2024-05-29.md index 423f40f..df8a52b 100644 --- a/notes/_journal/2024-05-29.md +++ b/notes/_journal/2024-05-29.md @@ -6,4 +6,6 @@ title: "2024-05-29" - [x] KoL - [ ] Sheet Music (10 min.) - [ ] Go (1 Life & Death Problem) -- [ ] Korean (Read 1 Story) \ No newline at end of file +- [ ] Korean (Read 1 Story) + +* Flashcards on $\lambda$-calculus [[lambda-calculus#Substitution|substitution]]. Comparison to substitution as defined in Gries's equivalence-transformation system. \ No newline at end of file diff --git a/notes/logic/equiv-trans.md b/notes/logic/equiv-trans.md index 03dcce3..cece1b3 100644 --- a/notes/logic/equiv-trans.md +++ b/notes/logic/equiv-trans.md @@ -394,6 +394,736 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in END%% +## Substitution + +**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. Let $\bar{x}$ denote a list of distinct identifiers. If $\bar{e}$ is a list of expressions of the same length as $\bar{x}$, then simultaneous substitution of $\bar{x}$ by $\bar{e}$ in expression $E$ is denoted as $$E_{\bar{e}}^{\bar{x}}$$ +Note that simultaneous substitution is different than sequential substitution. + +%%ANKI +Basic +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. + +END%% + +%%ANKI +Basic +What term refers to $x$ in textual substitution $E_e^x$? +Back: The reference. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What term refers to $e$ in textual substitution $E_e^x$? +Back: The expression. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What term refers to both $x$ and $e$ together in textual substitution $E_e^x$? +Back: The reference-expression pair. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What identifier is guaranteed to not occur freely in $E_e^x$? +Back: N/A. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What identifier is guaranteed to not occur freely in $E_{s(e)}^x$? +Back: $x$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +*Why* does $x$ not occur freely in $E_{s(e)}^x$? +Back: Because $s(e)$ evaluates to a constant proposition. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the role of $E$ in textual substitution $E_e^x$? +Back: It is the expression in which free occurrences of $x$ are replaced. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the role of $e$ in textual substitution $E_e^x$? +Back: It is the expression that is evaluated and substituted into $E$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the role of $x$ in textual substitution $E_e^x$? +Back: It is the identifier matching free occurrences in $E$ that are replaced. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +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. + +END%% + +%%ANKI +Basic +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. + +END%% + +%%ANKI +Basic +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. + +END%% + +%%ANKI +Basic +If $x \neq e$, why might $E_e^x = E$ be an equivalence despite $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. + +END%% + +%%ANKI +Basic +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. + +END%% + +%%ANKI +Basic +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. + +END%% + +%%ANKI +Basic +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. + +END%% + +%%ANKI +Basic +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. + +END%% + +%%ANKI +Basic +In textual substitution, what does e.g. $\bar{x}$ denote? +Back: A list of *distinct* identifiers. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the role of $E$ in textual substitution $E_{\bar{e}}^{\bar{x}}$? +Back: It is the expression in which free occurrences of $\bar{x}$ are replaced. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the role of $\bar{e}$ in textual substitution $E_{\bar{e}}^{\bar{x}}$? +Back: It is the expressions that are substituted into $E$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the role of $\bar{x}$ in textual substitution $E_{\bar{e}}^{\bar{x}}$? +Back: It is the distinct identifiers matching free occurrences in $E$ that are replaced. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +### Arrays + +An array can be seen as a function from the **domain** of the array to the subscripted values found in the array. We denote array subscript assignment similarly to state identifier assignment: $$(b; i{:}e)[j] = \begin{cases} i = j \rightarrow e \\ i \neq j \rightarrow b[j] \end{cases}$$ + +%%ANKI +Basic +Let $b$ be an array. What does $b.lower$ denote? +Back: The lower subscript bound of the array. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b$ be an array. What does $b.upper$ denote? +Back: The upper subscript bound of the array. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b$ be an array. How is $domain(b)$ defined in set-theoretic notation? +Back: $\{i \mid b.lower \leq i \leq b.upper\}$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b[0{:}2]$ be an array. What is $b.lower$? +Back: $0$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b[0{:}2]$ be an array. What is $b.upper$? +Back: $2$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Execution of `b[i] := e` of array $b$ yields what new value of $b$? +Back: $b = (b; i{:}e)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $s$ be a state. What *is* $x$ in $(s; x{:}e)$? +Back: An identifier found in $s$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $s$ be a state. What *is* $e$ in $(s; x{:}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 +Let $s$ be a state. What is $e$'s type in $(s; x{:}e)$? +Back: A type matching $x$'s declaration. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b$ be an array. What *is* $x$ in $(b; x{:}e)$? +Back: An expression that evaluates to a member of $domain(b)$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b$ be an array. What is $e$'s type in $(b; x{:}e)$? +Back: A type matching $b$'s member declaration. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b$ be an array. What case analysis does $(b; i{:}e)[j]$ evaluate to? +Back: $$(b; i{:}e)[j] = \begin{cases} i = j \rightarrow e \\ i \neq j \rightarrow b[j] \end{cases}$$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b$ be an array. How is $(((b; i{:}e_1); j{:}e_2); k{:}e_3)$ rewritten without nesting? +Back: As $(b; i{:}e_1; j{:}e_2; k{:}e_3)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b$ be an array. How is $(b; (i{:}e_1; (j{:}e_2; (k{:}e_3))))$ rewritten without nesting? +Back: N/A. This is invalid syntax. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b$ be an array. How is $(b; i{:}e_1; j{:}e_2; k{:}e_3)$ rewritten with nesting? +Back: As $(((b; i{:}e_1); j{:}e_2); k{:}e_3)$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b$ be an array. What does $(b; i{:}2; i{:}3; i{:}4)[i]$ evaluate to? +Back: $4$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b$ be an array. How is $(b; 0{:}8; 2{:}9; 0{:}7)[1]$ simplified? +Back: As $b[1]$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +According to Gries, what is the traditional interpretation of an array? +Back: As a collection of subscripted independent variables (with a common name). +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +According to Gries, what is the new interpretation of an array? +Back: As a function. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What expression results from eliminating $(b; \ldots)$ notation from $(b; i{:}5)[j] = 5$? +Back: $(i = j \land 5 = 5) \lor (i \neq j \land b[j] = 5)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What logical axiom is used when eliminating $(b; \ldots)$ notation from e.g. $(b; i{:}5)[j] = 5$? +Back: The Law of the Excluded Middle. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Cloze +For state $s$ and array $b$, {$(s; x{:}s(x))$} is analagous to {$(b; i{:}b[i])$}. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What is the simplification of $(b; i{:}b[i]; j{:}b[j]; k{:}b[j])$? +Back: $(b; k{:}b[j])$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given array $b$, what terminology does Gries use to describe $i{:}j$ in e.g. $b[i{:}j]$? +Back: A section. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given array $b$, how many elements are in section $b[i{:}j]$? +Back: $j - i + 1$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given array $b$ and fixed $j$, what is the largest possible value of $i$ in $b[i{:}j]$? +Back: $j + 1$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given array $b$, how many elements are in $b[j{+}1{:}j]$? +Back: $0$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given array $b$, what is $b[1{:}5] = x$ an abbreviation for? +Back: $\forall i, 1 \leq i \leq 5 \Rightarrow b[i] = x$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given array $b$, what is $b[1{:}k{-}1] < x < b[k{:}n{-}1]$ an abbreviation for? +Back: $(\forall i, 1 \leq i < k \Rightarrow b[i] < x) \land (\forall i, k \leq i < n \Rightarrow x < b[i])$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +### Selector Update Syntax + +A **selector** denotes a finite sequence of subscript expressions, each enclosed in brackets. $\epsilon$ denotes the empty selector. We can generalize the above to all variable types as follows: $$\begin{align*} (b; \epsilon{:}g) & = g \\ (b; [i] \circ s{:}e)[j] & = \begin{cases} i \neq j \rightarrow b[j] \\ i = j \rightarrow (b[j]; s{:}e) \end{cases} \end{align*}$$ + +%%ANKI +Basic +What is a selector? +Back: A finite sequence of subscript expressions. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given valid expression $(b; [i]{\circ}s{:}e)$, what can be said about $i$? +Back: $i$ is in the domain of $b$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given valid expression $(b; [i]{\circ}s{:}e)$, what is the type of $b$? +Back: A function (an array). +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given valid expression $(b; \epsilon{:}e)$, what is the type of $b$? +Back: A function or scalar. +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 of selector update syntax? +Back: $(b; \epsilon{:}g) = g$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +The null selector is usually denoted as what? +Back: $\epsilon$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +The null selector is the identity element of what operation? +Back: Concatenation of sequences of subscripts. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is assignment $x := e$ rewritten with a selector? +Back: $x \circ \epsilon := e$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is $x \circ \epsilon := e$ rewritten using selector update syntax? +Back: $x := (x; \epsilon{:}e)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What assignment expression (i.e. using `:=`) is simpler but equivalent to $x := (x; \epsilon{:}e)$? +Back: $x := e$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What two assignments (i.e. using `:=`) are used to prove $e = (x; \epsilon{:}e)$? +Back: $x := e$ and $x \circ \epsilon := e$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How do assignments $x := e$ and $x \circ \epsilon := e$ prove $e = (x; \epsilon{:}e)$? +Back: The assignments have the same effect and the latter can be written as $x := (x; \epsilon{:}e)$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b$ be an array. How is $b[i][j] := e$ rewritten using selector update syntax? +Back: $b := (b; [i][j]{:}e)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b$ be an array. What does $(b; \epsilon{:}g)$ evaluate to? +Back: $g$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b$ be an array and $i = j$. What does $(b; [i]{\circ}s{:}e)[j]$ evaluate to? +Back: $(b[j]; s{:}e)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Let $b$ be an array and $i \neq j$. What does $(b; [i]{\circ}s{:}e)[j]$ evaluate to? +Back: $b[j]$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Maintaining selector update syntax, how is $(c; 1{:}3)[1]$ more explicitly written with a selector? +Back: $(c; [1]{:}3)[1]$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Maintaining selector update syntax, how is $(c; 1{:}3)[1]$ rewritten with $[1]$ commuted as leftward as possible? +Back: $(c[1]; \epsilon{:}3)$ +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$. + +%%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. + +END%% + +%%ANKI +Basic +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. + +END%% + +%%ANKI +Basic +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$. + * $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 +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. + +END%% + +%%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. + +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. + +END%% + +%%ANKI +Basic +How does Gries denote state $s$ with identifer $x$ set to value $v$? +Back: $(s; x{:}v)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How is $(s; x{:}v)$ written instead using set-theoretical notation? +Back: $(s - \{\langle x, s(x) \rangle\}) \cup \{\langle x, v \rangle\}$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Execution of `x := e` in state $s$ terminates in what new state? +Back: $(s; x{:}s(e))$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given state $s$, what statement does $(s; x{:}s(e))$ derive from? +Back: `x := e` +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +What missing value guarantees state $s$ satisfies equivalence $s = (s; x{:}\_)$? +Back: $s(x)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given state $s$, why is it that $s = (s; x{:}s(x))$? +Back: Evaluating $x$ in state $s$ yields $s(x)$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +* $s(E_e^x) = s(E_{s(e)}^x)$ + * Substituting $x$ with $e$ and then evaluating is the same as substituting $x$ with the evaluation of $e$. + +%%ANKI +Basic +How can we simplify $s(E_{s(e)}^x)$? +Back: As $s(E_e^x)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given state $s$, what equivalence relates $E_e^x$ with $E_{s(e)}^x$? +Back: $s(E_e^x) = s(E_{s(e)}^x)$ +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +* Let $s$ be a state and $s' = (s; x{:}s(e))$. Then $s'(E) = s(E_e^x)$. + +%%ANKI +Cloze +Let $s$ be a state and $s' = (${$s; x{:}s(e)$}$)$. Then $s'(${$E$}$) = s(${$E_e^x$}$)$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +If $s' = (s; x{:}s(e))$, then $s'(E) = s(E_e^x)$. Why do we not say $s' = (s; x{:}e)$ instead? +Back: The value of a state's identifier must always be a constant proposition. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +How do you define $s'$ such that $s(E_e^x) = s'(E)$? +Back: $s' = (s; x{:}s(e))$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +%%ANKI +Basic +Given defined value $v \neq s(x)$, when is $s(E) = (s; x{:}v)(E)$? +Back: When $x$ is not free in $E$. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + +* Given identifiers $\bar{x}$ and fresh identifiers $\bar{u}$, $(E_{\bar{u}}^{\bar{x}})_{\bar{x}}^{\bar{u}} = E$. + +%%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}$ are all distinct identifiers. +Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. + +END%% + ## Bibliography * Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. diff --git a/notes/programming/lambda-calculus.md b/notes/programming/lambda-calculus.md index 03f6470..16c05e7 100644 --- a/notes/programming/lambda-calculus.md +++ b/notes/programming/lambda-calculus.md @@ -596,6 +596,128 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi END%% +## Substitution + +For any $M$, $N$, and $x$, define $[N/x]M$ to be the result of substituting $N$ for every free occurrence of $x$ in $M$, and changing bound variables to avoid clashes. + +%%ANKI +Basic +How is $E_e^x$ equivalently written in $\lambda$-calculus? +Back: $[e/x]E$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +How is $[N/x]M$ equivalently written in equivalence transformation? +Back: $M_N^x$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +How does substitution, say $[N/x]M$, affect free variables? +Back: Every free occurrence of $x$ is substituted with $N$. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +How does substitution, say $[N/x]M$, affect bound variables? +Back: Bound variables are renamed to avoid name clashes. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Cloze +$[N/x]M$ is the result of substituting {$N$} for every free occurrence of {$x$} in {$M$}. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Cloze +{$M^x_e$} is to equivalence transformation whereas {$[e/x]M$} is to $\lambda$-calculus. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +What is the result of $[N/x]x$? +Back: $N$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +What is the result of $[N/x]a$, for some atom $a \neq x$? +Back: $a$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +What is the result of $[N/x]a$, for some atom $a = x$? +Back: $N$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +What is the result of $[N/x](PQ)$? +Back: $([N/x]P)([N/x]Q)$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +What is the result of $[N/x](\lambda x. P)$? +Back: $\lambda x. P$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +If $x \in FV(P)$ and $y \in FV(N)$, what is the result of $[N/x](\lambda y. P)$? +Back: $\lambda z. [N/x][z/y]P$ where $z \not\in FV(NP)$. +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +If $x \not\in FV(P)$ and $y \in FV(N)$, what is the result of $[N/x](\lambda y. P)$? +Back: $\lambda y. P$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +If $x \in FV(P)$ and $y \not\in FV(N)$, what is the result of $[N/x](\lambda y. P)$? +Back: $\lambda y. [N/x]P$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + +%%ANKI +Basic +If $x \not\in FV(P)$ and $y \not\in FV(N)$, what is the result of $[N/x](\lambda y. P)$? +Back: $\lambda y. P$ +Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). + +END%% + ## Bibliography * Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). \ No newline at end of file diff --git a/notes/programming/text-sub.md b/notes/programming/text-sub.md deleted file mode 100644 index 3ead3ad..0000000 --- a/notes/programming/text-sub.md +++ /dev/null @@ -1,741 +0,0 @@ ---- -title: Textual Substitution -TARGET DECK: Obsidian::STEM -FILE TAGS: programming::text-sub -tags: - - programming - - text-sub ---- -## Overview - -**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. Let $\bar{x}$ denote a list of distinct identifiers. If $\bar{e}$ is a list of expressions of the same length as $\bar{x}$, then simultaneous substitution of $\bar{x}$ by $\bar{e}$ in expression $E$ is denoted as $$E_{\bar{e}}^{\bar{x}}$$ -Note that simultaneous substitution is different than sequential substitution. - -%%ANKI -Basic -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. - -END%% - -%%ANKI -Basic -What term refers to $x$ in textual substitution $E_e^x$? -Back: The reference. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What term refers to $e$ in textual substitution $E_e^x$? -Back: The expression. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What term refers to both $x$ and $e$ together in textual substitution $E_e^x$? -Back: The reference-expression pair. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What identifier is guaranteed to not occur freely in $E_e^x$? -Back: N/A. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What identifier is guaranteed to not occur freely in $E_{s(e)}^x$? -Back: $x$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -*Why* does $x$ not occur freely in $E_{s(e)}^x$? -Back: Because $s(e)$ evaluates to a constant proposition. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the role of $E$ in textual substitution $E_e^x$? -Back: It is the expression in which free occurrences of $x$ are replaced. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the role of $e$ in textual substitution $E_e^x$? -Back: It is the expression that is evaluated and substituted into $E$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the role of $x$ in textual substitution $E_e^x$? -Back: It is the identifier matching free occurrences in $E$ that are replaced. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -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. - -END%% - -%%ANKI -Basic -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. - -END%% - -%%ANKI -Basic -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. - -END%% - -%%ANKI -Basic -If $x \neq e$, why might $E_e^x = E$ be an equivalence despite $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. - -END%% - -%%ANKI -Basic -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. - -END%% - -%%ANKI -Basic -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. - -END%% - -%%ANKI -Basic -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. - -END%% - -%%ANKI -Basic -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. - -END%% - -%%ANKI -Basic -In textual substitution, what does e.g. $\bar{x}$ denote? -Back: A list of *distinct* identifiers. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the role of $E$ in textual substitution $E_{\bar{e}}^{\bar{x}}$? -Back: It is the expression in which free occurrences of $\bar{x}$ are replaced. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the role of $\bar{e}$ in textual substitution $E_{\bar{e}}^{\bar{x}}$? -Back: It is the expressions that are substituted into $E$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the role of $\bar{x}$ in textual substitution $E_{\bar{e}}^{\bar{x}}$? -Back: It is the distinct identifiers matching free occurrences in $E$ that are replaced. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -### Arrays - -An array can be seen as a function from the **domain** of the array to the subscripted values found in the array. We denote array subscript assignment similarly to state identifier assignment: $$(b; i{:}e)[j] = \begin{cases} i = j \rightarrow e \\ i \neq j \rightarrow b[j] \end{cases}$$ - -%%ANKI -Basic -Let $b$ be an array. What does $b.lower$ denote? -Back: The lower subscript bound of the array. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Let $b$ be an array. What does $b.upper$ denote? -Back: The upper subscript bound of the array. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Let $b$ be an array. How is $domain(b)$ defined in set-theoretic notation? -Back: $\{i \mid b.lower \leq i \leq b.upper\}$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Let $b[0{:}2]$ be an array. What is $b.lower$? -Back: $0$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Let $b[0{:}2]$ be an array. What is $b.upper$? -Back: $2$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Execution of `b[i] := e` of array $b$ yields what new value of $b$? -Back: $b = (b; i{:}e)$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Let $s$ be a state. What *is* $x$ in $(s; x{:}e)$? -Back: An identifier found in $s$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Let $s$ be a state. What *is* $e$ in $(s; x{:}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 -Let $s$ be a state. What is $e$'s type in $(s; x{:}e)$? -Back: A type matching $x$'s declaration. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Let $b$ be an array. What *is* $x$ in $(b; x{:}e)$? -Back: An expression that evaluates to a member of $domain(b)$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Let $b$ be an array. What is $e$'s type in $(b; x{:}e)$? -Back: A type matching $b$'s member declaration. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Let $b$ be an array. What case analysis does $(b; i{:}e)[j]$ evaluate to? -Back: $$(b; i{:}e)[j] = \begin{cases} i = j \rightarrow e \\ i \neq j \rightarrow b[j] \end{cases}$$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Let $b$ be an array. How is $(((b; i{:}e_1); j{:}e_2); k{:}e_3)$ rewritten without nesting? -Back: As $(b; i{:}e_1; j{:}e_2; k{:}e_3)$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Let $b$ be an array. How is $(b; (i{:}e_1; (j{:}e_2; (k{:}e_3))))$ rewritten without nesting? -Back: N/A. This is invalid syntax. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Let $b$ be an array. How is $(b; i{:}e_1; j{:}e_2; k{:}e_3)$ rewritten with nesting? -Back: As $(((b; i{:}e_1); j{:}e_2); k{:}e_3)$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Let $b$ be an array. What does $(b; i{:}2; i{:}3; i{:}4)[i]$ evaluate to? -Back: $4$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Let $b$ be an array. How is $(b; 0{:}8; 2{:}9; 0{:}7)[1]$ simplified? -Back: As $b[1]$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -According to Gries, what is the traditional interpretation of an array? -Back: As a collection of subscripted independent variables (with a common name). -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -According to Gries, what is the new interpretation of an array? -Back: As a function. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What expression results from eliminating $(b; \ldots)$ notation from $(b; i{:}5)[j] = 5$? -Back: $(i = j \land 5 = 5) \lor (i \neq j \land b[j] = 5)$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What logical axiom is used when eliminating $(b; \ldots)$ notation from e.g. $(b; i{:}5)[j] = 5$? -Back: The Law of the Excluded Middle. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Cloze -For state $s$ and array $b$, {$(s; x{:}s(x))$} is analagous to {$(b; i{:}b[i])$}. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What is the simplification of $(b; i{:}b[i]; j{:}b[j]; k{:}b[j])$? -Back: $(b; k{:}b[j])$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Given array $b$, what terminology does Gries use to describe $i{:}j$ in e.g. $b[i{:}j]$? -Back: A section. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Given array $b$, how many elements are in section $b[i{:}j]$? -Back: $j - i + 1$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Given array $b$ and fixed $j$, what is the largest possible value of $i$ in $b[i{:}j]$? -Back: $j + 1$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Given array $b$, how many elements are in $b[j{+}1{:}j]$? -Back: $0$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Given array $b$, what is $b[1{:}5] = x$ an abbreviation for? -Back: $\forall i, 1 \leq i \leq 5 \Rightarrow b[i] = x$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Given array $b$, what is $b[1{:}k{-}1] < x < b[k{:}n{-}1]$ an abbreviation for? -Back: $(\forall i, 1 \leq i < k \Rightarrow b[i] < x) \land (\forall i, k \leq i < n \Rightarrow x < b[i])$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -### Selector Update Syntax - -A **selector** denotes a finite sequence of subscript expressions, each enclosed in brackets. $\epsilon$ denotes the empty selector. We can generalize the above to all variable types as follows: $$\begin{align*} (b; \epsilon{:}g) & = g \\ (b; [i] \circ s{:}e)[j] & = \begin{cases} i \neq j \rightarrow b[j] \\ i = j \rightarrow (b[j]; s{:}e) \end{cases} \end{align*}$$ - -%%ANKI -Basic -What is a selector? -Back: A finite sequence of subscript expressions. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Given valid expression $(b; [i]{\circ}s{:}e)$, what can be said about $i$? -Back: $i$ is in the domain of $b$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Given valid expression $(b; [i]{\circ}s{:}e)$, what is the type of $b$? -Back: A function (an array). -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Given valid expression $(b; \epsilon{:}e)$, what is the type of $b$? -Back: A function or scalar. -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 of selector update syntax? -Back: $(b; \epsilon{:}g) = g$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -The null selector is usually denoted as what? -Back: $\epsilon$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -The null selector is the identity element of what operation? -Back: Concatenation of sequences of subscripts. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -How is assignment $x := e$ rewritten with a selector? -Back: $x \circ \epsilon := e$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -How is $x \circ \epsilon := e$ rewritten using selector update syntax? -Back: $x := (x; \epsilon{:}e)$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What assignment expression (i.e. using `:=`) is simpler but equivalent to $x := (x; \epsilon{:}e)$? -Back: $x := e$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What two assignments (i.e. using `:=`) are used to prove $e = (x; \epsilon{:}e)$? -Back: $x := e$ and $x \circ \epsilon := e$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -How do assignments $x := e$ and $x \circ \epsilon := e$ prove $e = (x; \epsilon{:}e)$? -Back: The assignments have the same effect and the latter can be written as $x := (x; \epsilon{:}e)$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Let $b$ be an array. How is $b[i][j] := e$ rewritten using selector update syntax? -Back: $b := (b; [i][j]{:}e)$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Let $b$ be an array. What does $(b; \epsilon{:}g)$ evaluate to? -Back: $g$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Let $b$ be an array and $i = j$. What does $(b; [i]{\circ}s{:}e)[j]$ evaluate to? -Back: $(b[j]; s{:}e)$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Let $b$ be an array and $i \neq j$. What does $(b; [i]{\circ}s{:}e)[j]$ evaluate to? -Back: $b[j]$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Maintaining selector update syntax, how is $(c; 1{:}3)[1]$ more explicitly written with a selector? -Back: $(c; [1]{:}3)[1]$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Maintaining selector update syntax, how is $(c; 1{:}3)[1]$ rewritten with $[1]$ commuted as leftward as possible? -Back: $(c[1]; \epsilon{:}3)$ -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$. - -%%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. - -END%% - -%%ANKI -Basic -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. - -END%% - -%%ANKI -Basic -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$. - * $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 -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. - -END%% - -%%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. - -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. - -END%% - -%%ANKI -Basic -How does Gries denote state $s$ with identifer $x$ set to value $v$? -Back: $(s; x{:}v)$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -How is $(s; x{:}v)$ written instead using set-theoretical notation? -Back: $(s - \{\langle x, s(x) \rangle\}) \cup \{\langle x, v \rangle\}$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Execution of `x := e` in state $s$ terminates in what new state? -Back: $(s; x{:}s(e))$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Given state $s$, what statement does $(s; x{:}s(e))$ derive from? -Back: `x := e` -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -What missing value guarantees state $s$ satisfies equivalence $s = (s; x{:}\_)$? -Back: $s(x)$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Given state $s$, why is it that $s = (s; x{:}s(x))$? -Back: Evaluating $x$ in state $s$ yields $s(x)$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -* $s(E_e^x) = s(E_{s(e)}^x)$ - * Substituting $x$ with $e$ and then evaluating is the same as substituting $x$ with the evaluation of $e$. - -%%ANKI -Basic -How can we simplify $s(E_{s(e)}^x)$? -Back: As $s(E_e^x)$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Given state $s$, what equivalence relates $E_e^x$ with $E_{s(e)}^x$? -Back: $s(E_e^x) = s(E_{s(e)}^x)$ -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -* Let $s$ be a state and $s' = (s; x{:}s(e))$. Then $s'(E) = s(E_e^x)$. - -%%ANKI -Cloze -Let $s$ be a state and $s' = (${$s; x{:}s(e)$}$)$. Then $s'(${$E$}$) = s(${$E_e^x$}$)$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -If $s' = (s; x{:}s(e))$, then $s'(E) = s(E_e^x)$. Why do we not say $s' = (s; x{:}e)$ instead? -Back: The value of a state's identifier must always be a constant proposition. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -How do you define $s'$ such that $s(E_e^x) = s'(E)$? -Back: $s' = (s; x{:}s(e))$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -%%ANKI -Basic -Given defined value $v \neq s(x)$, when is $s(E) = (s; x{:}v)(E)$? -Back: When $x$ is not free in $E$. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -* Given identifiers $\bar{x}$ and fresh identifiers $\bar{u}$, $(E_{\bar{u}}^{\bar{x}})_{\bar{x}}^{\bar{u}} = E$. - -%%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}$ are all distinct identifiers. -Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. - -END%% - -## Bibliography - -* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. \ No newline at end of file