CS代考 COMP302: Programming Languages and Paradigms

COMP302: Programming Languages and Paradigms
Prof. (Sec 01) Francisco Ferreira (Sec 02)

School of Computer Science Mc

Week 3-1, Fall 2017

Functional Tidbit: Cake!
COMP302: Programming Languages and Paradigms 2 / 13

Functional Tidbit: Cake is tasty!
COMP302: Programming Languages and Paradigms 3 / 13

More on Structural Induction
COMP302: Programming Languages and Paradigms 4 / 13

Two programs: Do they compute the same value?
Program A (naive)
1 2 3 4 5 6 7 8
(* rev : ’a list -> ’a list *)
let rec rev l = match l with | [] -> []
| x::l -> (rev l) @ [x]
Program B (tail-recursive)
(* rev’ : ’a list -> ’a list *)
let rev’ l =
(* rev_tr : ’a list -> ’a list -> ’a list *) let rec rev_tr l acc = match l with
| [] -> acc
| h::t -> rev_tr t (h::acc)
rev_tr l []
COMP302: Programming Languages and Paradigms

Two programs: Do they compute the same value?
Program A (naive)
1 2 3 4 5 6 7 8
(* rev : ’a list -> ’a list *)
let rec rev l = match l with | [] -> []
| x::l -> (rev l) @ [x]
Theorem: For all lists l. rev l = rev’ l
Program B (tail-recursive)
(* rev’ : ’a list -> ’a list *)
let rev’ l =
(* rev_tr : ’a list -> ’a list -> ’a list *) let rec rev_tr l acc = match l with
| [] -> acc
| h::t -> rev_tr t (h::acc)
rev_tr l []
COMP302: Programming Languages and Paradigms

What to prove? – Finding the invariant!
Program A (naive)
1 2 3 4 5 6 7 8 9
(* rev : ’a list -> ’a list *)
let rec rev l = match l with | [] -> []
| x::l -> (rev l) @ [x]
What is the relationship between l, acc and rev_tr l acc?
Program B (tail-recursive)
(* rev’ : ’a list -> ’a list *)
let rev’ l =
(* rev_tr : ’a list -> ’a list -> ’a list *) let rec rev_tr l acc = match l with
| [] -> acc
| h::t -> rev_tr t (h::acc)
rev_tr l []
COMP302: Programming Languages and Paradigms

What to prove? – Finding the invariant!
Program A (naive)
1 2 3 4 5 6 7 8 9
(* rev : ’a list -> ’a list *)
let rec rev l = match l with | [] -> []
| x::l -> (rev l) @ [x]
For all l, acc, (rev l) @ acc ⇓ v and rev_tr l acc ⇓ v
Program B (tail-recursive)
(* rev’ : ’a list -> ’a list *)
let rev’ l =
(* rev_tr : ’a list -> ’a list -> ’a list *) let rec rev_tr l acc = match l with
| [] -> acc
| h::t -> rev_tr t (h::acc)
rev_tr l []
COMP302: Programming Languages and Paradigms

Theorem: For all l, acc,
length (rev_tr l acc) ⇓ v and length l + length acc ⇓ v.
We often simply write instead: For all l, acc,
length (rev_tr l acc) = length l + length acc
COMP302: Programming Languages and Paradigms 9 / 13

Can’t see the forest for the trees
COMP302: Programming Languages and Paradigms 10 / 13

Inductive definition of a binary tree
• The empty binary tree Empty is a binary tree
• Ifl andr arebinarytreesandv isavalueoftype’a
then Node(v, l, r) is a binary tree. • Nothing else is a binary tree.
COMP302: Programming Languages and Paradigms 11 / 13

Inductive definition of a binary tree
• The empty binary tree Empty is a binary tree
• Ifl andr arebinarytreesandv isavalueoftype’a
then Node(v, l, r) is a binary tree. • Nothing else is a binary tree.
How can we define a data type that describes binary trees?
COMP302: Programming Languages and Paradigms

Forest and trees
Example of a mutual recursive data type definition:
type ’a forest = Forest of (’a tree) list and ’a tree = Empty | Node of ’a * ’a forest
COMP302: Programming Languages and Paradigms 12 / 13

Remember the slice of cake?
Give an OCaml data type definition for cake!
COMP302: Programming Languages and Paradigms 13 / 13

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

Related Posts