CS代写 COMP302: Programming Languages and Paradigms

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