Transcript Limitations

Structural Induction
CS 611
Structural Induction
• Useful for proving properties about
languages.
• Useful for proving properties about
algorithms defined on languages.
• A generalization of the induction you
know and love.
Induction on the Naturals
0
n
n+1
To prove : n  N .P (n) prove
1. P (0)
2.n  N .P (n)  P (n  1)
P is true of the basis case and
if P is true of a number, then
P is true of that number  1.
And "1" is how you get new numbers.
Example
0
n
n+1
Prove: every natural number is odd or even.
Base: 0 is even.
Induction: if n is odd or even
then n+1 is odd or even.
Suppose n is odd, then n+1 is even
Suppose n is even then n+1 is odd.
Induction on Aexp
var
const
+
Suppose I want to prove a property of
all arithmetic expressions.
Like “eval (aexp) is finite” for some
evaluation function eval.
Aexp has 2 atoms and 2 constructors.
Aexp Aexp
-
Aexp Aexp
So induction on Aexp has
___ base cases and
___ inductive steps?
What is the induction theorem for
arithmetic expressions?
Induction on Aexp
var
const
+
To prove b  Aexp .P (b), prove :
1.P (const)
2.P ( var)
3.a, b  Aexp .P (a )  P (b)  P (a  b)
Aexp Aexp
-
Aexp Aexp
4.a, b  Aexp .P (a )  P (b)  P (a - b)
Example
Eval (aexp a)
if a = var then val(a)
if a = const then a
if a = (b+c) then eval(b)*eval(c)
if a = (b-c) then eval(b)/eval(c)
Prove: forall a:aexp. eval(a) terminates
Base 1: eval(var) terminates
Base 2: eval(const) terminates
Ind1: suppose eval(b) and eval(c) terminate
prove eval (b+c) termiantes
Ind2: suppose eval(b) and eval(c) terminate
prove eval(b-c) terminates
Example
Eval (aexp a)
if a = var then val(a)
if a = const then a
if a = (b+c) then eval(b)*eval(c)
if a = (b-c) then eval(b)/eval(c)
Prove: forall a:aexp. eval(a) = correct_val(a)
Base 1: eval(var) = correct_val(var)
Base 2: eval(const) = correct_val(const)
Ind1: suppose eval(b) = correct_eval(b)
and eval(c) = correct_eval(c)
prove eval(b+c) = correct_eval(b+c)
Ind2: suppose eval(b) = correct_eval(b)
and eval(c) = correct_eval(c)
prove eval(b-c) = correct_eval(b-c)
Example
Eval (aexp a)
if a = var then val(a)
if a = const then a
if a = (b+c) then eval(b)*eval(c)
if a = (b-c) then eval(b)/eval(c)
Prove: forall a:aexp. eval(a) is finite
Base 1: eval(var) is finite
Base 2: eval(const) is finite
Ind1: suppose eval(b) is finite
and eval(c) is finite
prove eval(b+c) is finite
Ind2: suppose eval(b) is finite
and eval(c) is finite
prove eval(b-c) is finite
Reminders
• Reverse engineer proof of Thm 3.1 to
scratch work for Monday.
• Start on proofs of Thms 3.2, 3.3,
probably for Tuesday.
• Thm 3.4 and Cor 3.2 likely for Friday
• Paper 1 on Friday
• Cancel Godel encoding part of hwk.