**Equivalence-transformation** refers to a class of calculi for [[prop-logic|propositional logic]] derived from negation ($\neg$), conjunction ($\land$), disjunction ($\lor$), implication ($\Rightarrow$), and equality ($=$).
Gries covers two in "The Science of Programming": a system of evaluation and a formal system. The system of evaluation mirrors how a computer processes instructions, at least in an abstract sense. The formal system serves as a theoretical framework for reasoning about propositions and their transformations without resorting to "lower-level" operations like substitution.
Who is the author of "The Science of Programming"?
Back: David Gries
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861286-->
END%%
%%ANKI
Cloze
Gries replaces logical operator {$\Leftrightarrow$} in favor of {$=$}.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861295-->
END%%
%%ANKI
Basic
What Lean theorem justifies Gries' choice of $=$ over $\Leftrightarrow$?
Back: `propext`
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
Tags: lean
<!--ID: 1706994861302-->
END%%
%%ANKI
Basic
What are the two calculi Gries describes equivalence-transformation with?
Back: A formal system and a system of evaluation.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707251673342-->
END%%
## Equivalence Schemas
A proposition is said to be a **tautology** if it evaluates to $T$ in every state it is well-defined in. We say propositions $E1$ and $E2$ are **equivalent** if $E1 = E2$ is a tautology. In this case, we say $E1 = E2$ is an **equivalence**.
%%ANKI
Basic
What does it mean for a proposition to be a tautology?
Back: That the proposition is true in every state it is well-defined in.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861323-->
END%%
%%ANKI
Basic
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$.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707937867032-->
END%%
%%ANKI
Basic
The term "equivalent" refers to a comparison between what two objects?
Back: Expressions.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707251673345-->
END%%
%%ANKI
Basic
What does it mean for two propositions to be equivalent?
Back: Given propositions $E1$ and $E2$, it means $E1 = E2$ is a tautology.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707251673347-->
END%%
%%ANKI
Basic
What is an equivalence?
Back: Given propositions $E1$ and $E2$, tautology $E1 = E2$.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707251673348-->
END%%
* Commutative Laws
* $(E1 \land E2) = (E2 \land E1)$
* $(E1 \lor E2) = (E2 \lor E1)$
* $(E1 = E2) = (E2 = E1)$
%%ANKI
Basic
Which of the basic logical operators do the commutative laws apply to?
Back: $\land$, $\lor$, and $=$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707251673350-->
END%%
%%ANKI
Basic
What do the commutative laws allow us to do?
Back: Reorder operands.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
**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$?
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(\foralli:0 \leqi<n:b[i]<y))_z^x$$
Back: $$(z <y \land(\foralli:0 \leqi<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(\foralli:0 \leqi<n:b[i]<y))_z^y$$
Back: $$(x <z \land(\foralli:0 \leqi<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(\foralli:0 \leqi<n:b[i]<y))_z^i$$
Back: $$(x <y \land(\foralli:0 \leqi<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.
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]$anabbreviationfor?
Back: $(\forall i, 1 \leq i <k \Rightarrowb[i]<x) \land(\foralli,k \leqi<n \Rightarrowx<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?