Exercises for Week 05

Exercise 00

1. The index of concepts for this week is in a separate chapter. Peruse it and make sure that its entries make sense to you (otherwise, click on them to check them out).
2. The lecture notes start with updates (Chapter Lecture Notes, updates). Make sure to check them out regularly, as they reflect the development of the lecture.
3. Do take the time to peruse the lecture notes of this week and to reproduce their OCaml content.
4. What is the computational content of a paradox? Revisit Exercise 27 – multiple-choice questions in Week 01.
5. In the chapter about the factorial function, the factorial function refers to itself. That sounds paradoxical, and yet applying it on a non-negative integer terminates. Why is that?

Mandatory exercises

• Exercise 00: perusing the index and checking the updates
• Exercise 01: some food for thought about basic computational arithmetic
• Exercise 02: mapping a string of letters from lowercase to uppercase and vice-versa
• Exercise 06: implementing a polymorphic unparser for quadruples
• Exercise 07: comparing and contrasting two proof trees
• Exercise 09: figuring out what a given OCaml function computes
• Exercise 12: justifying the base case of the factorial function
• Exercise 13: implementing a predicate to determine whether a given non-negative integer is odd
• Exercise 14: testing the unit-test function for nat_of_digits
• Exercise 15: explaining nat_of_digit
• Exercise 16 (implementing the base case): implementing the base case of nat_of_digits
• Exercise 17 (implementing the induction step): implementing the induction-step of nat_of_digits
• Exercise 21: debugging an implementation of the power function

Recommended exercise

• Exercise 03: implementing Emacs’s M-u and M-l

Exercise 21

The present exercise arose from a live-coding section in class, where a previous generation of students proposed a collection of tests to populate the unit-test function for the power function, based on its specification (see Exercise 11):

Given an integer x,

• base case (i = 0): exponentiating x with 0 yields 1
• induction step (i = succ i’): given a number i’ such that exponentiating x with i’ yields ih (which is the induction hypothesis), exponentiating x with succ i' should yield x * ih

(The intuition behind this inductive specification is that x^n = x * (x * (...(x * 1)...)), where x is iteratively multiplied n times, starting with 1, as per Exercise 01.l in the lecture note about strings.)

The lecturer then fleshed the resulting .ml file with informative error messages, should one of the tests fail.

This .ml file contains a bug, and your task is to locate and fix this bug.

To this end, load this file a few times in OCaml, as in:

# #use "week-05_power.ml";;
...
#

until the bug becomes apparent (i.e., when an assertion fails to hold).

Then figure it out and fix it.

Hint: redefine the silent flag at the beginning of the file to enable the displaying of error messages.

Resources

• The accompanying .ml file for Exercise 21 (latest version: 11 Feb 2023).

Version

Added Exercise 12 [12 Feb 2023]

Streamlined the unit-test function in the accompanying .ml file for Exercise 21 [11 Feb 2023]

Created [10 Jan 2023]