留学生考试辅导 COMP 302: Programming Languages and Paradigms

COMP 302: Programming Languages and Paradigms
Week 3: Induction Proof Prof. Xujie Si

How do you gain confidence about your code?

How do you gain confidence about your code?
• No syntax error • Type checking • Testing

How do you gain confidence about your code?
• No syntax error • Type checking • Testing
Programs are executable math. –Your Instructor

Why? And who cares?

Why? And who cares?
$125 million lost!!

Inductive Definitions and Proofs by Induction

Inductive Definitions and Proofs by Induction
type nat = O | S of nat

Inductive Definitions and Proofs by Induction
type nat = O | S of nat
type lst = E | C of int * lst

Inductive Definitions and Proofs by Induction
type nat = O | S of nat
type lst = E | C of int * lst
type tree = Leaf | Node of int * tree * tree

Inductive Definitions and Proofs by Induction
type nat = O | S of nat
type lst = E | C of int * lst
type tree = Leaf | Node of int * tree * tree
Proof by induction

Inductive Definitions and Proofs by Induction
type nat = O | S of nat
type lst = E | C of int * lst
type tree = Leaf | Node of int * tree * tree
Proof by induction
1+3+5+⋯+ 2𝑛 −1 =𝑛!

Inductive Definitions and Proofs by Induction
type nat = O | S of nat
type lst = E | C of int * lst
type tree = Leaf | Node of int * tree * tree
Proof by induction
1+3+5+⋯+ 2𝑛 −1 =𝑛!
Basecase:n=1 LHS=1 RHS:1! =1 Stepcase:assume1+3+5+ …+ 2𝑘 −1 =𝑘!
consider 𝑛 = 𝑘 + 1
LHS=1+3+5+ …+ 2𝑘−1 + 2(𝑘+1) −1
=1+3+5+ …+ 2𝑘 −1 +(2𝑘+1)

Proving some basic properties of list

Proving some basic properties of list
type lst = E | C of int * lst
type ‘a list = []| (::) of ‘a * (‘a list)

Proving some basic properties of list
type lst = E | C of int * lst
type ‘a list = []| (::) of ‘a * (‘a list)
Theorem 1: ∀𝑙 ∶ 𝑙𝑖𝑠𝑡,𝑙𝑒𝑛 𝑙 ≥ 0

Proving some basic properties of list
type lst = E | C of int * lst
type ‘a list = []| (::) of ‘a * (‘a list)
Theorem 1: ∀𝑙 ∶ 𝑙𝑖𝑠𝑡,𝑙𝑒𝑛 𝑙 ≥ 0
Key Idea: Induction

Proving some basic properties of list
type lst = E | C of int * lst
type ‘a list = []| (::) of ‘a * (‘a list)
Theorem 1: ∀𝑙 ∶ 𝑙𝑖𝑠𝑡,𝑙𝑒𝑛 𝑙 ≥ 0
Key Idea: Induction
∀ 𝑛 ≥ 1, 𝑃(𝑛)
• P(1)istrue
• P(n)=>P(n+1)

Length is non-negative
Theorem 1: ∀𝑙 ∶ 𝑙𝑖𝑠𝑡,𝑙𝑒𝑛 𝑙 ≥ 0

Length is non-negative
Base Case: 𝑙 = []
Theorem 1: ∀𝑙 ∶ 𝑙𝑖𝑠𝑡,𝑙𝑒𝑛 𝑙 ≥ 0

Length is non-negative
Base Case: 𝑙 = []
len l = len [] = 0
Theorem 1: ∀𝑙 ∶ 𝑙𝑖𝑠𝑡,𝑙𝑒𝑛 𝑙 ≥ 0

Length is non-negative
Base Case: 𝑙 = []
len l = len [] = 0
Step Case:
Theorem 1: ∀𝑙 ∶ 𝑙𝑖𝑠𝑡,𝑙𝑒𝑛 𝑙 ≥ 0

Length is non-negative
Base Case: 𝑙 = []
len l = len [] = 0
Step Case:
Induction Hypothesis: len xs >= 0
Theorem 1: ∀𝑙 ∶ 𝑙𝑖𝑠𝑡,𝑙𝑒𝑛 𝑙 ≥ 0

