Assignment #2: recurrences & correctness

CSC236
Assignment #2: recurrences & correctness

1. In lecture, we used the following recurrence to represent the steps taken
by an implementation of mergesort on a list of size n:
T0(n) = (
1 if n = 1
n + 2T0(n=2) if n > 1
(This recurrence assumes n is a power of 2, hence the absence of  oor and
ceiling. You may maintain this assumption throughout this question.)
In reality, some implementations of divide-and-conquer algorithms stop
the recursion before the input size becomes trivial. For example, a programmer may  nd that their mergesort implementation ends up running
a bit faster if they stop recursing when the list size is less than 10, sorting
these small lists using selection sort.
Consider the following recurrence, which models this scenario:
T(n) = (
c if n  k
n + 2T(n=2) if n > k
k; c 2 N
+ are  xed constants, where k represents the largest problem size
which is solved non-recursively, and c represents the cost of solving these
small problems.
(a) Use unwinding1
to  nd a closed form for T(n) when n  k. (You do
1Logistical note: If you wish to use tree diagrams for the unwinding portions of this question
(parts (a) and (c)), you are welcome to include scanned hand-drawn images, or diagrams
generated using other software. See this chapter of the LATEXWikibook for information on including images in LATEXdocuments. You may also describe the solution tree without explicitly
drawing it (a table may be helpful).
1
not need to prove that your closed form is correct, but it should be
clear how you arrived at it.)
(b) What is the big- complexity of T(n)? Does it depend on k? Brie y
justify your answer (no proof required). You may not assume n  k
for this part. Do not use the master theorem.
(c) Rather than assigning a  xed cost to the n  k case, it may be more
realistic to use a function of n, since there are a range of input sizes
which are handled non-recursively. Since selection sort is a (n
2
)
algorithm, we'll de ne our new recurrence T
0
(n) to be
T
0
(n) = (
n
2
if n  k
n + 2T
0
(n=2) if n > k
Find a closed form for T
0
(n) for n  k, and show how you got there.
Rather than unwinding from scratch, you may  nd it simpler to build
on your work from part (a).
(d) Is T
0
(n) 2 (T(n))? Why or why not? Brie y justify your answer.
As in part (b), you may not assume n  k. Do not use the master
theorem.
2. Our boss has tasked us with writing a program to  nd the unique maximum of a non-empty list of positive integers. If there is no unique maximum, our program should signal this by returning a negative number. For
example, on input [5, 2, 1, 2], our algorithm should return 5. Given
[2, 1, 2], we may return -1, -2, -236, or any other negative number.
Below is our  rst attempt to solve this problem.2
1 def umax ( A ) :
2 if len( A ) == 1:
3 return A [0]
4 head = A [0]
5 tail = A [1:]
6 tmax = umax ( tail )
7 if head == tmax :
8 return -1
9 elif head > tmax :
10 return head
11 else :
12 return tmax
(a) Based on the informal speci cation above, write precise pre- and
post-conditions for umax. Your postcondition should use symbolic
2You can download the code for this question from http://www.cs.toronto.edu/~colin/
236/W20/assignments/umax.py
2
notation rather than restating the English description above (\ nd
the unique maximum..."). The following postcondition was used in
lecture for the function max, which found the (not necessarily unique)
maximum of a list. It may be a useful starting point:
max(A) = x where (9j 2 N; A[j] = x)^(8i 2 N; i < len(A) =) A[i]  x)
You may  nd it helpful to formally de ne `helper' functions or predicates, as is done in question 3.
(b) The given Python code above has a bug. Demonstrate the bug by
 nding a value of A which meets the precondition, where umax misbehaves. For the value of A that you  nd, you should state the
expected behaviour (according to your postcondition) and how it
di ers from the function's actual behaviour on that input.
(c) Consider our second draft of the function umax below:
1 def umax ( A ) :
2 if len( A ) == 1:
3 return A [0]
4 head = A [0]
5 tail = A [1:]
6 tmax = umax ( tail )
7 if head == tmax :
8 return -1 * head
9 elif head > abs( tmax ) :
10 return head
11 else :
12 return tmax
Prove that this function is correct with respect to the speci cations
you devised in part (a).
3. The function maj takes as input a list of natural numbers and, if the
list has a majority element (one that appears more often than all other
elements combined), it returns that element.3 For example maj([1, 3,
3, 2, 3]) returns 3.4
1 def R ( A ) :
2 B = []
3 i = 0
4 while i < len( A ) :
5 a = A [ i ]
6 b = A [( i +1) % len( A ) ]
3Note that the function's behaviour is unde ned if the input list does not have a majority
element. i.e. the presence of a majority element is a precondition of maj.
4You can download the code for this question from http://www.cs.toronto.edu/~colin/
236/W20/assignments/maj.py
3
7 if a == b :
8 B . append ( a )
9 i += 1
10 return B
11
12 def maj ( A ) :
13 prev = A
14 curr = R ( A )
15 while len( curr ) != len( prev ) :
16 prev = curr
17 curr = R ( curr )
18 return curr [0]
Prove that maj is correct.
To aid you on your quest, the appendix below contains some de nitions
that you may  nd useful in your proof, as well as a proof of Theorem 1.1,
which, roughly speaking, says that every element x in R(A) corresponds
to an [x; x] pair in A (with the twist that pairs can \wrap around" from
the end of the list to the front).
The A2 starter .tex source also includes the same de nitions and a restatement of Theorem 1.1, which you may use in your proof. For brevity,
the proofs of 1.1 and the associated helper lemmas are omitted. (You're
unlikely to need to reuse these lemmas - they're provided here only as
optional reading.)
You can download the .tex source for the appendix, if you'd like to emulate the commands used to generate numbered theorems/lemmas, and
refer back to them.
Warning: This proof is both conceptually challenging and long (and the allocation of marks will re ect this). Count on it taking signi cantly longer
than the other two questions. I recommend initially focusing on breaking the problem down into smaller pieces. We will allocate a signi cant
number of marks for identifying an appropriate set of facts (invariants,
postconditions, etc.) which link together to form a proof of the correctness of maj. If you can't prove a particular fact in the chain, simply state
it, and assume it in the remainder of your proof.5
5The number of marks you will earn in this scenario will depend on the magnitude of the
assumption. For example, if you simply assume the partial correctness of maj, your proof
will earn few marks. On the other hand, if you have a nearly complete proof of the partial
correctness of maj which uses one very speci c unproven assumption, you may earn most of
the marks.
4
1 Appendix: Q3 starting point
1.1 Definitions
We will begin by introducing some formally de ned functions, predicates,
and other notation (along with informal English descriptions) which capture some useful concepts. (You are welcome to introduce additional such
de nitions in your own proof.)
We will use N

to denote the set of lists of natural numbers. Each of the
functions below takes as its  rst argument a list A 2 N

.
COUNT(A; x): jfi 2 N j A[i] = xgj
i.e. the number of occurrences of x in list A
SUCC(A; i) : (
0 if i = len(A)  1
i + 1 if i < len(A)  1
i.e. the `next' index in list A after index i, treating A as
a circular list (with the last index `wrapping around' back to
index 0). Not de ned if i  len(A).
PAIRS(A; x): jfi 2 N j A[i] = A[SUCC(A; i)] = xgj
i.e. the number of [x; x] pairs in list A, again treating A as
circular
ADVANTAGE(A; x): COUNT(A; x)  len(A)=2
MAJORITY(A; x): ADVANTAGE(A; x) > 0
i.e. x is the majority element of A
1.2 R counts are pair counts
This section proves a theorem about a postcondition of the function R.
You may use this theorem in your proof. For the purposes of answering
question 3, you do not need to read or understand the proof of Theorem 1.1
that follows. However, you may  nd it useful as an example to model your
proof on, in terms of content, organization (notice how we take a major
result and break it down into several digestible sub-proofs), and level of
rigour.
Theorem 1.1 (R \correctness"). Given any A 2 N

, R(A) terminates and
returns a list of natural numbers B such that 8x 2 N; COUNT(B; x) =
PAIRS(A; x)
We will prove this theorem in pieces,  rst proving a loop invariant for
R, then proving that R terminates, and  nally proving that termination
implies the postcondition above.
For our loop invariant, we introduce the following function, PPAIRS,
which counts the pairs in a pre x of a list:
PPAIRS(A; x; k): jfi 2 N j i < k ^ A[i] = A[SUCC(A; i)] = xgj
i.e. the number of x pairs in a length k pre x of A. (Note that
we use A's successor function, rather than one speci c to the
pre x A[: k]. This means we are allowed to `peek' ahead to the
k + 1th element of A, if it exists, rather than wrapping around
to the beginning of the pre x.
Lemma 1.2. PAIRS(A; x) = PPAIRS(A; x; len(A)).
Proof. When k = len(A), the i < k condition in the de nition of PPAIRS
does not exclude any valid indices of A, so the de nitions of PAIRS and
PPAIRS become equivalent.
Lemma 1.3 (R loop invariant). The following are all true at the end of
the jth iteration of R's while loop (if it occurs), when A is a list of
natural numbers:
(a) ij  len(A)
(b) 8x 2 N; COUNT(Bj ; x) = PPAIRS(A; x; ij )
(c) Bj contains only natural numbers
Proof. Base Case: Before the  rst iteration, i = 0, so (a) holds. B0 = [ ],
so (c) trivially holds. (b) holds because, by de nition, COUNT([ ]; x) and
PPAIRS(A; x; 0) are 0 for any x and A.
Inductive Step: Assume that the invariant holds at the end of the jth
iteration, and assume that the code runs for a j + 1th iteration.
By the while loop condition (line 4), ij < len(A), so it follows that ij +1 
len(A) ((a)).
Either Bj+1 = Bj , or line 8 is reached and Bj+1 di ers from Bj by the
addition of element aj+1 = A[ij ] 2 N. In either case, (c) is satis ed.
It remains to show (b). Let x 2 N, and consider

c = COUNT(Bj+1; x)  COUNT(Bj ; x)

p = PPAIRS(A; x; ij+1)  PPAIRS(A; x; ij )
= PPAIRS(A; x; ij + 1)  PPAIRS(A; x; ij )
By the code (lines 7-8), we can see
c is 1 if aj+1 = bj+1 = x, and 0
otherwise.
By the de nition of PPAIRS, we can see that
p is 1 if A[ij ] = A[SUCC(A; ij )] =
x, and 0 otherwise. By line 5, aj+1 = A[ij ]. By line 6 and the de nition
of SUCC, bj+1 = A[SUCC(A; ij )]. Therefore
c =
p. Since (b) holds at
the beginning of the iteration, and for arbitrary x, the change in the LHS
and the RHS (relative to the values at the beginning of the iteration) is
identical, it follows that (b) holds at the end of the iteration.
Lemma 1.4 (R termination). R terminates on any A 2 N

Proof. Let qj = len(A)  ij be a quantity associated with each loop iteration j. By Lemma 1.3 (a), qj 2 N. By line 9, qj+1 = qj  1. Thus
q0; q1; q2; : : : is a decreasing sequence of natural numbers, and therefore
 nite. Therefore, R terminates.
We are now ready to prove the postcondition of R given in Theorem 1.1.
Proof of 1.1. Let A be an arbitrary list. By Lemma 1.4 the loop on line
4 terminates at the end of some iteration, call it j. By the loop condition,
ij  len(A). By Lemma 1.3 (a) ij  len(A). Therefore ij = len(A).
By line 10, we return Bj . By 1.3, we have that 8x 2 N
COUNT(Bj ; x) = PPAIRS(A; x; ij )
= PPAIRS(A; x; len(A))
= PAIRS(A; x) # by Lemma 1.2
Also, by 1.3, we know that Bj contains only natural numbers.