State Machines (review from Class 13)

A state machine, $M = (S, G: S \times S, q_0 \in S)$, is a binary relation (called a transition relation) on a set (both the domain and codomain are the same set). One state, denoted $q_0$, is designated as the start state.

An execution of a state machine $M = (S, G \subseteq S \times S, q_0 \in S)$ is a (possibly infinite) sequence of states, $(x_0, x_1, \cdots, x_n)$ where (1) $x_0 = q_0$ (it begins with the start state), and (2) $\forall i \in {0, 1, \ldots, n - 1} \ldotp (xi, x{i + 1}) \in G$ (if $q$ and $r$ are consecutive states in the sequence, then there is an edge $q \rightarrow r$ in $G$).

A state $q$ is reachable if it appears in some execution.

A preserved invariant of a state machine $M = (S, G \subseteq S \times S, q_0 \in S)$ is a predicate, $P$, on states, such that whenever $P(q)$ is true of a state $q$, and $q \rightarrow r \in G$, then $P®$ is true.

Bishop State Machine

$S = { (\fillin ) \, | \, r, c \in \mathbb{N} }$ $G = { (r, c) \rightarrow (r’, c’) \, | \, r, c \in \mathbb{N} \wedge (\exists d \in \mathbb{N}^{+} \textrm{ such that } r’ = r \fillin d \wedge r’ \ge 0 \wedge c’ = c \fillin d \wedge c’ \ge 0 }$ $q_0 = (0, 2)$

What states are reachable?

#

``Progress” Machine

$S = { (x, d) \, | \, x \in \mathbb{Z}, d \in { \mathrm{\bf F}, \mathrm{\bf B}} }$ $G = { (x, \mathrm{\bf F}) \rightarrow (x + 1, \mathrm{\bf B}) \, | \, x \in \mathbb{Z} } \cup { (x, \mathrm{\bf B}) \rightarrow (x - 2, \mathrm{\bf F}) \, | \, x \in \mathbb{Z} }$ $q_0 = (0, \mathrm{\bf F})$

Which states are reachable?

Preserved Invariants

A predicate $P(q)$ is a preserved invariant of machine $M = (S, G \subseteq S \times S, q_0 \in S)$ if: $$ \forall q \in S \ldotp (P(q) \wedge (q \rightarrow r) \in G) \implies P® $$

What are some preserved invariants for the (original) Bishop State Machine?

Invariant Principle. If a preserved invariant of a state machine is true for the start state, it is true for all reachable states.

To show $P(q)$ for machine $M = (S, G \subseteq S \times S, q_0 \in S)$ all $q \in S$, show:

1. Base case: $P(\fillin)$
2. $\forall s \in S \ldotp \fillin \implies \fillin$

Prove that the original Bishop State Machine never reaches a square where $r + c$ is odd.

Slow Exponentiation

def slow_power(a, b):
   y = 1
   z = b
   while z > 0:
      y = y * a
      z = z - 1
   return y

$S ::= \mathbb{N} \times \mathbb{N}$ $G ::= { (y, z) \rightarrow (y \cdot a, z - 1) \, | \, \forall y, z \in \mathbb{N}^{+}}$ $q_0 ::= (1, b)$

Prove slow_power(a, b) = $a^b$.

#

Fast Exponentiation

This is the algorithm from Section 6.3.1 written as Python code:

def power(a, b):
   x = a
   y = 1
   z = b
   while z > 0:
      r = z % 2 # remainder of z / 2
      z = z // 2 # quotient of z / 2
      if r == 1:
         y = x * y
      x = x * x
   return y