Length is non-negative
Base Case: 𝑙 = []
len l = len [] = 0
Step Case:
Induction Hypothesis: len xs >= 0 Consider l = x :: xs
Theorem 1: ∀𝑙 ∶ 𝑙𝑖𝑠𝑡,𝑙𝑒𝑛 𝑙 ≥ 0

Length is non-negative
Base Case: 𝑙 = []
len l = len [] = 0
Step Case:
Induction Hypothesis: len xs >= 0 Consider l = x :: xs
len l = len (x::xs) = 1 + len xs
Theorem 1: ∀𝑙 ∶ 𝑙𝑖𝑠𝑡,𝑙𝑒𝑛 𝑙 ≥ 0

Length is non-negative
Base Case: 𝑙 = []
len l = len [] = 0
Step Case:
Theorem 1: ∀𝑙 ∶ 𝑙𝑖𝑠𝑡,𝑙𝑒𝑛 𝑙 ≥ 0
Induction Hypothesis: len xs >= 0
Consider l = x :: xs lenl=len(x::xs)=1+lenxs >=1+0>=0

List concatenation

List concatenation
Theorem 2:
∀𝑙”, 𝑙!: 𝑙𝑖𝑠𝑡, 𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑙” 𝑙! = 𝑙𝑒𝑛 𝑙” + 𝑙𝑒𝑛 𝑙!

List concatenation
Theorem 2:
∀𝑙”, 𝑙!: 𝑙𝑖𝑠𝑡, 𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑙” 𝑙! = 𝑙𝑒𝑛 𝑙” + 𝑙𝑒𝑛 𝑙!
What should be the base case?

List concatenation
Theorem 2:
∀𝑙”, 𝑙!: 𝑙𝑖𝑠𝑡, 𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑙” 𝑙! = 𝑙𝑒𝑛 𝑙” + 𝑙𝑒𝑛 𝑙!
What should be the base case?
What should be the inductive hypothesis?

List concatenation
Theorem 2:
∀𝑙”, 𝑙!: 𝑙𝑖𝑠𝑡, 𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑙” 𝑙! = 𝑙𝑒𝑛 𝑙” + 𝑙𝑒𝑛 𝑙!
What should be the base case?
What should be the inductive hypothesis?
Base case: l1 = [], l2 = []

List concatenation
Theorem 2:
∀𝑙”, 𝑙!: 𝑙𝑖𝑠𝑡, 𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑙” 𝑙! = 𝑙𝑒𝑛 𝑙” + 𝑙𝑒𝑛 𝑙!
What should be the base case?
What should be the inductive hypothesis?
Step case:
Base case: l1 = [], l2 = []
LHS: len (concat [] []) = len [] = 0
RHS: len [] + len [] = 0 + 0 = 0
l1 = x :: xs
l2 = y :: ys

List concatenation
Theorem 2:
∀𝑙”, 𝑙!: 𝑙𝑖𝑠𝑡, 𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑙” 𝑙! = 𝑙𝑒𝑛 𝑙” + 𝑙𝑒𝑛 𝑙!
What should be the base case?
What should be the inductive hypothesis?
Base case: l1 = [], l2 = []
LHS: len (concat [] []) = len [] = 0
RHS: len [] + len [] = 0 + 0 = 0
Step case: l1 = x :: xs l2 = y :: ys
Induction Hypothesis:
𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑥𝑠𝑦𝑠 =𝑙𝑒𝑛𝑥𝑠+𝑙𝑒𝑛𝑦𝑠

List concatenation
Theorem 2:
∀𝑙”, 𝑙!: 𝑙𝑖𝑠𝑡, 𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑙” 𝑙! = 𝑙𝑒𝑛 𝑙” + 𝑙𝑒𝑛 𝑙!
What should be the base case?
Base case: l1 = [], l2 = []
LHS: len (concat [] []) = len [] = 0
RHS: len [] + len [] = 0 + 0 = 0
Step case: l1 = x :: xs l2 = y :: ys
Induction Hypothesis:
𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑥𝑠𝑦𝑠 =𝑙𝑒𝑛𝑥𝑠+𝑙𝑒𝑛𝑦𝑠
LHS: len (concat l1 l2)
= len (concat (x::xs) (y::ys))
= len (x :: (concat xs (y::ys)))
RHS: len (x::xs) + len (y::ys)
What should be the inductive hypothesis?
Got stuck!
IH is NOT applicable
= 1 + len (concat xs (y::ys))
= (1 + len xs) + (1 + len ys)

