程序代写代做代考 C Java algorithm graph data structure go ocaml c++ Thinking Inductively

Thinking Inductively
CSI 3120
Amy Felty University of Ottawa
slides copyright 2017, 2018 David Walker, Amy Felty permission granted to reuse these slides for non-commercial educational purposes

A value v has type t option if it is either: – the value None, or
– a value Some v’, and v’ has type t
Options
Options can signal there is no useful result to the computation
Example: we look up a value in a hash table using a key.
– If the key is present, return Some v where v is the associated value – If the key is not present, we return None
2

Slope between two points
a
type point = float * float
let slope (p1:point) (p2:point) : float =
(x2, y2)
(x1, y1)
c
b
3

Slope between two points
a
type point = float * float
(x2, y2)
let slope (p1:point) (p2:point) : float =
let (x1,y1) = p1 in
let (x2,y2) = p2 in
deconstruct tuple
(x1, y1)
c
b
4

Slope between two points
a
type point = float * float
(x2, y2)
let slope (p1:point) (p2:point) : float =
let (x1,y1) = p1 in
let (x2,y2) = p2 in
let xd = x2 -. x1 in
if xd != 0.0 then
(y2 -. y1) /. xd
avoid divide by zero
else ???
what can we return?
(x1, y1)
c
b
5

Slope between two points
a
type point = float * float
(x2, y2)
let slope (p1:point) (p2:point) : float option =
let (x1,y1) = p1 in
let (x2,y2) = p2 in
let xd = x2 -. x1 in
if xd != 0.0 then
???
we need an option type as the result type
else
???
(x1, y1)
c
b
6

Slope between two points
a
type point = float * float
(x2, y2)
let slope (p1:point) (p2:point) : float option =
let (x1,y1) = p1 in
let (x2,y2) = p2 in
let xd = x2 -. x1 in
if xd != 0.0 then
Some ((y2 -. y1) /. xd)
else
None
(x1, y1)
c
b
7

Slope between two points
a
type point = float * float
(x2, y2)
let slope (p1:point) (p2:point) : float option =
let (x1,y1) = p1 in
let (x2,y2) = p2 in
let xd = x2 -. x1 in
if xd != 0.0 then
(y2 -. y1) /. xd
else
None
Has type float
Can have type float option
(x1, y1)
c
b
8

Slope between two points
a
type point = float * float
(x2, y2)
let slope (p1:point) (p2:point) : float option =
let (x1,y1) = p1 in
let (x2,y2) = p2 in
let xd = x2 -. x1 in
if xd != 0.0 then
doubly WRONG: result does not match declared result
(y2 -. y1) /. xd
else
None
Has type float
(x1, y1)
c
b
10

Remember the typing rule for if
if e1 : bool
and e2 : t and e3 : t (for some type t) then if e1 then e2 else e3 : t
Returning an optional value from an if statement:
if … then
None : t option
else
Some ( … ) : t option
11

How do we use an option?
slope : point -> point -> float option
returns a float option
12

How do we use an option?
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit =
13

How do we use an option?
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit =
slope p1 p2
returns a float option;
to print we must discover if it is None or Some
14

How do we use an option?
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit =
match slope p1 p2 with
15

How do we use an option?
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit =
match slope p1 p2 with
Some s ->
| None ->
There are two possibilities
Vertical bar separates possibilities
16

How do we use an option?
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit =
match slope p1 p2 with
Some s ->
| None ->
The “Some s” pattern includes the variable s The object between | and -> is called a pattern
17

How do we use an option?
slope : point -> point -> float option
let print_slope (p1:point) (p2:point) : unit =
match slope p1 p2 with
Some s ->
print_string (“Slope: ” ^ string_of_float s)
| None ->
print_string “Vertical line.\n”
18

•
Steps to writing functions over typed data:
•
For option types:
Writing Functions Over Typed Data
1. Write down the function and argument names
2. Write down argument and result types
3. Write down some examples (in a comment)
4. Deconstruct input data structures
5. Build new output values
6. Clean up by identifying repeated patterns
when the input has type t option, deconstruct with:
when the output has type t option, construct with:
match … with
| None -> …
| Some s -> …
Some (…) None
19

MORE PATTERN MATCHING
20

Recall the Distance Function
type point = float * float
let distance (p1:point) (p2:point) : float =
let square x = x *. x in
let (x1,y1) = p1 in
let (x2,y2) = p2 in
sqrt (square (x2 -. x1) +. square (y2 -. y1))
;;
(x2, y2) is an example of a pattern – a pattern for tuples.
So let declarations can contain patterns just like match statements
The difference is that a match allows you to consider multiple different data shapes
22

