COMP302: Programming Languages and Paradigms
Prof. (Sec 01) Francisco Ferreira (Sec 02)
School of Computer Science Mc
Copyright By PowCoder代写 加微信 powcoder
Week 2-1, Fall 2017
Functional Tidbit: Prove All Things!
Anybody knows where this is on campus?
COMP302: Programming Languages and Paradigms 2 / 13
Let’s prove some stuff!
COMP302: Programming Languages and Paradigms 3 / 13
Warm Up: Lookup
Write a function lookup: ’a -> (’a * ’b) list -> ’b option. Given a key k of type ’a and a list l of key-value pairs, return the corresponding value v in l (if it exists).
COMP302: Programming Languages and Paradigms 4 / 13
Write a function insert which given a key k and a value v and an ordered list l of type (’a * ’b) list it inserts the key-value pair (k,v) into the list l preserving the order.
insert (3,”a”) [(2,”b”) ; (7, “c”)] =⇒∗ [(2, “b”); (3, “ab”); (7, “c”)]
COMP302: Programming Languages and Paradigms 5 / 13
Write a function insert which given a key k and a value v and an ordered list l of type (’a * ’b) list it inserts the key-value pair (k,v) into the list l preserving the order.
insert (3,”a”) [(2,”b”) ; (7, “c”)] =⇒∗ [(2, “b”); (3, “ab”); (7, “c”)]
What is the relationship between lookup and insert?
COMP302: Programming Languages and Paradigms
Write a function insert which given a key k and a value v and an ordered list l of type (’a * ’b) list it inserts the key-value pair (k,v) into the list l preserving the order.
insert (3,”a”) [(2,”b”) ; (7, “c”)] =⇒∗ [(2, “b”); (3, “ab”); (7, “c”)]
What is the relationship between lookup and insert?
lookup k (insert k v l) returns Some v
COMP302: Programming Languages and Paradigms
How to prove it?
COMP302: Programming Languages and Paradigms 6 / 13
How to prove it?
Step 1: We need to understand how programs are executed (operational semantics)
COMP302: Programming Languages and Paradigms 6 / 13
How to prove it?
Step 1: We need to understand how programs are executed (operational semantics)
expression e evaluates in multiple steps to the value v. (Big-Step)
expression e evaluates in one steps to expression e′. (Small-Step (single))
expression e evaluates in multiple steps to expression e′ (Small-Step (multiple)).
COMP302: Programming Languages and Paradigms
How to prove it?
Step 1: We need to understand how programs are executed (operational semantics)
expression e evaluates in multiple steps to the value v. (Big-Step)
expression e evaluates in one steps to expression e′. (Small-Step (single))
expression e evaluates in multiple steps to expression e′ (Small-Step (multiple)).
Foralll,v,k,lookup k (insert k v l)=⇒∗ Some v
COMP302: Programming Languages and Paradigms
How to prove it?
Step 2: How to reason inductively about lists?
COMP302: Programming Languages and Paradigms 7 / 13
How to prove it?
Step 2: How to reason inductively about lists? Analyze their structure!
COMP302: Programming Languages and Paradigms 7 / 13
How to prove it?
Step 2: How to reason inductively about lists? Analyze their structure!
The recipe …
To prove a property P(l) holds about a list l
Base Case:
Step Case:
l=[] P([]) holds
Assume the property P holds for lists smaller than l.
P(x::xs) holds
COMP302: Programming Languages and Paradigms
Show the property P holds for the original list l.
Let’s prove something
let rec lookup k l = match l with | [] -> None
| (k’,v) :: t ->
if k = k’ then Some v else lookup k t
let rec insert (k,v) l = match l with | [] -> [(k,v)]
| ((k’,v’) as h) :: t ->
if k = k’ then (k,v)::t else
if k < k’ then (k,v)::l else h::insert (k,v) t
1 2 3 4 5 6 7 8 9
10 11 12 13
COMP302: Programming Languages and Paradigms
Theorem: For all l, v, k, lookup k (insert (k,v) l) =⇒∗ Some v
Let’s prove something
let rec lookup k l = match l with | [] -> None
| (k’,v) :: t ->
if k = k’ then Some v else lookup k t
let rec insert (k,v) l = match l with | [] -> [(k,v)]
| ((k’,v’) as h) :: t ->
if k = k’ then (k,v)::t else
if k < k’ then (k,v)::l else h::insert (k,v) t
1 2 3 4 5 6 7 8 9
10 11 12 13
COMP302: Programming Languages and Paradigms
Theorem: For all l, v, k, lookup k (insert (k,v) l) =⇒∗ Some v
Lessons to take away
• State what you are doing induction on.
Proof by structural induction in the list l.
COMP302: Programming Languages and Paradigms 9 / 13
Lessons to take away
• State what you are doing induction on.
• Consider the different cases!
Proof by structural induction in the list l.
For lists, there are two cases – either l = [] or l = h::t
COMP302: Programming Languages and Paradigms 9 / 13
Lessons to take away
• State what you are doing induction on.
• Consider the different cases!
• State your induction hypothesis!
Proof by structural induction in the list l.
For lists, there are two cases – either l = [] or l = h::t
IH: For all v, k, lookup insert (k,v) t) ⇓ Some v
COMP302: Programming Languages and Paradigms 9 / 13
Lessons to take away
• State what you are doing induction on.
• Consider the different cases!
• State your induction hypothesis!
• Justify your evaluation / reasoning steps by
- Referring to evaluation of a given program
- The induction hypothesis
- Lemmas / Properties (such as associativity, commutativity, etc.)
Proof by structural induction in the list l.
For lists, there are two cases – either l = [] or l = h::t
IH: For all v, k, lookup insert (k,v) t) ⇓ Some v
COMP302: Programming Languages and Paradigms
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com