Bridge ideas on substition.
parent
016d498862
commit
216ca47217
|
|
@ -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": {
|
||||
|
|
|
|||
|
|
@ -6,4 +6,6 @@ title: "2024-05-29"
|
|||
- [x] KoL
|
||||
- [ ] Sheet Music (10 min.)
|
||||
- [ ] Go (1 Life & Death Problem)
|
||||
- [ ] Korean (Read 1 Story)
|
||||
- [ ] Korean (Read 1 Story)
|
||||
|
||||
* Flashcards on $\lambda$-calculus [[lambda-calculus#Substitution|substitution]]. Comparison to substitution as defined in Gries's equivalence-transformation system.
|
||||
|
|
@ -394,6 +394,736 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in
|
|||
<!--ID: 1707316276203-->
|
||||
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.
|
||||
<!--ID: 1707762304123-->
|
||||
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.
|
||||
<!--ID: 1707939006275-->
|
||||
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.
|
||||
<!--ID: 1707939006283-->
|
||||
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.
|
||||
<!--ID: 1707939006288-->
|
||||
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.
|
||||
<!--ID: 1707937867036-->
|
||||
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.
|
||||
<!--ID: 1707937867039-->
|
||||
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.
|
||||
<!--ID: 1707937867042-->
|
||||
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.
|
||||
<!--ID: 1708347042194-->
|
||||
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.
|
||||
<!--ID: 1708347042199-->
|
||||
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.
|
||||
<!--ID: 1708347042203-->
|
||||
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.
|
||||
<!--ID: 1707762304130-->
|
||||
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.
|
||||
<!--ID: 1707762304132-->
|
||||
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.
|
||||
<!--ID: 1707762304133-->
|
||||
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.
|
||||
<!--ID: 1707762304135-->
|
||||
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.
|
||||
<!--ID: 1707762304137-->
|
||||
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.
|
||||
<!--ID: 1707762304139-->
|
||||
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.
|
||||
<!--ID: 1707762304140-->
|
||||
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.
|
||||
<!--ID: 1707762304141-->
|
||||
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.
|
||||
<!--ID: 1707937867046-->
|
||||
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.
|
||||
<!--ID: 1707762304126-->
|
||||
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.
|
||||
<!--ID: 1707762304127-->
|
||||
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.
|
||||
<!--ID: 1707762304129-->
|
||||
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.
|
||||
<!--ID: 1713793130015-->
|
||||
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.
|
||||
<!--ID: 1713793130019-->
|
||||
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.
|
||||
<!--ID: 1713793130022-->
|
||||
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.
|
||||
<!--ID: 1713793130025-->
|
||||
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.
|
||||
<!--ID: 1713793130028-->
|
||||
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.
|
||||
<!--ID: 1713793130031-->
|
||||
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.
|
||||
<!--ID: 1713793130034-->
|
||||
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.
|
||||
<!--ID: 1713793130037-->
|
||||
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.
|
||||
<!--ID: 1713793130041-->
|
||||
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.
|
||||
<!--ID: 1713793130045-->
|
||||
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.
|
||||
<!--ID: 1713793130050-->
|
||||
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.
|
||||
<!--ID: 1713793130056-->
|
||||
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.
|
||||
<!--ID: 1713793130062-->
|
||||
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.
|
||||
<!--ID: 1713793130067-->
|
||||
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.
|
||||
<!--ID: 1713793130072-->
|
||||
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.
|
||||
<!--ID: 1713793130077-->
|
||||
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.
|
||||
<!--ID: 1713793130081-->
|
||||
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.
|
||||
<!--ID: 1713793130086-->
|
||||
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.
|
||||
<!--ID: 1713793130090-->
|
||||
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.
|
||||
<!--ID: 1713793130095-->
|
||||
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.
|
||||
<!--ID: 1713793130100-->
|
||||
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.
|
||||
<!--ID: 1713793130104-->
|
||||
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.
|
||||
<!--ID: 1713793130108-->
|
||||
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.
|
||||
<!--ID: 1714395640885-->
|
||||
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.
|
||||
<!--ID: 1714336859994-->
|
||||
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.
|
||||
<!--ID: 1714336859997-->
|
||||
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.
|
||||
<!--ID: 1714336860000-->
|
||||
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.
|
||||
<!--ID: 1714336860003-->
|
||||
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.
|
||||
<!--ID: 1714336860005-->
|
||||
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.
|
||||
<!--ID: 1714395640890-->
|
||||
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.
|
||||
<!--ID: 1714395640893-->
|
||||
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.
|
||||
<!--ID: 1714395640896-->
|
||||
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.
|
||||
<!--ID: 1714395640898-->
|
||||
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.
|
||||
<!--ID: 1714395640901-->
|
||||
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.
|
||||
<!--ID: 1714395640904-->
|
||||
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.
|
||||
<!--ID: 1714395640907-->
|
||||
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.
|
||||
<!--ID: 1714395640910-->
|
||||
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.
|
||||
<!--ID: 1714395640913-->
|
||||
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.
|
||||
<!--ID: 1714395640917-->
|
||||
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.
|
||||
<!--ID: 1714395640921-->
|
||||
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.
|
||||
<!--ID: 1714395640926-->
|
||||
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.
|
||||
<!--ID: 1714395640930-->
|
||||
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.
|
||||
<!--ID: 1714395640934-->
|
||||
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.
|
||||
<!--ID: 1714395640938-->
|
||||
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.
|
||||
<!--ID: 1714395640942-->
|
||||
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.
|
||||
<!--ID: 1714395640948-->
|
||||
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.
|
||||
<!--ID: 1714395640953-->
|
||||
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.
|
||||
<!--ID: 1707762304143-->
|
||||
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.
|
||||
<!--ID: 1707762304145-->
|
||||
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.
|
||||
<!--ID: 1707762304146-->
|
||||
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.
|
||||
<!--ID: 1707762304148-->
|
||||
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.
|
||||
<!--ID: 1707762304150-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Why should $y$ not be free in $E$ for $(E_u^x)_v^y = E_{u_v^y}^x$ to be an equivalence?
|
||||
Back: If it were, a $v$ would exist in the LHS that doesn't in the RHS.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707762304152-->
|
||||
END%%
|
||||
|
||||
%%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.
|
||||
<!--ID: 1707937867049-->
|
||||
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.
|
||||
<!--ID: 1707937867053-->
|
||||
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.
|
||||
<!--ID: 1707937867058-->
|
||||
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.
|
||||
<!--ID: 1707937867062-->
|
||||
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.
|
||||
<!--ID: 1707937867067-->
|
||||
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.
|
||||
<!--ID: 1707937867072-->
|
||||
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.
|
||||
<!--ID: 1707937867076-->
|
||||
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.
|
||||
<!--ID: 1707937867080-->
|
||||
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.
|
||||
<!--ID: 1707938187973-->
|
||||
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.
|
||||
<!--ID: 1708693353856-->
|
||||
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.
|
||||
<!--ID: 1707939006292-->
|
||||
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.
|
||||
<!--ID: 1707939315519-->
|
||||
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.
|
||||
<!--ID: 1707939006297-->
|
||||
END%%
|
||||
|
||||
## Bibliography
|
||||
|
||||
* Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
|
||||
|
|
|
|||
|
|
@ -596,6 +596,128 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi
|
|||
<!--ID: 1716745016034-->
|
||||
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).
|
||||
<!--ID: 1717036717032-->
|
||||
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).
|
||||
<!--ID: 1717036717038-->
|
||||
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).
|
||||
<!--ID: 1717036717043-->
|
||||
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).
|
||||
<!--ID: 1717036717048-->
|
||||
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).
|
||||
<!--ID: 1717036717054-->
|
||||
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).
|
||||
<!--ID: 1717035917143-->
|
||||
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).
|
||||
<!--ID: 1717036717059-->
|
||||
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).
|
||||
<!--ID: 1717036717064-->
|
||||
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).
|
||||
<!--ID: 1717036717069-->
|
||||
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).
|
||||
<!--ID: 1717036717074-->
|
||||
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).
|
||||
<!--ID: 1717036717080-->
|
||||
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).
|
||||
<!--ID: 1717036717086-->
|
||||
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).
|
||||
<!--ID: 1717036717092-->
|
||||
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).
|
||||
<!--ID: 1717036717097-->
|
||||
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).
|
||||
<!--ID: 1717036717102-->
|
||||
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).
|
||||
|
|
@ -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.
|
||||
<!--ID: 1707762304123-->
|
||||
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.
|
||||
<!--ID: 1707939006275-->
|
||||
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.
|
||||
<!--ID: 1707939006283-->
|
||||
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.
|
||||
<!--ID: 1707939006288-->
|
||||
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.
|
||||
<!--ID: 1707937867036-->
|
||||
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.
|
||||
<!--ID: 1707937867039-->
|
||||
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.
|
||||
<!--ID: 1707937867042-->
|
||||
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.
|
||||
<!--ID: 1708347042194-->
|
||||
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.
|
||||
<!--ID: 1708347042199-->
|
||||
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.
|
||||
<!--ID: 1708347042203-->
|
||||
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.
|
||||
<!--ID: 1707762304130-->
|
||||
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.
|
||||
<!--ID: 1707762304132-->
|
||||
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.
|
||||
<!--ID: 1707762304133-->
|
||||
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.
|
||||
<!--ID: 1707762304135-->
|
||||
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.
|
||||
<!--ID: 1707762304137-->
|
||||
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.
|
||||
<!--ID: 1707762304139-->
|
||||
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.
|
||||
<!--ID: 1707762304140-->
|
||||
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.
|
||||
<!--ID: 1707762304141-->
|
||||
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.
|
||||
<!--ID: 1707937867046-->
|
||||
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.
|
||||
<!--ID: 1707762304126-->
|
||||
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.
|
||||
<!--ID: 1707762304127-->
|
||||
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.
|
||||
<!--ID: 1707762304129-->
|
||||
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.
|
||||
<!--ID: 1713793130015-->
|
||||
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.
|
||||
<!--ID: 1713793130019-->
|
||||
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.
|
||||
<!--ID: 1713793130022-->
|
||||
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.
|
||||
<!--ID: 1713793130025-->
|
||||
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.
|
||||
<!--ID: 1713793130028-->
|
||||
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.
|
||||
<!--ID: 1713793130031-->
|
||||
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.
|
||||
<!--ID: 1713793130034-->
|
||||
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.
|
||||
<!--ID: 1713793130037-->
|
||||
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.
|
||||
<!--ID: 1713793130041-->
|
||||
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.
|
||||
<!--ID: 1713793130045-->
|
||||
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.
|
||||
<!--ID: 1713793130050-->
|
||||
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.
|
||||
<!--ID: 1713793130056-->
|
||||
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.
|
||||
<!--ID: 1713793130062-->
|
||||
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.
|
||||
<!--ID: 1713793130067-->
|
||||
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.
|
||||
<!--ID: 1713793130072-->
|
||||
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.
|
||||
<!--ID: 1713793130077-->
|
||||
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.
|
||||
<!--ID: 1713793130081-->
|
||||
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.
|
||||
<!--ID: 1713793130086-->
|
||||
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.
|
||||
<!--ID: 1713793130090-->
|
||||
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.
|
||||
<!--ID: 1713793130095-->
|
||||
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.
|
||||
<!--ID: 1713793130100-->
|
||||
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.
|
||||
<!--ID: 1713793130104-->
|
||||
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.
|
||||
<!--ID: 1713793130108-->
|
||||
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.
|
||||
<!--ID: 1714395640885-->
|
||||
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.
|
||||
<!--ID: 1714336859994-->
|
||||
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.
|
||||
<!--ID: 1714336859997-->
|
||||
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.
|
||||
<!--ID: 1714336860000-->
|
||||
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.
|
||||
<!--ID: 1714336860003-->
|
||||
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.
|
||||
<!--ID: 1714336860005-->
|
||||
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.
|
||||
<!--ID: 1714395640890-->
|
||||
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.
|
||||
<!--ID: 1714395640893-->
|
||||
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.
|
||||
<!--ID: 1714395640896-->
|
||||
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.
|
||||
<!--ID: 1714395640898-->
|
||||
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.
|
||||
<!--ID: 1714395640901-->
|
||||
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.
|
||||
<!--ID: 1714395640904-->
|
||||
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.
|
||||
<!--ID: 1714395640907-->
|
||||
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.
|
||||
<!--ID: 1714395640910-->
|
||||
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.
|
||||
<!--ID: 1714395640913-->
|
||||
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.
|
||||
<!--ID: 1714395640917-->
|
||||
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.
|
||||
<!--ID: 1714395640921-->
|
||||
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.
|
||||
<!--ID: 1714395640926-->
|
||||
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.
|
||||
<!--ID: 1714395640930-->
|
||||
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.
|
||||
<!--ID: 1714395640934-->
|
||||
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.
|
||||
<!--ID: 1714395640938-->
|
||||
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.
|
||||
<!--ID: 1714395640942-->
|
||||
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.
|
||||
<!--ID: 1714395640948-->
|
||||
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.
|
||||
<!--ID: 1714395640953-->
|
||||
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.
|
||||
<!--ID: 1707762304143-->
|
||||
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.
|
||||
<!--ID: 1707762304145-->
|
||||
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.
|
||||
<!--ID: 1707762304146-->
|
||||
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.
|
||||
<!--ID: 1707762304148-->
|
||||
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.
|
||||
<!--ID: 1707762304150-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Why should $y$ not be free in $E$ for $(E_u^x)_v^y = E_{u_v^y}^x$ to be an equivalence?
|
||||
Back: If it were, a $v$ would exist in the LHS that doesn't in the RHS.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707762304152-->
|
||||
END%%
|
||||
|
||||
%%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.
|
||||
<!--ID: 1707937867049-->
|
||||
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.
|
||||
<!--ID: 1707937867053-->
|
||||
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.
|
||||
<!--ID: 1707937867058-->
|
||||
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.
|
||||
<!--ID: 1707937867062-->
|
||||
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.
|
||||
<!--ID: 1707937867067-->
|
||||
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.
|
||||
<!--ID: 1707937867072-->
|
||||
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.
|
||||
<!--ID: 1707937867076-->
|
||||
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.
|
||||
<!--ID: 1707937867080-->
|
||||
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.
|
||||
<!--ID: 1707938187973-->
|
||||
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.
|
||||
<!--ID: 1708693353856-->
|
||||
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.
|
||||
<!--ID: 1707939006292-->
|
||||
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.
|
||||
<!--ID: 1707939315519-->
|
||||
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.
|
||||
<!--ID: 1707939006297-->
|
||||
END%%
|
||||
|
||||
## Bibliography
|
||||
|
||||
* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
Loading…
Reference in New Issue