Closed Forms

An important theme of induction is determining closed forms from recursive functions and summations. This is a tool where you can use $T_{E} X$ notation to describe these and see how different values play out.

x^2

$x^2$
2x - 1

$2x - 1$
\sum_{k=1}^{x} g(k)

$\sum_{k=1}^{x} g(k)$
\begin{cases} 0 & x = 0 \\ 2p(x-1) + 1 & x > 0 \end{cases}

$\begin{cases} 0 & x = 0 \\ 2p(x-1) + 1 & x > 0 \end{cases}$

$x$ starts at

Working out the values…

Extended Euclid's Algorithm

Knuth provides an extended form of Euclid's Algorithm to illustrate the concepts in this section. Here is a table to explore how different values behave going through that algorithm.

m

n

$a^{'}$	$a$	$b^{'}$	$b$	$c$	$d$	$q$	$r$
1	0	0	1	1769	551	3	116
0	1	1	-3	551	116	4	87
1	-4	-3	13	116	87	1	29
-4	5	13	-16	87	29	3	0

$5 \cdot 1769 - 16 \cdot 551 = 29$
$\gcd(1769, 551) = 29$

Implementation

export function extended_euclids_algorithm(m: number, n: number) {
  // E1
  let a_prime = 1
  let b = 1
  let a = 0
  let b_prime = 0
  let c = m
  let d = n

  while (true) {
    // E2
    const q = Math.floor(c / d)
    const r = c % d

    if (r == 0) return { remainder: d, a, b } // E3

    // E4
    c = d
    d = r
    let t = a_prime
    a_prime = a
    a = t - q * a
    t = b_prime
    b_prime = b
    b = t - q * b
  }
}

export function extended_euclids_algorithm(
  m: number,
  n: number,
  a = 0,
  a_prime = 1,
  b = 1,
  b_prime = 0,
) {
  const q = Math.floor(m / n)
  const r = m % n
  if (r == 0) return { remainder: n, a, b }

  return extended_euclids_algorithm(n, r, a_prime - q * a, a, b_prime - q * b, b)
}

Creating Diagrams

To help you explore Assertions within diagrams more extensively, here is a tool to assist you in creating them and labelling assertions. Connect to other steps by mentioning their label (e.g. E1, E2, etc.). To branch, state "If condition, whatever." The word "terminate" signals the end of the algorithm. If you hover over or click a step in the diagram, it will show what's needed to prove that step.

Algorithm

A1 [Start ⇒ E1] $m > 0$, $n > 0$.
E1. $a \leftarrow 0$ $a' \leftarrow 1$ $c \leftarrow m$ $b \leftarrow 1$ $b' \leftarrow 0$ $d \leftarrow n$
A2 [E1 ⇒ E2] $c = m > 0$, $d = n > 0$, $a = b' = 0$, $a' = b = 1$.
E2. $q \leftarrow \text{quotient}(c / d)$ $r \leftarrow \text{remainder}(c / d)$
A3 [E2 ⇒ E3] $am + bn = d$, $a'm + b'n = c = qd + r$, $0 \leq r < d$, $\text{gcd}(c, d) = \text{gcd}(m, n)$.
E3. If r = 0, terminate.
A4 [E3 ⇒ End] $am + bn = d = \text{gcd}(m, n)$.
A5 [E3 ⇒ E4] $am + bn = d$, $a'm + b'n = c = qd + r$, $0 < r < d$, $\text{gcd}(c, d) = \text{gcd}(m, n)$.
E4. $c \leftarrow d$, $d \leftarrow r$; $t \leftarrow a'$, $a' \leftarrow a$, $a \leftarrow t - qa$; $t \leftarrow b'$, $b' \leftarrow b$, $b \leftarrow t - qb$. Go back to E2.
A6 [E4 ⇒ E2] $am + bn = d$, $a'm + b'n = c$, $d > 0$, $\text{gcd}(c, d) = \text{gcd}(m , n)$

---
config:
  forceLegacyMathML: true
  flowchart:
    minNodeWidth: 0
---
flowchart LR
  subgraph algorithm["Algorithm E"]
    direction TB
    Start@{ shape: flip-tri, label: "Start" }
    E1["$$\begin{array}{c} \text{E1. }a \leftarrow 0\text{ }a' \leftarrow 1\text{ }c \leftarrow m \cr b \leftarrow 1\text{ }b' \leftarrow 0\text{ }d \leftarrow n \end{array}$$"]
    E2["$$\begin{array}{c} \text{E2. }q \leftarrow \text{quotient}(c / d) \cr r \leftarrow \text{remainder}(c / d) \end{array}$$"]
    E3["E3. If r = 0, terminate."]
    E4["$$\begin{array}{c} \text{E4. }c \leftarrow d\text{, }d \leftarrow r\text{;} \cr t \leftarrow a'\text{, }a' \leftarrow a\text{, }a \leftarrow t - qa\text{;} \cr t \leftarrow b'\text{, }b' \leftarrow b\text{, }b \leftarrow t - qb\text{.} \cr \text{ Go back to E2.} \end{array}$$"]
    End@{ shape: tri, label: "End" }
    Start --> E1
    E1 --> E2
    E2 --> E3
    E3 -- "$$(\text{r = 0})$$" --> End
    E3 -- "$$\lnot(\text{r = 0})$$" --> E4
    E4 --> E2
  end
  subgraph assertions["Assertions"]
    direction TB
    A1["$$\text{A1. }m \gt  0\text{, }n \gt  0\text{.}$$"]:::bare
    A2["$$\begin{array}{c} \text{A2. }c = m \gt  0\text{, }d = n \gt  0\text{,} \cr a = b' = 0\text{, }a' = b = 1\text{.} \end{array}$$"]:::bare
    A3["$$\begin{array}{c} \text{A3. }am + bn = d\text{, }a'm + b'n = c = qd + r\text{,} \cr 0 \leq r \lt  d\text{, }\text{gcd}(c, d) = \text{gcd}(m, n)\text{.} \end{array}$$"]:::bare
    A4["$$\text{A4. }am + bn = d = \text{gcd}(m, n)\text{.}$$"]:::bare
    A5["$$\begin{array}{c} \text{A5. }am + bn = d\text{, }a'm + b'n = c = qd + r\text{,} \cr 0 \lt  r \lt  d\text{, }\text{gcd}(c, d) = \text{gcd}(m, n)\text{.} \end{array}$$"]:::bare
    A6["$$\text{A6. }am + bn = d\text{, }a'm + b'n = c\text{, }d \gt  0\text{, }\text{gcd}(c, d) = \text{gcd}(m , n)$$"]:::bare
    A1 ~~~ A2 ~~~ A3 ~~~ A4 ~~~ A5 ~~~ A6
  end
  algorithm ~~~ assertions