代写代考 Advanced Structural Induction

Advanced Structural Induction
Copyright © 2018 by . All Rights Reserved.

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)
Copyright © 2018 by . All Rights Reserved.

Reading and Suggested Exercises
Copyright © 2018 by . All Rights Reserved.
Read the following Chapter(s): None

Structural Induction
How would you Write a Function for Computing the Length of List?
length :: [a] -> Int
Copyright © 2018 by . All Rights Reserved.

Structural Induction
length :: [a] -> Int length [] = 0
length (h:t) = 1 + length t
How would you Trace the following Evaluation? length [1, 2, 3]
Copyright © 2018 by . All Rights Reserved.

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 [3])
1 + (1 + (1 + length [])) 1 + (1 + (1 + 0))
To What are h and t Bound to at Each Stage? Copyright © 2018 by . All Rights Reserved.
Structural Induction

Structural Induction
How would you Write a Function for Concatenating Two Lists (without ++)?
concat :: [a] -> [a] -> [a]
Copyright © 2018 by . All Rights Reserved.

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]
Copyright © 2018 by . All Rights Reserved.

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 [3] [4, 5, 6]))
1 : (2 : (3 : (concat [3] [4, 5, 6]))) 1 : (2 : (3 : [4, 5, 6]))
To What are h and t Bound to at Each Stage? Copyright © 2018 by . All Rights Reserved.
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)
Copyright © 2018 by . All Rights Reserved.

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
the Assumption is the Induction Hypothesis Copyright © 2018 by . All Rights Reserved.

Structural Induction first Prove the Base Case…
What is the Base Case? …then Assume…
What is the Inductive Assumption? …in order To Prove…
What is the Inductive Case? Copyright © 2018 by . All Rights Reserved.

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)
Copyright © 2018 by . All Rights Reserved.

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
Copyright © 2018 by . All Rights Reserved.

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)
Copyright © 2018 by . All Rights Reserved.

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
Copyright © 2018 by . All Rights Reserved.
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)
Copyright © 2018 by . All Rights Reserved.

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.
Copyright © 2018 by . All Rights Reserved.
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
Copyright © 2018 by . All Rights Reserved.

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))
Why or Why Not? Copyright © 2018 by . All Rights Reserved.

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
Copyright © 2018 by . All Rights Reserved.

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) : [10]) 3 weird ((15 : [10]) 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
weird and average Functions for Computing Mean? Copyright © 2018 by . All Rights Reserved.

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
this is known as “Partial Correctness” Copyright © 2018 by . All Rights Reserved.

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))
Copyright © 2018 by . All Rights Reserved.

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
Copyright © 2018 by . All Rights Reserved.

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
Copyright © 2018 by . All Rights Reserved.

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
Copyright © 2018 by . All Rights Reserved.

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
Copyright © 2018 by . All Rights Reserved.

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 𝑛
is the Same As Proving (sum x) / (length x) Copyright © 2018 by . All Rights Reserved.

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…
What is the Inductive Case? Copyright © 2018 by . All Rights Reserved.

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))
Copyright © 2018 by . All Rights Reserved.

Structural Induction (with a Questionable Program) What is the Knowledge Base?
i.e., What Properties will we Use for this Proof?
Copyright © 2018 by . All Rights Reserved.

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
Copyright © 2018 by . All Rights Reserved.

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
Copyright © 2018 by . All Rights Reserved.

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)
Copyright © 2018 by . All Rights Reserved.
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?
Copyright © 2018 by . All Rights Reserved.

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))
Copyright © 2018 by . All Rights Reserved.

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
Copyright © 2018 by . All Rights Reserved.

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𝑘
Copyright © 2018 by . All Rights Reserved.

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
𝑛+𝑚 isEven Copyright © 2018 by . All Rights Reserved.
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?
Copyright © 2018 by . All Rights Reserved.

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]
Copyright © 2018 by . All Rights Reserved.

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
Copyright © 2018 by . All Rights Reserved.

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…
What is the Inductive Case? Copyright © 2018 by . All Rights Reserved.

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…
sum (selectEven (h:t)) is Even Copyright © 2018 by . All Rights Reserved.

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
Copyright © 2018 by . All Rights Reserved.

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
Copyright © 2018 by . All Rights Reserved.

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
Copyright © 2018 by . All Rights Reserved.

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
by © 2018 by . All Rights Reserved.

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
Copyright © 2018 by . All Rights Reserved.

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

Related Posts