# 代写代考 Advanced Structural Induction – cscodehelp代写

Learning Outcomes

by the End of the Lecture, Students that Complete
the Recommended Exercises should be Able to:
Prove Termination using Rank Functions Prove Correctness using Structural Induction Use Structural Induction (on a Dubious Program) Use Structural Induction (on a Branching Program)

Structural Induction
How would you Write a Function for Computing the Length of List?
length :: [a] -> Int

Structural Induction
length :: [a] -> Int length [] = 0
length (h:t) = 1 + length t
How would you Trace the following Evaluation? length [1, 2, 3]

length :: [a] -> Int length [] = 0
length (h:t) = 1 + length t
How would you Trace the following Evaluation?
length [1, 2, 3]
1 + length [2, 3]
1 + (1 + length )
1 + (1 + (1 + length [])) 1 + (1 + (1 + 0))
Structural Induction

Structural Induction
How would you Write a Function for Concatenating Two Lists (without ++)?
concat :: [a] -> [a] -> [a]

Structural Induction
concat :: [a] -> [a] -> [a] concat [] x = x
concat (h:t) x = h : (concat t x)
How would you Trace the following Evaluation? concat [1, 2, 3] [4, 5, 6]

concat :: [a] -> [a] -> [a] concat [] x = x
concat (h:t) x = h : (concat t x)
How would you Trace the following Evaluation?
concat [1, 2, 3] [4, 5, 6]
1 : (concat [2, 3] [4, 5, 6])
1 : (2 : (concat  [4, 5, 6]))
1 : (2 : (3 : (concat  [4, 5, 6]))) 1 : (2 : (3 : [4, 5, 6]))
Structural Induction

Structural Induction
the Conjecture to be Proven is that Concatenating Lists Length x and y results in a List of Length x + y
i.e., Proving that this Works is the Same As Proving length (concat a b) = (length a) + (length b)

Structural Induction to Prove that a Property 𝑃 holds for
All Finite Lists using Structural Induction: Prove the Property Holds for the Base Case
i.e., 𝑃 = 𝑇𝑟𝑢𝑒
Then Prove that, Under the Assumption 𝑃 𝑥 = 𝑇𝑟𝑢𝑒,
the Claim 𝑃 𝑦 ∶ 𝑥 = 𝑇𝑟𝑢𝑒 Holds as well

Structural Induction first Prove the Base Case…
What is the Base Case? …then Assume…
What is the Inductive Assumption? …in order To Prove…

Structural Induction first Prove the Base Case…
length (concat [] b) = (length []) + (length b)
…then Assume…
length (concat a b) = (length a) + (length b)
…in order To Prove…
length (concat (h:t) b) = (length (h:t)) + (length b)

Structural Induction
What is the Knowledge Base?
i.e., What Properties will we Use for this Proof?
this is Programming in the Functional Paradigm, so the Code Describes “What” length and concat are, and Not “How” they are Computed

Structural Induction
Knowledge Base
length [] = 0
length (h:t) = 1 + length (t)
concat [] x = x
concat (h:t) x = h : (concat t x)
length (concat a b) = (length a) + (length b)
Prove: length (concat [] b) = (length []) + (length b)

Structural Induction
Knowledge Base
length [] = 0
length (h:t) = 1 + length (t)
concat [] x = x
concat (h:t) x = h : (concat t x)
length (concat a b) = (length a) + (length b)
length (concat [] b) = (length []) + (length b)
length b = (length []) + (length b) length b = 0 + (length b)
length b = length b
by C1 by L1

Structural Induction
Knowledge Base
length [] = 0
length (h:t) = 1 + length (t)
concat [] x = x
concat (h:t) x = h : (concat t x)
length (concat a b) = (length a) + (length b)
Prove: length (concat (h:t) b) = (length (h:t)) + (length b)

Structural Induction
Knowledge Base
length [] = 0
length (h:t) = 1 + length (t)
concat [] x = x
concat (h:t) x = h : (concat t x)
length (concat a b) = (length a) + (length b)
length (concat (h:t) b) = (length (h:t)) + (length b)
length (h : (concat t b)) = (length (h:t)) + (length b) 1 + length (concat t b) = (length (h:t)) + (length b)
1 + (length t) + (length b) = (length (h:t)) + (length b) 1 + (length t) + (length b) = 1 + length (t) + (length b) Q.E.D.
by C2 by L2 by IA by L2

Structural Induction (with a Questionable Program)
How would you Write a Function for Computing the Arithmetic Mean of a List of Floats?
average :: [Float] -> Float

Structural Induction (with a Questionable Program) Would this Work?
average :: [Float] -> Float
average [] = error “Nope!” average x = weird x 0
weird :: [Float] -> Float -> Float
weird (h:(x:y)) n = weird ((h+x):y) (n+1) weird (h:[]) n = (h/(n+1))