Recall the Distance Function
type point = float * float
let distance (p1:point) (p2:point) : float =
let square x = x *. x in
match p1 with
| (x1,y1) ->
;;
let (x2,y2) = p2 in
sqrt (square (x2 -. x1) +. square (y2 -. y1))
There is only 1 possibility when matching a pair
23

;;
Recall the Distance Function
type point = float * float
let distance (p1:point) (p2:point) : float =
let square x = x *. x in
match p1 with
| (x1,y1) ->
match p2 with
| (x2,y2) ->
sqrt (square (x2 -. x1) +. square (y2 -. y1))
We can nest one match expression inside another.
(We can nest any expression inside any other, if the expressions have the right types)
24

type point = float * float
Complex Patterns we built a pair of pairs
let distance (p1:point) (p2:point) : float =
let square x = x *. x in
match (p1, p2) with
| ((x1,y1), (x2, y2)) ->
sqrt (square (x2 -. x1) +. square (y2 -. y1))
;;
Pattern for a pair of pairs: ((variable, variable), (variable, variable)) All the variable names in the pattern must be different.
25

type point = float * float
Complex Patterns we built a pair of pairs
let distance (p1:point) (p2:point) : float =
let square x = x *. x in
match (p1, p2) with
| (p3, p4) ->
;;
let (x1, y1) = p3 in
let (x2, y2) = p4 in
sqrt (square (x2 -. x1) +. square (y2 -. y1))
A pattern must be consistent with the type of the expression in between match … with
We use (p3, p4) here instead of ((x1, y1), (x2, y2))
26

Pattern-matching in function parameters
type point = float * float
let distance ((x1,y1):point) ((x2,y2):point) : float =
let square x = x *. x in
sqrt (square (x2 -. x1) +. square (y2 -. y1))
;;
Function parameters are patterns too!
27

What’s the best style?
let distance (p1:point) (p2:point) : float =
let square x = x *. x in
let (x1,y1) = p1 in
let (x2,y2) = p2 in
sqrt (square (x2 -. x1) +. square (y2 -. y1))
let distance ((x1,y1):point) ((x2,y2):point) : float =
let square x = x *. x in
sqrt (square (x2 -. x1) +. square (y2 -. y1))
Either of these is reasonably clear and compact.
Code with unnecessary nested matches/lets is particularly ugly to read.
28

