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

Advanced Structural Induction

Copyright © 2018 by . All Rights Reserved.

Learning Outcomes

Copyright By cscodehelp代写 加微信 cscodehelp

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:[])

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)

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

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) 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 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

Prove: sum (selectEven []) 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 []) is Even

sum [] is Even

Copyright © 2018 by . All Rights Reserved.

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

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代考 加微信: cscodehelp QQ: 2235208643 Email: kyit630461@163.com