List concatenation (2nd attempt)
Why our first attempt failed? Induction Hypothesis:
𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑥𝑠𝑦𝑠 =𝑙𝑒𝑛𝑥𝑠+𝑙𝑒𝑛𝑦𝑠
LHS = 1 + len (concat xs (y::ys))

List concatenation (2nd attempt)
Why our first attempt failed?
Induction Hypothesis:
𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑥𝑠𝑦𝑠 =𝑙𝑒𝑛𝑥𝑠+𝑙𝑒𝑛𝑦𝑠
LHS = 1 + len (concat xs (y::ys))

List concatenation (2nd attempt)
Why our first attempt failed?
Induction Hypothesis:
𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑥𝑠𝑦𝑠 =𝑙𝑒𝑛𝑥𝑠+𝑙𝑒𝑛𝑦𝑠
LHS = 1 + len (concat xs (y::ys))
(More general) Induction Hypothesis:
∀𝑙:𝑙𝑖𝑠𝑡,𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑥𝑠𝑙 =𝑙𝑒𝑛𝑥𝑠+𝑙𝑒𝑛𝑙
Base case: l1 = []
LHS: len (concat [] l2) = len l2

List concatenation (2nd attempt)
Why our first attempt failed?
Induction Hypothesis:
𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑥𝑠𝑦𝑠 =𝑙𝑒𝑛𝑥𝑠+𝑙𝑒𝑛𝑦𝑠
LHS = 1 + len (concat xs (y::ys))
Base case: l1 = []
LHS: len (concat [] l2) = len l2
RHS: len [] + len l2 = 0 + len l2 = len l2
Stepcase: l1=x::xs LHS: len (concat (x::xs) l2)
= len (x :: (concat xs l2))
= 1 + len (concat xs l2)
(More general) Induction Hypothesis:
∀𝑙:𝑙𝑖𝑠𝑡,𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑥𝑠𝑙 =𝑙𝑒𝑛𝑥𝑠+𝑙𝑒𝑛𝑙

List concatenation (2nd attempt)
Why our first attempt failed?
Induction Hypothesis:
𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑥𝑠𝑦𝑠 =𝑙𝑒𝑛𝑥𝑠+𝑙𝑒𝑛𝑦𝑠
LHS = 1 + len (concat xs (y::ys))
Base case: l1 = []
LHS: len (concat [] l2) = len l2
RHS: len [] + len l2 = 0 + len l2 = len l2
Stepcase: l1=x::xs LHS: len (concat (x::xs) l2)
= len (x :: (concat xs l2))
= 1 + len (concat xs l2)
= 1 + (len xs + len l2)
(More general) Induction Hypothesis:
∀𝑙:𝑙𝑖𝑠𝑡,𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑥𝑠𝑙 =𝑙𝑒𝑛𝑥𝑠+𝑙𝑒𝑛𝑙

List concatenation (2nd attempt)
Why our first attempt failed?
Induction Hypothesis:
𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑥𝑠𝑦𝑠 =𝑙𝑒𝑛𝑥𝑠+𝑙𝑒𝑛𝑦𝑠
LHS = 1 + len (concat xs (y::ys))
Base case: l1 = []
LHS: len (concat [] l2) = len l2
RHS: len [] + len l2 = 0 + len l2 = len l2
Stepcase: l1=x::xs LHS: len (concat (x::xs) l2)
= len (x :: (concat xs l2))
= 1 + len (concat xs l2)
= 1 + (len xs + len l2)
RHS: len (x::xs) + len l2
(More general) Induction Hypothesis:
∀𝑙:𝑙𝑖𝑠𝑡,𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑥𝑠𝑙 =𝑙𝑒𝑛𝑥𝑠+𝑙𝑒𝑛𝑙

