up arrow proof
In this page I will prove that in Bowers' array notation, {a,b,c} is equal to a^cb for all a, b, and c. I will prove it like so:
- Prove that {a,b,1} = a^b
- Prove with induction on b that {a,b,2} = a^^b
- Prove inductively that {a,b,c} = a^cb with induction on b and c
First off, it's easy to see why {a,b,1} = a^b. For this array, we follow rule 2 of array notation (remove the 1 at the end), giving us the array {a,b}, which evaluates to a^b.
Now let's try to see if {a,b,2} = a^^b. We'll prove it inductively, first showing that {a,1,2} = a^^1, then that if {a,b,2} = a^^b, then {a,b+1,2} = a^^(b+1).
To evaluate {a,1,2}, we follow the 3rd rule (2nd entry is 1), which states that if the second entry of an array is 1, then the array evaluates to the first entry. Then, {a,1,2} evaluates to a, which is the same as a^^1.
Now, let's assume that {a,b,2} = a^^b. Does a similar equality hold for {a,b+1,2}? To find out, we calculate:
{a,b+1,2}
= {a,{a,b,2},1} [rule 5]
= {a,{a,b,2}} [rule 2]
= {a,a^^b} [given]
= a^(a^^b) [rule 1]
= a^^(b+1) [definition of up-arrow notation]
Now let's try a more general case. Let's assume that {a,b,c} = a^cb, and that {a,b,c-1} = a^c-1b as well. Then, we will need to show that {a,b+1,c} = a^c(b+1), and that {a,b,c+1} = a^c+1b.
If {a,b,c} = a^cb, then:
{a,b+1,c}
= {a,{a,b,c},c-1}
= a^c-1({a,b,c})
= a^c-1(a^cb)
= a^c(b+1)
And also, if {a,b,c} = a^cb, then we need to first show that {a,1,c+1} = a (same thing as a^c+11), and then that if {a,b,c+1} = a^c+1b then {a,b+1,c+1} = a^c+1(b+1). This will complete the proof.
{a,1,c+1}
= a (rule 3 tells us to remove the 1)
and
{a,b+1,c+1}
= {a,{a,b,c+1},c}
= a^c(a^c+1b)
= a^c+1(b+1)
So we have now completed the proof of translating Bowers' array notation to Knuth's up-arrows.