assignment, you will go over some of the basic concepts we want you to learn in this course, including defining recursive functions and proving their correctness. We expect you to follow the methodology for defining a function, as shown in class.
1.1 Getting The Homework Assignment
The starter files for the homework assignment have been distributed through our git repos- itory, as usual.
1.2 Submitting The Homework Assignment
Submissions will be handled through Autolab, at
In preparation for submission, your hw/02 directory should contain a file named exactly
hw02.pdf containing your written solutions to the homework.
To submit your solutions, run make from the hw/02 directory (that contains a code folder and a file hw02.pdf). This should produce a file hw02.tar, containing the files that should be handed in for this homework assignment. Open the Autolab web site, find the page for this assignment, and submit your hw02.tar file via the “Handin your work” link.
The Autolab handin script does some basic checks on your submission: making sure that the file names are correct; making sure that no files are missing; making sure that your PDF is valid; making sure that your code compiles cleanly. Note that the handin script is not a grading script—a timely submission that passes the handin script will be graded, but will not necessarily receive full credit. You can view the results of the handin script by clicking the number (usually either 0.0 or 1.0) corresponding to the “check” section of your latest handin on the “Handin History” page. If this number is 0.0, your submission failed the check script; if it is 1.0, it passed.
Remember that your written solutions must be submitted in PDF format—we do not accept MS Word files or other formats.
Your hw02.sml file must contain all the code that you want to have graded for this assignment, and must compile cleanly. If you have a function that happens to be named the same as one of the required functions but does not have the required type, it will not be graded.
1.3 Due Date
This assignment is due on Tuesday, 10 September 2013 at 23:59 EST. Remember that you may use a maximum of one late day per assignment, and that you are allowed a total of three late days for the semester.
You must use the five step methodology discussed in class for writing functions, for every
function you write in this assignment. Recall the five step methodology:
- In the first line of comments, write the name and type of the function.
- In the second line of comments, specify via a REQUIRES clause any assumptions about the arguments passed to the function.
- In the third line of comments, specify via an ENSURES clause what the function com- putes (what it returns).
- Implement the function.
- Provide testcases, generally in the format
val <return value> = <function> <argument value>. For example, for the factorial function:
(* fact : int -> int
* REQUIRES: n >= 0
* ENSURES: fact(n) ==> n!
fun fact (0 : int) : int = 1
| fact (n : int) : int = n * fact(n-1) (* Tests: *)
val 1 = fact 0
val 720 = fact 6
The built-in function
real : int -> real
returns the real value corresponding to a given int input; for example, real 1 evaluates to 1.0. Conversely, the built-in function
trunc : real -> int
returns the integral part (intuitively, the digits before the decimal point) of its input; for example, trunc 3.9 evaluates to 3. Feel free to try these functions out in smlnj.
Once you understand these functions, you should solve the questions in this section in
your head, without first trying them out in smlnj. The type of mental reasoning involved in answering these questions should become second nature.
Task 2.1 (4%). Consider the following code fragment:
fun double (x : real) : real = x + x fun double (y : int) : int = y + y
fun doubleplus (z : real) : real = double (z + 1.0)
Does this typecheck? Briefly explain why or why not.
Task 2.2 (6%). For each of the following patterns, state what kinds of values of type int list can be matched to it successfully. For example, the pattern [ ] only matches the empty list and the pattern [true] matches no values of type int list.
(i) Pattern x::L
(ii) Pattern ::
(iii) Pattern x::(y::L) (iv) Pattern (x::y)::L (v) Pattern [x, y]
Task 2.3 (5%). For each of the following sets of values, give a single pattern that would match only with the values in the set. If such a pattern cannot be made, explain why.
(i) Lists of length 3
(ii) Lists of length 2 or 3 (iii) Non-empty lists of pairs
(iv) Pairs with both components being non-empty lists
Let Bindings In Lecture 2, we went over SML’s syntax for let-bindings. It is possible to write val declarations in the middle of other expressions with the syntax let … in … end.
Task 2.4 (8%). Consider the following code fragment (the line-numbers are for reference;
they are not part of the code itself ):
(1) val x : int = 3
(2) val temp : int = x + 1
(3) fun assemble (x : int, y : real) : int = (4) let val g : real = let val x : int = 2
(5) val m : real = 6.2 * (real x) (6) val x : int = 9001
(7) val y : real = m * y
(8) in y – m
(11) x + (trunc g) (12) end
(14) val z = assemble (x, 3.0)
Note that in the declaration of temp in line (2), the binding J x:3 K is introduced for the variable x in that line. The value of the binding is of type int.
(a) What binding (and type) does the declaration in line (4) introduce for the variable x?
Briefly explain why.
(b) What binding (and type) does the declaration in line (5) introduce for the variable m?
Briefly explain why.
(c) What binding (and type) does the declaration in line (6) introduce for the variable x?
Briefly explain why.
(d) What value does the expression assemble (x, 3.0) evaluate to in line (14)?
2.3 Evaluational and Equational Reasoning
It is important to understand the difference between expression evaluation using ⇒∗ and extensional equivalence (equational reasoning) using =. To test your understanding of each of these symbols and their definitions and properties, we ask you in this section to determine whether the following statements are extensionally equivalent and whether one expression evaluates to the next.
Task 2.5 (8%). For the following statements, state whether it is true or false (make sure to note which symbol is being used). Next, give enough detail to show that you understand what the notation means. This will involve using equational laws and equational reasoning, or evaluation rules and evaluational reasoning, as appropriate. Laws, rules, and examples of such reasoning were shown in class. You can consult the lecture notes for more examples.
(a) (fn x:int => x+(2-1)) = (fn x:int => x+1)
(b) (fn x:int => x+(2-1)) ⇒∗ (fn x:int => x+1)
Now look carefully at the following function, decimal, as shown in lecture:
fun decimal (n:int) : int list =
if n<10 then [n]
else (n mod 10) :: decimal(n div 10)
Remember, the symbols = and ⇒∗ for extensional equivalence and expression evaluation, respectively, have different meanings. With that in mind:
Task 2.6 (4%). Using equational reasoning (with the = symbol), show the following:
decimal (5 + 5) = [0, 1]
Do not use the ⇒∗ notation for evaluation. You must use equational laws about function application, substitution, and conditional expressions as shown in lecture. Give enough detail to show that you understand how to use these equational laws, making sure to only use an equation when it is applicable to the problem at hand. For example, the substitution law for function application requires that the argument expression is a value.
Task 2.7 (4%). Using evaluational reasoning (with the ⇒∗ symbol), show the following:
decimal (5 + 5) ⇒∗ [0, 1]
Do not use the equational reasoning that you used in the previous task. You must use evaluational facts as shown in lecture. Give enough detail to show that you understand how SML evaluates expressions, and make sure to clearly explain the order in which sub- expressions get evaluated.
3 Recursive Functions
3.1 Addition and Subtraction
The following function adds two natural numbers recursively by repeatedly adding 1:
(* add : int * int -> int
REQUIRES: x, y >= 0
ENSURES: add(x,y) = x+y
fun add (0 : int, y : int) : int = y
| add (x : int, y : int) : int = 1 + add(x-1, y)
(Recall that a natural number is a non-negative integer.)
In the next part, let us define a function leq : int * int -> bool that accepts a pair
(x, y) of two natural numbers x and y and returns true if x ≤ y and false otherwise.
Task 3.1 (5%). In hw02.sml, write and document a recursive function
leq : int * int -> bool
that satisfies the specification above. Your implementation has a specific set of restrictions, namely that it:
- must use recursion;
- can only decrement values by 1;
- must use only pattern-matching on integer values (no conditional expressions, no use of <, and no boolean case expressions!).
3.2 Going Halfway Forwards
A famous series in mathematics that can be used to represent one of Zeno’s paradoxes is of the following form:
X 1 1 1 1
+ + +
2 4 8
This series converges to the real value 1.0, because the “partial sum” of the first n terms of this series gets closer and closer to the value 1.0 as n gets larger. We will be exploring the partial sum of the first n terms in this series, which we will denote as Sn, for n ≥ 0:
Sn = X
Recall that, by definition, Pn
f (i) is 0 if n < k.
Task 3.2 (4%). What are S0, S1, S2, S3 ?
Task 3.3 (8%). In hw02.sml, write and document a recursive function
halfSum : int -> real
such that halfSum n calculates Sn for any natural number n. For this problem you may use any functions or operators you wish. In particular you may want to use the built-in function real discussed earlier in this assignment, although it is not crucial (there are other ways to write halfSum : ). Please only use recursion; do not look for a closed form for Sn. Instead, look for a way to compute Sn recursively.
Note: When testing your code, it is somewhat fragile to compare real values for equality, because computations on reals are prone to rounding errors. For this reason, SML does not allow pattern-matching on values of type real (floating point numbers), so you cannot do a test like val 0.5 = halfSum 1. Instead, you need to use an explicit equality test, like the following:
val true = Real.==(halfSum 1, 0.5)
Methodologically, it is usually better to check that two real values differ by a small , rather than checking for exact equality with Real.==. However, Real.== should suffice for writing tests in this assignment. That said, if you encounter an unexpected failing test, it may be because Real.== does exact floating point comparison, and your calculation does not come out to exactly the value you anticipate.
3.2.1 Going Halfway Forwards and Back
A related sequence is the alternating version of this series, in which every other term has negative sign:
1 1 1 1
2 − 4 + 8 − 16 + · · ·
For any natural number n, we will call the partial sums of this alternating series In:
In = X
Like the previous series, this alternating series converges; as n approaches infinity, In
approaches 1 .
Task 3.4 (4%). What are I0, I1, I2 , I3?
Task 3.5 (8%). In hw02.sml, write and document a recursive function
altHalfSum : int -> real
such that altHalfSum n calculates In, according to the specifications above. Again, please use recursion. Hint: find a way to calculate In recursively. Don’t look for a closed form for In, and don’t try to use halfSum as a helper function!
3.3 Primality Test
You have probably heard about prime numbers in the past. Here, we will be utilizing recursion to determine if a natural number is prime. Recall the definition for prime numbers:
Theorem 1. A natural number n > 1 is prime if and only if it is divisible by only itself and
Given the input number n, a simple test for primality is to go through all of the numbers from 2 to n − 1 and check if each divides into n. This can be done with recursion, using an extra argument that keeps track of which potential divisors we have already checked. We can test for divisibility using mod, because n is divisible by m if and only if n mod m = 0.
Of course, we only really need to check for divisibility by 2 through √n, but we will not
penalize you if your code checks for divisibility by 2 through n − 1.
Task 3.6 (12%). Write an ML function
is prime : int -> bool
in hw02.sml such that for all natural numbers n, is prime returns true if n is prime and false otherwise.
Hint: Use a recursive helper function of a suitable type, as outlined above. Make sure you give proper documentation for any helper function(s) that you define, including type and specification.
4.1 All-Zero Lists
Recall the function eval : int list -> int as shown in lecture:
fun eval [ ] = 0
| eval (x::L) = x + 10 * eval L
An integer list is called all zeroes if each of its members is 0. Trivially, the empty list has this property, and a non-empty list x::R has this property if and only if x = 0 and R is all zeros.
Task 4.1 (10%). Prove that for all integer lists L such that L is all zeros, eval L ⇒∗ 0. Make sure to use evaluational reasoning accurately, and state clearly what method of induction you use. You can find some helpful proof templates in code/hw02-proof-templates.tex. You should structure your proof using the appropriate template for the proof method you use.
4.2 Summation of Odd Numbers
Task 4.2 (10%). Look at the following function carefully.
fun sumOdd (0 : int) : int = 0
| sumOdd (n : int) : int = (2*n – 1) + (sumOdd (n – 1))
Prove the following theorem about sumOdd:
Theorem 2. For all natural numbers n, sumOdd n = n * n.
The proof is by induction on the natural number n.
Follow the same requirements as in the previous induction proof. You may assume that
n*n + 2*n + 1 = (n+1) * (n+1). Cite this as fact (i).