List concatenation (2nd attempt)
Why our first attempt failed?
Induction Hypothesis:
𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑥𝑠𝑦𝑠 =𝑙𝑒𝑛𝑥𝑠+𝑙𝑒𝑛𝑦𝑠
LHS = 1 + len (concat xs (y::ys))
Base case: l1 = []
LHS: len (concat [] l2) = len l2
RHS: len [] + len l2 = 0 + len l2 = len l2
Stepcase: l1=x::xs LHS: len (concat (x::xs) l2)
= len (x :: (concat xs l2))
= 1 + len (concat xs l2)
= 1 + (len xs + len l2)
RHS: len (x::xs) + len l2
= (1 + len xs) + len l2
(More general) Induction Hypothesis:
∀𝑙:𝑙𝑖𝑠𝑡,𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑥𝑠𝑙 =𝑙𝑒𝑛𝑥𝑠+𝑙𝑒𝑛𝑙

List concatenation (2nd attempt)
Why our first attempt failed?
Induction Hypothesis:
𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑥𝑠𝑦𝑠 =𝑙𝑒𝑛𝑥𝑠+𝑙𝑒𝑛𝑦𝑠
LHS = 1 + len (concat xs (y::ys))
Base case: l1 = []
LHS: len (concat [] l2) = len l2
RHS: len [] + len l2 = 0 + len l2 = len l2
Stepcase: l1=x::xs LHS: len (concat (x::xs) l2)
= len (x :: (concat xs l2))
= 1 + len (concat xs l2)
= 1 + (len xs + len l2)
RHS: len (x::xs) + len l2
= (1 + len xs) + len l2
(More general) Induction Hypothesis:
∀𝑙:𝑙𝑖𝑠𝑡,𝑙𝑒𝑛 𝑐𝑜𝑛𝑐𝑎𝑡 𝑥𝑠𝑙 =𝑙𝑒𝑛𝑥𝑠+𝑙𝑒𝑛𝑙
Associativity: 𝑎+𝑏 +𝑐=𝑎+(𝑏+𝑐)

List reversal

List reversal
Are rev and rev_tl equivalent?

List reversal
Are rev and rev_tl equivalent?
Theorem 3:
∀𝑙∶𝑙𝑖𝑠𝑡,𝑟𝑒𝑣 𝑙 =𝑟𝑒𝑣#$ 𝑙 []

List reversal
Theorem 3:
∀𝑙∶𝑙𝑖𝑠𝑡,𝑟𝑒𝑣 𝑙 =𝑟𝑒𝑣#$ 𝑙 []

List reversal
Theorem 3:
∀𝑙∶𝑙𝑖𝑠𝑡,𝑟𝑒𝑣 𝑙 =𝑟𝑒𝑣#$ 𝑙 []
Base case: l = []

List reversal
Theorem 3:
∀𝑙∶𝑙𝑖𝑠𝑡,𝑟𝑒𝑣 𝑙 =𝑟𝑒𝑣#$ 𝑙 []
Base case: l = [] LHS: rev [] = []

List reversal
Theorem 3:
∀𝑙∶𝑙𝑖𝑠𝑡,𝑟𝑒𝑣 𝑙 =𝑟𝑒𝑣#$ 𝑙 []
Base case: l = []
LHS: rev [] = []
RHS: rev_tl [] [] = []

List reversal
Theorem 3:
∀𝑙∶𝑙𝑖𝑠𝑡,𝑟𝑒𝑣 𝑙 =𝑟𝑒𝑣#$ 𝑙 []
Base case: l = [] LHS: rev [] = []
RHS: rev_tl [] [] = [] Stepcase: l=x::xs

List reversal
Theorem 3:
∀𝑙∶𝑙𝑖𝑠𝑡,𝑟𝑒𝑣 𝑙 =𝑟𝑒𝑣#$ 𝑙 []
Base case: l = [] LHS: rev [] = []
RHS: rev_tl [] [] = []
Stepcase: l=x::xs
IH: 𝑟𝑒𝑣 𝑥𝑠 = 𝑟𝑒𝑣”# 𝑥𝑠 []

List reversal
Theorem 3:
∀𝑙∶𝑙𝑖𝑠𝑡,𝑟𝑒𝑣 𝑙 =𝑟𝑒𝑣#$ 𝑙 []
Base case: l = [] LHS: rev [] = []
RHS: rev_tl [] [] = []
Stepcase: l=x::xs
IH: 𝑟𝑒𝑣 𝑥𝑠 = 𝑟𝑒𝑣”# 𝑥𝑠 []
LHS: rev (x::xs)

程序代写 CS代考加微信: powcoder QQ: 1823890830 Email: powcoder@163.com

Related Posts