Structural Induction (with a Questionable Program)
weird :: [Float] -> Float -> Float weird (h:(x:y)) n = weird ((h+x):y) (n+1) weird (h:[]) n = (h/(n+1))
How would you Trace the following Evaluation? (and To What are h, x, and y Bound to at Each Stage?)
weird [1, 2, 3, 9, 10] 0

Structural Induction (with a Questionable Program)
weird [1, 2, 3, 9, 10] 0 weird ((1 + 2) : [3, 9, 10]) 1 weird (3 : [3, 9, 10]) 1 weird ((3 + 3) : [9, 10]) 2 weird (6 : [9, 10]) 2 weird ((6 + 9) : ) 3 weird ((15 : ) 3 weird ((15 + 10) : []) 4 weird (25 : []) 4
25 / (4+1)
Does it Always Work?
i.e., How do you Prove the Total Correctness of the

Structural Induction (with a Questionable Program) to Prove that a Function is Totally Correct
you must Prove that:
the Function Terminates whenever the Input is Valid
this is known as “Termination”
If the Function Terminates, Then the Result is Correct

Structural Induction (with a Questionable Program)
How do we Prove Termination?
average :: [Float] -> Float average [] = error “Nope!” average x = weird x 0
weird :: [Float] -> Float -> Float weird (h:(x:y)) n = weird ((h+x):y) (n+1) weird (h:[]) n = (h/(n+1))

Structural Induction (with a Questionable Program) this is 𝒂𝒍𝒎𝒐𝒔𝒕 Primitive Recursion
(which would Guarantee that Termination occurs)
weird :: [Float] -> Float -> Float weird (h:(x:y)) n = weird ((h+x):y) (n+1) weird (h:[]) n = (h/(n+1))
Primitive Recursion for Lists has a Base Case at [] and a Recursive Case at h : t such that the Argument for Each Recursive Call is t

Structural Induction (with a Questionable Program)
alternatively, to Prove that Recursive Function 𝑓 Terminates, Devise a Rank Function that Maps Each Input onto a Nonnegative Integer and Prove:
If function 𝒇 is passed an Argument of Rank 𝑘 Then Rank 𝑘 must be Greater Than the Rank of the Argument passed to Each Subsequent Recursive Call

Structural Induction (with a Questionable Program)
weird :: [Float] -> Float -> Float weird (h:(x:y)) n = weird ((h+x):y) (n+1) weird (h:[]) n = (h/(n+1))
What is a Suitable Rank Function? rank :: [Float] -> Float -> Integer

Structural Induction (with a Questionable Program)
weird :: [Float] -> Float -> Float
weird (h:(x:y)) n = weird ((h+x):y) (n+1) weird (h:[]) n = (h/(n+1))
What is a Suitable Rank Function? rank :: [Float] -> Float -> Integer
rank x n = length x

Structural Induction (with a Questionable Program)
having proven Termination, for Total Correctness the only Conjecture to be Proven is that average x (i.e., weird x 0) Returns the Correct Mean of x
since the Mean of [𝑎1, 𝑎2, 𝑎3, … , 𝑎𝑛] can be 𝑖=0
Computed using σ𝑛 𝑎𝑖 , Proving this Conjecture 𝑛

Structural Induction (with a Questionable Program) first Prove the Base Case…
What is the Base Case? …then Assume…
What is the Inductive Assumption? …in order To Prove…

Structural Induction (with a Questionable Program) first Prove the Base Case…
weird (h:[]) 0 = sum (h:[]) / length (h:[])
…then Assume… weird t 0 = sum t / length t
…in order To Prove…
weird (h:t) 0 = (sum (h:t)) / (length (h:t))

Structural Induction (with a Questionable Program) What is the Knowledge Base?
i.e., What Properties will we Use for this Proof?

Structural Induction (with a Questionable Program)
What is the Knowledge Base?
i.e., What Properties will we Use for this Proof?
Knowledge Base
weird (h:[]) n = (h/(n+1))
weird (h:(x:y)) n = weird ((h+x):y) (n+1)
sum [] = 0
sum (h:t) = h + sum t
length [] = 0
length (h:t) = 1 + length t

Structural Induction (with a Questionable Program)
Knowledge Base
weird (h:[]) n = (h/(n+1))
weird (h:(x:y)) n = weird ((h+x):y) (n+1)
sum [] = 0
sum (h:t) = h + sum t
length [] = 0
length (h:t) = 1 + length t
first Prove the Base Case weird (h:[]) 0 =
sum (h:[]) / length (h:[])

Structural Induction (with a Questionable Program)
Knowledge Base
weird (h:[]) n = (h/(n+1))
weird (h:(x:y)) n = weird ((h+x):y) (n+1)
sum [] = 0
sum (h:t) = h + sum t
length [] = 0
length (h:t) = 1 + length t
first Prove the Base Case weird (h:[]) 0 =
sum (h:[]) / length (h:[])
weird (h:[]) 0
= h / (0 + 1) W1 =h/1

Structural Induction (with a Questionable Program)
Knowledge Base
weird (h:[]) n = (h/(n+1))
weird (h:(x:y)) n = weird ((h+x):y) (n+1)
sum [] = 0
sum (h:t) = h + sum t
length [] = 0
length (h:t) = 1 + length t
first Prove the Base Case weird (h:[]) 0 =
sum (h:[]) / length (h:[])
weird (h:[]) 0
= h / (0 + 1)
Right Side
sum (h:[]) / length (h:[])
W1 = (h + sum []) / length (h:[]) S2 = (h + 0) / length (h:[]) S1 = h / length (h:[])
= h / (1 + length []) L2 = h / (1 + 0) L1 =h/1

Structural Induction (with a Questionable Program)
Knowledge Base
weird (h:[]) n = (h/(n+1))
weird (h:(x:y)) n = weird ((h+x):y) (n+1)
sum [] = 0
sum (h:t) = h + sum t
length [] = 0
length (h:t) = 1 + length t
weird t 0 = sum t / length t
Proving the Inductive Case is Substantially Harder (even with the inclusion of the Inductive Assumption)
to Prove weird (h:t) 0 = sum (h:t)) / (length (h:t) with a Proof by Cases, What are the Cases?

Structural Induction (with a Questionable Program)
to Prove weird (h:t) 0 = sum (h:t)) / (length (h:t) Note that t is a List and a List is a Variant Type, so Either t is Empty or t can be Written (x:y)
Prove weird (h:[]) 0 = sum (h:[])) / (length (h:[]) n.b., this is just the base case again so no additional steps are required
Prove weird (h:(x:y)) 0 = sum (h:(x:y))) / (length (h:(x:y))

Structural Induction (with a Questionable Program)
Knowledge Base
weird (h:[]) n = (h/(n+1))
weird (h:(x:y)) n = weird ((h+x):y) (n+1)
sum [] = 0
sum (h:t) = h + sum t
length [] = 0
length (h:t) = 1 + length t
weird x 0 = sum x / length x
Prove weird (h:(x:y)) 0 =
sum (h:(x:y))) / (length (h:(x:y))
weird (h : (x : y)) 0
= weird ((h + x) : y) 0+1 W2 = weird ((h + x) : y) 1
= weird ((h + x + 0) : y) 1
= weird ((h + x) : (0 : y)) 0 W2 =sum((h+x):(0:y)))/length((h+x):(0 : y))) IA = ((h + x) + sum (0 : y)) / length ((h + x) : (0 : y))) S2 = ((h + x) + (0 + sum y)) / length ((h + x) : (0 : y))) S2 = ((h + x) + sum y) / length ((h + x) : (0 : y)))
= (h + (x + sum y)) / length ((h + x) : (0 : y))) =(h+sum(x:y))/length((h+x):(0:y))) S2 =sum(h:(x:y))/length((h+x):(0:y))) S2 = sum (h : (x : y)) / 1 + length (0 : y))) L2 = sum (h : (x : y)) / 1 + 1 + length y)) L2 = sum (h : (x : y)) / 1 + length (x : y)) L2 = sum (h : (x : y)) / length (h : (x : y))) L2