What’s the best style?
let distance (x1,y1) (x2,y2) =
let square x = x *. x in
sqrt (square (x2 -. x1) +. square (y2 -. y1))
Note that the types for tuples plus the tuple patterns are a little ugly/verbose, and they can be inferred from the operators used such as `+.’ … but for now in class, use the explicit type annotations.
29

Other Patterns
type point = float * float
(* returns a nearby point in the graph if one exists *)
nearby : graph -> point -> point option
let printer (g:graph) (p:point) : unit =
match nearby g p with
| None -> print_string “could not find one\n”
| Some (x,y) ->
;;
print_float x;
print_string “, “;
print_float y;
print_newline();
30

INDUCTIVE THINKING
32

Inductive Programming and Proving An inductive data type T is a data type defined by:
– a collection of base cases • that don’t refer to T
– a collection of inductive cases that build new values of type T from pre-existing data of type T
• thepre-existingdataisguarateedtobesmallerthanthenewvalues Programming principle:
– solve programming problem for base cases
– solve programming problem for inductive cases by calling function
recursively (inductively) on smaller data value Proving principle:
– prove program satisfies property P for base cases
– prove inductive cases satisfy property P assuming inductive calls on smaller data values satisfy property P
33

LISTS: AN INDUCTIVE DATA TYPE
34

Lists are Recursive Data
• In OCaml, a list value is:
– [ ] (the empty list)
– v :: vs (a value v followed by a shorter list of values vs)
Inductive Case
Base Case
35

Lists are Inductive Data
• In OCaml, a list value is:
– [ ] (the empty list)
– v :: vs (a value v followed by a shorter list of values vs)
• An example:
– 2::3::5::[]hastypeintlist
– isthesameas: 2::(3::(5::[])) – “::” is called “cons”
• An alternative syntax (“syntactic sugar” for lists): – [2; 3; 5]
– Butthisisjustashorthandfor2::3::5::[]. Ifyoueverget confused fall back on the 2 basic constructors: :: and []
36

• Typing rules for lists:
(1) [ ] may have any list type t list
(2)
ife1:tand e2:tlist then (e1 :: e2) : t list
Typing Lists
37

Typing Lists (1) [ ] may have any list type t list
• Typing rules for lists:
(2)
ife1:tand e2:tlist then (e1 :: e2) : t list
• More examples:
(1 + 2) :: (3 + 4) :: [ ]
: ?? :?? : ??
(2::[])::(5::6 ::[])::[] [ [2]; [5; 6] ]
38

Typing Lists (1) [ ] may have any list type t list
• Typing rules for lists:
(2)
ife1:tand e2:tlist then (e1 :: e2) : t list
• More examples:
(1 + 2) :: (3 + 4) :: [ ] : int list
(2::[])::(5::6 ::[])::[] :(intlist)list orjust intlistlist
[ [2]; [5; 6] ] : int list list
(Remember that the 3rd example is an abbreviation for the 2nd)
39

• What type does this have?
[ 2 ] :: [ 3 ]
Another Example
40

#
• What type does this have?
[ 2 ] :: [ 3 ]
int list
int list
Another Example
# [2] :: [3];;
Error: This expression has type int but an
expression was expected of type
int list
41

• What type does this have?
[ 2 ] :: [ 3 ]
int list
int list
Another Example
• What is a simple fix that makes the expression type check?
42

• What type does this have?
[ 2 ] :: [ 3 ]
int list
int list
Another Example
• What is a simple fix that makes the expression type check? Either: 2 :: [3] :intlist
Or: [ 2 ] :: [ [ 3 ] ] : int list list
43

Analyzing Lists
• Just like options, there are two possibilities when deconstructing lists. Hence we use a match with two branches
(* return Some v, if v is the first list element;
return None, if the list is empty *)
let head (xs : int list) : int option =
match xs with
| [] ->
| hd :: _ ->
we don’t care about the contents of the tail of the list so we use the underscore
45

Analyzing Lists
• Just like options, there are two possibilities when deconstructing lists. Hence we use a match with two branches
(* return Some v, if v is the first list element;
return None, if the list is empty *)
let head (xs : int list) : int option =
match xs with
| [] -> None
| hd :: _ -> Some hd
• This function isn’t recursive — we only extracted a small , fixed amount of information from the list — the first element
46

A more interesting example
(* Given a list of pairs of integers,
produce the list of products of the pairs
prods [(2,3); (4,7); (5,2)] == [6; 28; 10]
*)
47

A more interesting example
(* Given a list of pairs of integers,
produce the list of products of the pairs
prods [(2,3); (4,7); (5,2)] == [6; 28; 10]
*)
let rec prods (xs : (int * int) list) : int list =
match xs with
| [] ->
| (x,y) :: tl ->
49

Three Parts to Constructing a Function (1) Think about how to break down the input into cases:
let rec prods (xs : (int*int) list) : int list =
match xs with
|[]-> …
| (x,y) :: tl -> …
This assumption is called the Induction Hypothesis. It can be used it to prove your program correct.
(2) Assume the recursive call on smaller data is correct.
(3) Use the result of the recursive call to build correct answer.
let rec prods (xs : (int*int) list) : int list =
…
| (x,y) :: tl -> … prods tl …
55

*)
Another example: zip
(* Given two lists of integers,
return None if the lists are different lengths
otherwise stitch the lists together to create
Some of a list of pairs
zip [2; 3] [4; 5] == Some [(2,4); (3,5)]
zip [5; 3] [4] == None
zip [4; 5; 6] [8; 9; 10; 11; 12] == None
56

Another example: zip
let rec zip (xs : int list) (ys : int list)
: (int * int) list option =
57

Another example: zip
let rec zip (xs : int list) (ys : int list)
: (int * int) list option =
match (xs, ys) with
58

Another example: zip
let rec zip (xs : int list) (ys : int list)
: (int * int) list option =
match (xs, ys) with
| ([], []) ->
| ([], y::ys’) ->
| (x::xs’, []) ->
| (x::xs’, y::ys’) ->
59

Another example: zip
let rec zip (xs : int list) (ys : int list)
: (int * int) list option =
match (xs, ys) with
| ([], []) -> Some []
| ([], y::ys’) ->
| (x::xs’, []) ->
| (x::xs’, y::ys’) ->
60

Another example: zip
let rec zip (xs : int list) (ys : int list)
: (int * int) list option =
match (xs, ys) with
| ([], []) -> Some []
| ([], y::ys’) -> None
| (x::xs’, []) -> None
| (x::xs’, y::ys’) -> (x, y) :: zip xs’ ys’
is this ok?
62

match (xs, ys) with
| ([], []) -> Some []
| (x::xs’, y::ys’) ->
Another example: zip
let rec zip (xs : int list) (ys : int list)
: (int * int) list option =
(match zip xs’ ys’ with
None -> None
| Some zs -> Some ((x,y) :: zs))
| (_, _) -> None
Clean up.
Reorganize the cases.
Pattern matching proceeds in order.
66

A bad list example
let rec sum (xs : int list) : int =
match xs with
| hd::tl -> hd + sum tl
67

#
Characters 39-78:
..match xs with
A bad list example
let rec sum (xs : int list) : int =
match xs with
| hd::tl -> hd + sum tl
hd :: tl -> hd + sum tl..
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched: []
val sum : int list -> int =
68

INSERTION SORT
69

Recall Insertion Sort
• At any point during the insertion sort:
– some initial segment of the array will be sorted
– the rest of the array will be in the same (unsorted) order as it was originally
-5 -2 3 -4 10 6 7
sorted
unsorted
• At each step, take the next item in the array and insert it in order into the sorted portion of the list
-5 -4 -2 3 10 6 7
sorted
unsorted
71

Insertion Sort With Lists
• The algorithm is similar, except instead of one array, we will
maintain two lists, a sorted list and an unsorted list
list 1:
list 2:
-5 -2 3
-4 10 6 7
sorted
unsorted
• We’ll factor the algorithm:
– a function to insert into a sorted list
– a sorting function that repeatedly inserts
72

Insert
(* insert x in to sorted list xs *)
let rec insert (x : int) (xs : int list) : int list =
73

(* insert x in to sorted list xs *)
Insert
let rec insert (x : int) (xs : int list) : int list =
match xs with
| [] ->
| hd :: tl ->
a familiar pattern: analyze the list by cases
74

(* insert x in to sorted list xs *)
Insert
let rec insert (x : int) (xs : int list) : int list =
match xs with
| [] -> [x]
| hd :: tl ->
insert x into the empty list
75

(* insert x in to sorted list xs *)
Insert
let rec insert (x : int) (xs : int list) : int list =
match xs with
| [] -> [x]
| hd :: tl ->
if hd < x then hd :: insert x tl build a new list with: • hd at the beginning • the result of inserting x in to the tail of the list afterwards 76 (* insert x in to sorted list xs *) Insert let rec insert (x : int) (xs : int list) : int list = match xs with | [] -> [x]
| hd :: tl ->
if hd < x then hd :: insert x tl else x :: xs put x on the front of the list, the rest of the list follows 77 type il = int list insert : int -> il -> il
(* insertion sort *)
let rec insert_sort(xs : il) : il =
Insertion Sort
78

type il = int list
insert : int -> il -> il
(* insertion sort *)
let rec insert_sort(xs : il) : il =
Insertion Sort
let rec aux (sorted : il) (unsorted : il) : il =
in
79

type il = int list
insert : int -> il -> il
(* insertion sort *)
let rec insert_sort(xs : il) : il =
Insertion Sort
let rec aux (sorted : il) (unsorted : il) : il =
in
aux [] xs
80

type il = int list
insert : int -> il -> il
(* insertion sort *)
let rec insert_sort(xs : il) : il =
Insertion Sort
let rec aux (sorted : il) (unsorted : il) : il =
match unsorted with
| [] ->
| hd :: tl ->
in
aux [] xs
81

type il = int list
insert : int -> il -> il
(* insertion sort *)
let rec insert_sort(xs : il) : il =
Insertion Sort
let rec aux (sorted : il) (unsorted : il) : il =
match unsorted with
| [] -> sorted
| hd :: tl -> aux (insert hd sorted) tl
in
aux [] xs
82

A SHORT JAVA RANT
83

public class Pair {
public class User {
}
public int x;
public int y;
public Pair swap (Pair p1) {
Pair p2 =
Definition and Use of Java Pairs
public Pair (int a, int b) {
x = a;
new Pair(p1.y, p1.x);
return p2;
y = b; }}
}
What could go wrong?
84

public class Pair {
public class User {
}
public int x;
public int y;
public Pair swap (Pair p1) {
Pair p2 =
public Pair (int a, int b) {
x = a;
new Pair(p1.y, p1.x);
return p2;
y = b; }}
}
A Paucity of Types
The input p1 to swap may be null and we forgot to check. Java has no way to define a pair data structure that is just a pair.
How many students in the class have seen an accidental null pointer exception thrown in their Java code?
85

From Java Pairs to OCaml Pairs
In OCaml, if a pair may be null it is a pair option:
type java_pair = (int * int) option
86

From Java Pairs to OCaml Pairs
In OCaml, if a pair may be null it is a pair option:
type java_pair = (int * int) option
And if you write code like this:
let swap_java_pair (p:java_pair) : java_pair = let (x,y) = p in
(y,x)
# … Characters 91-92:
let (x,y) = p in (y,x);;
You get a helpful error message like this:
^
Error: This expression has type java_pair = (int * int) option
but an expression was expected of type ‘a * ‘b
88

From Java Pairs to OCaml Pairs
type java_pair = (int * int) option
And what if you were up late trying to finish your assignment and you accidentally wrote the following statement?
let swap_java_pair (p:java_pair) : java_pair = match p with
| Some (x,y) -> Some (y,x)
..match p with
| Some (x,y) -> Some (y,x)
OCaml to the rescue!
Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: None
90

From Java Pairs to OCaml Pairs
type java_pair = (int * int) option
And what if you were up late trying to finish your assignment and you accidentally wrote the following statement?
let swap_java_pair (p:java_pair) : java_pair = match p with
| Some (x,y) -> Some (y,x)
An easy fix!
let swap_java_pair (p:java_pair) : java_pair = match p with
| None -> None
| Some (x,y) -> Some (y,x)
91

From Java Pairs to OCaml Pairs
Moreover, your pairs are probably almost never null!
Defensive programming & always checking for null can be annoying.
92

From Java Pairs to OCaml Pairs
There just isn’t always some “good thing” for a function to do when it receives a bad input, like a null pointer
In OCaml, all these issues disappear when you use the proper type for a pair and that type contains no “extra junk”
type pair = int * int
Once you know OCaml, it is hard to write swap incorrectly Your bullet-proof code is much simpler than in Java.
let swap (p:pair) : pair =
let (x,y) = p in (y,x)
93

Java has a paucity of types
OCaml has many more types
Summary of Java Pair Rant
– Thereisnotypetodescribejustthepairs
– Thereisnotypetodescribejustthetriples
– Thereisnotypetodescribethepairsofpairs – Thereisnotype…
– useoptionwhenthingsmaybenull
– donotuseoptionwhenthingsarenotnull
– OCamltypesdescribedatastructuresmoreprecisely
• programmershavefewercasestoworryabout
• entireclassesoferrorsjustgoaway
• typecheckingandpatternanalysishelppreventprogrammersfrom ever forgetting about a case
94

Java has a paucity of types
Summary of Java Pair Rant
– Thereisnotypetodescribejustthepairs
– Thereisnotypetodescribejustthetriples
– Thereisnotypetodescribethepairsofpairs – Thereisnotype…
OCaml has many more types
SCORE: OCAML 1, JAVA 0
– useoptionwhenthingsmaybenull
– donotuseoptionwhenthingsarenotnull
– ocamltypesdescribedatastructuresmoreprecisely
• programmershavefewercasestoworryabout
• entireclassesoferrorsjustgoaway
• typecheckingandpatternanalysishelppreventprogrammersfrom ever forgetting about a case
95

Java has a paucity of types
C, C++ Rant
– but at least when you forget something,
it throws an exception instead of silently going off the rails!
If you forget to check for null pointer in a C program,
– no type-check error at compile time
– no exception at run time
– it might crash right away (that would be best), or
– it might permit a buffer-overrun (or similar) vulnerability
96

Java has a paucity of types
Summary of C, C++ rant
– but at least when you forget something,
it throws an exception instead of silently going off the trolley!
If you forget to check for null pointer in a C program,
SCORE:
– no type-check error at compile time
– no excepOtioCnAatMrunLti1m,e JAVA 0, C -1
– it might crash right away (that would be best), or
– it might permit a buffer-overrun (or similar) vulnerability – so the hackers pwn you!
97

Example problems to practice
• Write a function to sum the elements of a list – sum[1;2;3]==>6
• Write a function to append two lists
– append [1;2;3] [4;5;6] ==> [1;2;3;4;5;6]
• Write a function to reverse a list – rev [1;2;3] ==> [3;2;1]
• Write a function to turn a list of pairs into a pair of lists – split [(1,2); (3,4); (5,6)] ==> ([1;3;5], [2;4;6])
• Write a function that returns all prefixes of a list – prefixes [1;2;3] ==> [[]; [1]; [1;2]; [1;2;3]]
• suffixes…
98

Related Posts