Additional notes on binary shifting.

c-declarations
Joshua Potter 2024-02-15 16:23:53 -07:00
parent 448bf65909
commit 30c6fb97b5
9 changed files with 257 additions and 82 deletions

View File

@ -80,7 +80,7 @@
"File Hashes": { "File Hashes": {
"algorithms/index.md": "a5ff7313f71777f1f3536e27dd9894fa", "algorithms/index.md": "a5ff7313f71777f1f3536e27dd9894fa",
"algorithms/sorting/index.md": "2d5a18a3079d96fa9e3d4289181a8b6c", "algorithms/sorting/index.md": "2d5a18a3079d96fa9e3d4289181a8b6c",
"algorithms/sorting/insertion-sort.md": "d40da14992d8331a07cebe1c4cfa41d4", "algorithms/sorting/insertion-sort.md": "00e4edb132d473b0516fde3307ebae30",
"bash/index.md": "3dfeb538d781e4645e3aaaf32beb1034", "bash/index.md": "3dfeb538d781e4645e3aaaf32beb1034",
"bash/prompts.md": "61cb877e68da040a15b85af76b1f68ba", "bash/prompts.md": "61cb877e68da040a15b85af76b1f68ba",
"bash/quoting.md": "b1d8869a91001f8b22f0cdc54d806f61", "bash/quoting.md": "b1d8869a91001f8b22f0cdc54d806f61",
@ -89,7 +89,7 @@
"c/escape-sequences.md": "0d6219ebb51f6f21e026de67603e25b8", "c/escape-sequences.md": "0d6219ebb51f6f21e026de67603e25b8",
"c/index.md": "a021c92f19831bdd2bca4cbf813882fe", "c/index.md": "a021c92f19831bdd2bca4cbf813882fe",
"gawk/index.md": "dd851e023e11c556c0272a0dcb6dd55d", "gawk/index.md": "dd851e023e11c556c0272a0dcb6dd55d",
"gawk/variables.md": "a9cd0344390974b3bfdf794d75d434e5", "gawk/variables.md": "a7d95bd458e07b5a329c62366f368c8d",
"index.md": "e48e895feeed7046425bb2ee15419770", "index.md": "e48e895feeed7046425bb2ee15419770",
"journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970", "journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970",
"journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb", "journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb",
@ -114,14 +114,14 @@
"_journal/2024-02-02.md": "a3b222daee8a50bce4cbac699efc7180", "_journal/2024-02-02.md": "a3b222daee8a50bce4cbac699efc7180",
"_journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb", "_journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb",
"_journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970", "_journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970",
"logic/equiv-trans.md": "ba87bed095b095540393db90ad350da0", "logic/equiv-trans.md": "3385a3cf9ba8b0cebbc1bdff3f994751",
"_journal/2024-02-07.md": "8d81cd56a3b33883a7706d32e77b5889", "_journal/2024-02-07.md": "8d81cd56a3b33883a7706d32e77b5889",
"algorithms/loop-invariants.md": "cbefc346842c21a6cce5c5edce451eb2", "algorithms/loop-invariants.md": "cbefc346842c21a6cce5c5edce451eb2",
"algorithms/loop-invariant.md": "d883dfc997ee28a7a1e24b995377792b", "algorithms/loop-invariant.md": "d883dfc997ee28a7a1e24b995377792b",
"algorithms/running-time.md": "5efc0791097d2c996f931c9046c95f65", "algorithms/running-time.md": "5efc0791097d2c996f931c9046c95f65",
"algorithms/order-growth.md": "5fb2e3ccfc3710be7396a37da7c4f162", "algorithms/order-growth.md": "5fb2e3ccfc3710be7396a37da7c4f162",
"_journal/2024-02-08.md": "19092bdfe378f31e2774f20d6afbfbac", "_journal/2024-02-08.md": "19092bdfe378f31e2774f20d6afbfbac",
"algorithms/sorting/selection-sort.md": "73a077a726afd376650d1bd9e2d0bed9", "algorithms/sorting/selection-sort.md": "fcd0dc2ebaabd0a4db1baf7e7ef9f7a9",
"algorithms/index 1.md": "6fada1f3d5d3af64687719eb465a5b97", "algorithms/index 1.md": "6fada1f3d5d3af64687719eb465a5b97",
"binary/hexadecimal.md": "c3d485f1fd869fe600334ecbef7d5d70", "binary/hexadecimal.md": "c3d485f1fd869fe600334ecbef7d5d70",
"binary/index.md": "27bdd4423e323cd961ddb307ab28d977", "binary/index.md": "27bdd4423e323cd961ddb307ab28d977",
@ -152,12 +152,14 @@
"c/strings.md": "e08be6bdc820ec4903480a736448a5d7", "c/strings.md": "e08be6bdc820ec4903480a736448a5d7",
"logic/truth-tables.md": "7892ceaa416c9a65acc79ca1e6ff778f", "logic/truth-tables.md": "7892ceaa416c9a65acc79ca1e6ff778f",
"logic/short-circuit.md": "26d300f407f14883022d0ef8dc4f7300", "logic/short-circuit.md": "26d300f407f14883022d0ef8dc4f7300",
"logic/boolean-algebra.md": "c5d699d407e03d280aa1f201bc3e8b02", "logic/boolean-algebra.md": "370065481448e60aa8ffa67a437b5482",
"_journal/2024-02-13.md": "6242ed4fecabf95df6b45d892fee8eb0", "_journal/2024-02-13.md": "6242ed4fecabf95df6b45d892fee8eb0",
"_journal/2024-02/2024-02-12.md": "618c0035a69b48227119379236a02f44", "_journal/2024-02/2024-02-12.md": "618c0035a69b48227119379236a02f44",
"binary/shifts.md": "24a1f56268fdbae4fe22e92c18366abc", "binary/shifts.md": "4c8fccaa2a5a38041b8708ace97319df",
"_journal/2024-02-14.md": "22dbfc7f440d63a3c5685a3d32ab9c72", "_journal/2024-02-14.md": "76d1b607470305fb3f00a47b8e9ece27",
"_journal/2024-02/2024-02-13.md": "6242ed4fecabf95df6b45d892fee8eb0" "_journal/2024-02/2024-02-13.md": "6242ed4fecabf95df6b45d892fee8eb0",
"_journal/2024-02-15.md": "575ba46d692795d9606de9e635d1f4ac",
"_journal/2024-02/2024-02-14.md": "aa009f9569e175a8104b0537ebcc5520"
}, },
"fields_dict": { "fields_dict": {
"Basic": [ "Basic": [

View File

@ -0,0 +1,15 @@
---
title: "2024-02-15"
---
- [x] Anki Flashcards
- [x] KoL
- [ ] Sheet Music (10 min.)
- [ ] OGS (1 Life & Death Problem)
- [ ] Korean (Read 1 Story)
- [ ] Interview Prep (1 Practice Problem)
- [ ] Log Work Hours (Max 3 hours)
* Finished "Ingestion" chapter of "Fundamentals of Data Engineering".
* Read first chapter of "Concrete Mathematics" and added additional notes on bit shifting.
* Met with Gus on Soft Skills workshop.

View File

@ -7,9 +7,10 @@ title: "2024-02-14"
- [ ] Sheet Music (10 min.) - [ ] Sheet Music (10 min.)
- [ ] OGS (1 Life & Death Problem) - [ ] OGS (1 Life & Death Problem)
- [x] Korean (Read 1 Story) - [x] Korean (Read 1 Story)
- [ ] Interview Prep (1 Practice Problem) - [x] Interview Prep (1 Practice Problem)
- [x] Log Work Hours (Max 3 hours) - [x] Log Work Hours (Max 3 hours)
* More flashcards on `printf`. This time on flags. * More flashcards on `printf`. This time on flags.
* Read 금덩이를 버린 형제 (Two brothers Who Threw Away Their Lumps of Gold). * Read 금덩이를 버린 형제 (Two brothers Who Threw Away Their Lumps of Gold).
* Flashcards are growing much more rapidly with my Obsidian_to_Anki plugin approach. Increased new card limit to 40 and will evaluate how well that works. * Flashcards are growing much more rapidly with my Obsidian_to_Anki plugin approach. Increased new card limit to 40 and will evaluate how well that works.
* Notes on textual substitution.

View File

@ -153,10 +153,10 @@ Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambri
END%% END%%
%%ANKI %%ANKI
Basic Cloze
insertion sort makes fewer {comparisons} than selection sort in the average case. insertion sort makes fewer {comparisons} than selection sort in the average case.
Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009).
<!--ID: 1707500283783--> <!--ID: 1708002185982-->
END%% END%%
## Analogy ## Analogy

View File

@ -171,7 +171,7 @@ END%%
Cloze Cloze
Selection sort makes fewer {swaps} than insertion sort in the average case. Selection sort makes fewer {swaps} than insertion sort in the average case.
Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009). Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009).
<!--ID: 1707500283779--> <!--ID: 1708002177782-->
END%% END%%
## References ## References

View File

@ -150,7 +150,7 @@ END%%
%%ANKI %%ANKI
Cloze Cloze
{Arithmetic} right shifts are to {signed} numbers whereas {logical} right shifts are to {unsigned} numbers. {1:Arithmetic} right shifts are to {1:signed} numbers whereas {2:logical} right shifts are to {2:unsigned} numbers.
Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
Tags: c Tags: c
<!--ID: 1707854589813--> <!--ID: 1707854589813-->
@ -194,6 +194,102 @@ Tags: c
<!--ID: 1707873410780--> <!--ID: 1707873410780-->
END%% END%%
## Arithmetic
Shifting left by a single bit is equivalent to multiplication by $2$. Likewise, logically shifting right is equivalent to floor division by $2$. This is most clearly seen by examining the decimal expansion of a binary value. For example, consider $$001101_2 = 2^3 + 2^2 + 2^0$$
Multiplying by $2$ yields $$2 \cdot (2^3 + 2^2 + 2^0) = 2^4 + 2^3 + 2^1 = 011010_2$$
Dividing by $2$ yields $$(2^3 + 2^2 + 2^0) / 2 = 2^2 + 2^1 = 000110_2$$
%%ANKI
Basic
Multiplication by 2 is equivalent to what bitwise shift operation?
Back: Left shifting by 1 bit.
Reference: Ronald L. Graham, Donald Ervin Knuth, and Oren Patashnik, *Concrete Mathematics: A Foundation for Computer Science*, 2nd ed (Reading, Mass: Addison-Wesley, 1994).
<!--ID: 1708009783552-->
END%%
%%ANKI
Basic
Floor division by 2 is equivalent to what bitwise shift operation?
Back: Logical right shifting by 1 bit.
Reference: Ronald L. Graham, Donald Ervin Knuth, and Oren Patashnik, *Concrete Mathematics: A Foundation for Computer Science*, 2nd ed (Reading, Mass: Addison-Wesley, 1994).
<!--ID: 1708009783562-->
END%%
%%ANKI
Basic
Ceiling division by 2 is equivalent to what bitwise shift operation?
Back: None.
Reference: Ronald L. Graham, Donald Ervin Knuth, and Oren Patashnik, *Concrete Mathematics: A Foundation for Computer Science*, 2nd ed (Reading, Mass: Addison-Wesley, 1994).
<!--ID: 1708009783565-->
END%%
%%ANKI
Cloze
{1:Multiplication} by 2 is to {2:left shifts} whereas {2:floor division} by 2 is to {1:logical right shifts}.
Reference: Ronald L. Graham, Donald Ervin Knuth, and Oren Patashnik, *Concrete Mathematics: A Foundation for Computer Science*, 2nd ed (Reading, Mass: Addison-Wesley, 1994).
<!--ID: 1708009783568-->
END%%
%%ANKI
Basic
What arithmetic operation is equivalent to shifting left by $n$ bits?
Back: Multiplication by $2^n$.
Reference: Ronald L. Graham, Donald Ervin Knuth, and Oren Patashnik, *Concrete Mathematics: A Foundation for Computer Science*, 2nd ed (Reading, Mass: Addison-Wesley, 1994).
<!--ID: 1708009783571-->
END%%
%%ANKI
Basic
When is $2n + 1$ equivalent to a one-bit cyclic shift left?
Back: When $n$'s leading bit is `1`.
Reference: Ronald L. Graham, Donald Ervin Knuth, and Oren Patashnik, *Concrete Mathematics: A Foundation for Computer Science*, 2nd ed (Reading, Mass: Addison-Wesley, 1994).
<!--ID: 1708012138055-->
END%%
%%ANKI
Basic
What arithmetic operation is equivalent to a one-bit cyclic shift left?
Back: Given $n$ with no leading zeros, $2n + 1$.
Reference: Ronald L. Graham, Donald Ervin Knuth, and Oren Patashnik, *Concrete Mathematics: A Foundation for Computer Science*, 2nd ed (Reading, Mass: Addison-Wesley, 1994).
<!--ID: 1708012138062-->
END%%
%%ANKI
Basic
What arithmetic operation is equivalent to logically shifting right by $n$ bits?
Back: Floor division by $2^n$.
Reference: Ronald L. Graham, Donald Ervin Knuth, and Oren Patashnik, *Concrete Mathematics: A Foundation for Computer Science*, 2nd ed (Reading, Mass: Addison-Wesley, 1994).
<!--ID: 1708009783574-->
END%%
%%ANKI
Basic
Given $n = 0110_2$, what is the binary value of $2n$?
Back: $1100_2$
Reference: Ronald L. Graham, Donald Ervin Knuth, and Oren Patashnik, *Concrete Mathematics: A Foundation for Computer Science*, 2nd ed (Reading, Mass: Addison-Wesley, 1994).
<!--ID: 1708012138065-->
END%%
%%ANKI
Basic
Given $n = 0110_2$, what is the binary value of $2n + 1$?
Back: $1101_2$
Reference: Ronald L. Graham, Donald Ervin Knuth, and Oren Patashnik, *Concrete Mathematics: A Foundation for Computer Science*, 2nd ed (Reading, Mass: Addison-Wesley, 1994).
<!--ID: 1708012138068-->
END%%
%%ANKI
Basic
Given $n = 0110_2$, what is the binary value of $\lfloor n / 2 \rfloor$?
Back: $0011_2$
Reference: Ronald L. Graham, Donald Ervin Knuth, and Oren Patashnik, *Concrete Mathematics: A Foundation for Computer Science*, 2nd ed (Reading, Mass: Addison-Wesley, 1994).
<!--ID: 1708012138071-->
END%%
## References ## References
* Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016. * Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
* Ronald L. Graham, Donald Ervin Knuth, and Oren Patashnik, *Concrete Mathematics: A Foundation for Computer Science*, 2nd ed (Reading, Mass: Addison-Wesley, 1994).

View File

@ -192,7 +192,7 @@ END%%
%%ANKI %%ANKI
Basic Basic
What value is `${NF + 1}` given when we run `${NF + 2} = "test"`? What value is `$${NF + 1}` given when we run `${NF + 2} = "test"`?
Back: `""` Back: `""`
Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf) Reference: Robbins, Arnold D. “GAWK: Effective AWK Programming,” October 2023. [https://www.gnu.org/software/gawk/manual/gawk.pdf](https://www.gnu.org/software/gawk/manual/gawk.pdf)
<!--ID: 1707491299854--> <!--ID: 1707491299854-->

View File

@ -11,6 +11,67 @@ tags:
**Boolean algebra** refers to an algebraic system characterised by a set of axioms. This is something I'll explore further, probably after reading more on abstract algebra. The basic operations of Boolean algebra are negation ($\neg$), conjunction ($\land$), and disjunction ($\lor$). **Boolean algebra** refers to an algebraic system characterised by a set of axioms. This is something I'll explore further, probably after reading more on abstract algebra. The basic operations of Boolean algebra are negation ($\neg$), conjunction ($\land$), and disjunction ($\lor$).
%%ANKI
Basic
What name is given to $\land$ operands?
Back: Conjuncts
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861304-->
END%%
%%ANKI
Basic
What name is given to $\lor$ operands?
Back: Disjuncts
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861306-->
END%%
%%ANKI
Basic
What C logical operator corresponds to $\neg$?
Back: `!`
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
Tags: c
<!--ID: 1706994861325-->
END%%
%%ANKI
Basic
What C logical operator corresponds to $\land$?
Back: There isn't one.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
Tags: c
<!--ID: 1706994861327-->
END%%
%%ANKI
Basic
What C logical operator corresponds to $\lor$?
Back: There isn't one.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
Tags: c
<!--ID: 1706994861329-->
END%%
%%ANKI
Basic
What C logical operator corresponds to $\Rightarrow$?
Back: There isn't one.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
Tags: c
<!--ID: 1706994861331-->
END%%
%%ANKI
Basic
What C logical operator corresponds to $\Leftrightarrow$?
Back: `==`
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
Tags: c
<!--ID: 1706994861333-->
END%%
%%ANKI %%ANKI
Basic Basic
What C bit-level operator corresponds to $\neg$? What C bit-level operator corresponds to $\neg$?

View File

@ -72,22 +72,6 @@ Tags: lean
<!--ID: 1706994861302--> <!--ID: 1706994861302-->
END%% END%%
%%ANKI
Basic
What name is given to $\land$ operands?
Back: Conjuncts
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861304-->
END%%
%%ANKI
Basic
What name is given to $\lor$ operands?
Back: Disjuncts
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861306-->
END%%
%%ANKI %%ANKI
Basic Basic
What name is given to operand $a$ in $a \Rightarrow b$? What name is given to operand $a$ in $a \Rightarrow b$?
@ -120,51 +104,6 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in
<!--ID: 1706994861320--> <!--ID: 1706994861320-->
END%% END%%
%%ANKI
Basic
What C logical operator corresponds to $\neg$?
Back: `!`
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
Tags: c
<!--ID: 1706994861325-->
END%%
%%ANKI
Basic
What C logical operator corresponds to $\land$?
Back: There isn't one.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
Tags: c
<!--ID: 1706994861327-->
END%%
%%ANKI
Basic
What C logical operator corresponds to $\lor$?
Back: There isn't one.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
Tags: c
<!--ID: 1706994861329-->
END%%
%%ANKI
Basic
What C logical operator corresponds to $\Rightarrow$?
Back: There isn't one.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
Tags: c
<!--ID: 1706994861331-->
END%%
%%ANKI
Basic
What C logical operator corresponds to $\Leftrightarrow$?
Back: `==`
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
Tags: c
<!--ID: 1706994861333-->
END%%
%%ANKI %%ANKI
Basic Basic
What proposition represents states $\{(b, T)\}$ and $\{(c, F)\}$? What proposition represents states $\{(b, T)\}$ and $\{(c, F)\}$?
@ -294,6 +233,7 @@ Basic
How is tautology $e$ written equivalently with a quantifier? How is tautology $e$ written equivalently with a quantifier?
Back: For free identifiers $i_1, \ldots, i_n$ in $e$, as $\forall (i_1, \ldots, i_n), e$. Back: For free identifiers $i_1, \ldots, i_n$ in $e$, as $\forall (i_1, \ldots, i_n), e$.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707937867032-->
END%% END%%
%%ANKI %%ANKI
@ -637,11 +577,36 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in
<!--ID: 1707762304123--> <!--ID: 1707762304123-->
END%% 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 %%ANKI
Basic Basic
What identifier is guaranteed to not occur in $E_e^x$? What identifier is guaranteed to not occur in $E_e^x$?
Back: None. Back: None.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707937867036-->
END%% END%%
%%ANKI %%ANKI
@ -649,6 +614,7 @@ Basic
What identifier is guaranteed to not occur in $E_{s(e)}^x$? What identifier is guaranteed to not occur in $E_{s(e)}^x$?
Back: $x$. Back: $x$.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707937867039-->
END%% END%%
%%ANKI %%ANKI
@ -656,6 +622,7 @@ Basic
*Why* does $x$ not occur in $E_{s(e)}^x$? *Why* does $x$ not occur in $E_{s(e)}^x$?
Back: Because $s(e)$ evaluates to a constant proposition. 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. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707937867042-->
END%% END%%
%%ANKI %%ANKI
@ -751,6 +718,7 @@ Basic
In textual substitution, what does e.g. $\bar{x}$ denote? In textual substitution, what does e.g. $\bar{x}$ denote?
Back: A list of *distinct* identifiers. Back: A list of *distinct* identifiers.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707937867046-->
END%% END%%
%%ANKI %%ANKI
@ -838,6 +806,7 @@ Basic
How does Gries denote state $s$ with identifer $x$ set to value $v$? How does Gries denote state $s$ with identifer $x$ set to value $v$?
Back: $(s; x{:}v)$ Back: $(s; x{:}v)$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707937867049-->
END%% END%%
%%ANKI %%ANKI
@ -845,6 +814,7 @@ Basic
How is $(s; x{:}v)$ written instead using set-theoretical notation? How is $(s; x{:}v)$ written instead using set-theoretical notation?
Back: $(s - \{(x, s(x))\}) \cup \{(x, v)\}$ Back: $(s - \{(x, s(x))\}) \cup \{(x, v)\}$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707937867053-->
END%% END%%
%%ANKI %%ANKI
@ -852,6 +822,7 @@ Basic
Execution of `x := e` in state $s$ terminates in what new state? Execution of `x := e` in state $s$ terminates in what new state?
Back: $(s; x{:}s(e))$ Back: $(s; x{:}s(e))$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707937867058-->
END%% END%%
%%ANKI %%ANKI
@ -859,6 +830,7 @@ Basic
Given state $s$, what statement does $(s; x{:}s(e))$ derive from? Given state $s$, what statement does $(s; x{:}s(e))$ derive from?
Back: `x := e` Back: `x := e`
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707937867062-->
END%% END%%
%%ANKI %%ANKI
@ -866,6 +838,7 @@ Basic
What missing value guarantees state $s$ satisfies equivalence $s = (s; x{:}\_)$? What missing value guarantees state $s$ satisfies equivalence $s = (s; x{:}\_)$?
Back: $s(x)$ Back: $s(x)$
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707937867067-->
END%% END%%
%%ANKI %%ANKI
@ -873,35 +846,62 @@ Basic
Given state $s$, why is it that $s = (s; x{:}s(x))$? Given state $s$, why is it that $s = (s; x{:}s(x))$?
Back: Evaluating $x$ in state $s$ yields $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. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707937867072-->
END%% END%%
* $s(E_e^x) = s(E_{s(e)}^x)$ * $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$. * Substituting $x$ with $e$ and then evaluating is the same as substituting $x$ with the evaluation of $e$.
* This follows directly from the recursive definition of state evaluation.
%%ANKI %%ANKI
Basic Basic
How can we simplify $s(E_{s(e)}^x)$? How can we simplify $s(E_{s(e)}^x)$?
Back: As $s(E_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. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707937867076-->
END%% END%%
%%ANKI %%ANKI
Basic Basic
What equivalence relates $E_e^x$ with $E_{s(e)}^x$? Given state $s$, what equivalence relates $E_e^x$ with $E_{s(e)}^x$?
Back: $s(E_e^x) = s(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. Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707937867080-->
END%% END%%
TODO
* Let $s$ be a state and $s' = (s; x{:}s(e))$. Then $s'(E) = s(E_e^x)$. * Let $s$ be a state and $s' = (s; x{:}s(e))$. Then $s'(E) = s(E_e^x)$.
TODO %%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
How can we write an expression equivalent to $s(E_e^x)$ that doesn't use textual substitution?
Back: Write $s'(E)$ where $s' = (s; x{:}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$. * Given identifiers $\bar{x}$ and fresh identifiers $\bar{u}$, $(E_{\bar{u}}^{\bar{x}})_{\bar{x}}^{\bar{u}} = E$.
TODO %%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%%
## References ## References