Structural Induction (with a Branching Program)
How would you Prove (with Induction) that the Sum of 𝑛 Even Numbers is, itself, an Even Number?

Structural Induction (with a Branching Program)
start with the Lemma (i.e., Intermediate Proof) that the Sum of Two Even Numbers is Even
the Operational Definition of an Even Number can be Stated as “𝑛 is Even” ≡ ∃𝑘 𝑘 ∈ Z ∧ 𝑛 = 2𝑘

3. 4. 5. 6.
10. 11. 12. 13. 14.
15. 16. 17.
Structural Induction (with a Branching Program) 𝑛 is Even ∧ 𝑚 is Even
∃𝑘 𝑘∈Z∧𝑛=2𝑘
𝑎∈Z ∧ 𝑛=2𝑎 𝑛 = 2𝑎
∃𝑘 𝑘∈Z∧𝑚=2𝑘 𝑏∈Z ∧ 𝑚=2𝑏
𝑛 + 𝑚 = 2𝑎 + 2𝑏 𝑛 + 𝑚 = 2(𝑎 + 𝑏) let 𝑐=𝑎+𝑏 𝑐∈Z
𝑛 + 𝑚 = 2𝑐
(𝑐∈Z)∧ 𝑛+𝑚 =2𝑐 ∃𝑘 𝑘∈Z∧ 𝑛+𝑚=2𝑘
by Simplification, 1
by Definition of Even, 2
by Existential Instantation, 3 by Simplification, 4
by Simplification, 1
by Definition of Even, 6
by Existential Instantation, 7 by Simplification, 8
by Closure of Integers under Addition, 12 11
by Conjunction, 13, 14
by Existential Generalization, 15 by Definition of Even, 16

Structural Induction (with a Branching Program)
How would you Prove (with Induction) that the Sum of 𝑛 Even Numbers is, itself, an Even Number?
What is (are) the Base Cases? What is the Inductive Assumption?

Structural Induction (with a Branching Program)
How would you Write a Function for “Filtering” the Even Elements from a List of Integers?
selectEven :: [Int] -> [Int]

Structural Induction (with a Branching Program) What is the Knowledge Base?
i.e., What Properties will we Use for this Proof?

Structural Induction (with a Branching Program)
the Conjecture to be Proven is that the Sum of the List that Results from selectEven is an Even Number
i.e., Proving that this Works is the Same As Proving sum (selectEven x) is Even

Structural Induction (with a Branching Program) first Prove the Base Case…
What is the Base Case? …then Assume…
What is the Inductive Assumption? …in order To Prove…

Structural Induction (with a Branching Program) first Prove the Base Case…
sum (selectEven []) is Even …then Assume…
sum (selectEven t) is Even …in order To Prove…

Structural Induction (with a Branching Program)
What is the Knowledge Base?
i.e., What Properties will we Use for this Proof?
Knowledge Base
sum [] = 0
sum (h:t) = h + sum t
selectEven [] = []
selectEven uses Guards, so some Properties in the Knowledge Base will only be Available in Certain Cases

Structural Induction (with a Branching Program)
“When I’m at work, I answer emails. When I’m at home, I answer emails.
I am always either at work or at home. Therefore I am always answering emails.”
𝑝∨𝑟 𝑝→𝑞 𝑟→𝑞
this is an Example of Disjunction Elimination since Both (i.e., All) Cases 𝒑 and 𝒓 Entail 𝒒 𝒒 can be Concluded

Structural Induction (with a Branching Program)
What is the Knowledge Base?
i.e., What Properties will we Use for this Proof?
Knowledge Base
sum [] = 0
sum (h:t) = h + sum t
selectEven [] = []
Case: mod h 2 == 0 selectEven(h:t) = h : selectEven t
Case: otherwise selectEven(h:t) = selectEven t
sum (selectEven t) is Even

Structural Induction (with a Branching Program)
Knowledge Base
sum [] = 0
sum (h:t) = h + sum t
selectEven [] = []
Case: mod h 2 == 0 selectEven(h:t) = h : selectEven t
Case: otherwise selectEven(h:t) = selectEven t
Prove: sum (selectEven []) is Even

Structural Induction (with a Branching Program)
Knowledge Base
sum [] = 0
sum (h:t) = h + sum t
selectEven [] = []
Case: mod h 2 == 0 selectEven(h:t) = h : selectEven t
Case: otherwise selectEven(h:t) = selectEven t
sum (selectEven []) is Even
sum [] is Even
by E1 by S1

Structural Induction (with a Branching Program)
Knowledge Base
sum [] = 0
sum (h:t) = h + sum t
selectEven [] = []
Case: mod h 2 == 0 selectEven(h:t) = h : selectEven t
Case: otherwise selectEven(h:t) = selectEven t
sum (selectEven t) is Even
Prove: sum (selectEven (h:t)) is Even

Structural Induction (with a Branching Program)
Knowledge Base
sum [] = 0
sum (h:t) = h + sum t
selectEven [] = []
Case: mod h 2 == 0 selectEven(h:t) = h : selectEven t
Case: otherwise selectEven(h:t) = selectEven t
sum (selectEven t) is Even
Prove: Case 1:
sum (selectEven (h:t)) is Even
mod h 2 == 0
sum (h : selectEven t) is Even
h + sum (selectEven t) is Even
Even + sum (selectEven t) Even + Even
E2a is available
by Definition by IA

Structural Induction (with a Branching Program)
Knowledge Base
sum [] = 0
sum (h:t) = h + sum t
selectEven [] = []
Case: mod h 2 == 0 selectEven(h:t) = h : selectEven t
Case: otherwise selectEven(h:t) = selectEven t
sum (selectEven t) is Even
Prove: Case 2:
sum (selectEven (h:t)) is Even
sum (selectEven t) is Even
E2b is available
by E2b by IA