Functional Programming as a Discrete Mathematics Topic

tions have, and we write proofs about functions. This study of mathematical functions situates the final, advanced functional programming topics, the programming idioms which students can transfer to other programming contexts. As students think about functions as mathematical objects, functions as first-class values follow naturally. We can now talk about anonymous functions (lambda abstractions), map/reduce, and generic programming strategies that are parameterized by a function, such as fixed-point iteration. Students observe the analogy between the image of a function mathematically and the programming idiom of mapping a function onto a list, as displayed in Figure 4.

ARE THERE OTHER BENEFITS TO TEACHING
DISCRETE MATH AND FUNCTIONAL
PROGRAMMING TOGETHER?

Can this approach motivate students in discrete math? McMaster et al. [ 14] reported that “most students enjoy the benefit from having programming projects in the discrete math course.” My own experience confirms that the computer science majors who are less mathematically inclined find that the programming assignments sweeten the experience in a course largely devoted to proof-writing.

As I have argued elsewhere [ 23], another reason for teaching
functional programming in a discrete math course is simply that
functional programming is an important part of the computer
science curriculum in general, and the discrete math course is a
convenient place to put it. Functional programming received less
attention in CS education for years, but CS2013 now allots three
Core Tier- 1 hours and four Core Tier- 2 hours to functional pro-
gramming [ 12]. Even if primary instruction in the CS1 and CS2
courses is in the imperative or object-oriented style and even if
students go on to do most of the programming in their careers
in those styles, familiarity and usage of functional programming
illuminates the idea. Figure 3 illustrates this connection with
a theorem about the transitive closure and a programming
problem induced by that theorem.

Students write recursive functions from the second week of the course, but the sixth unit takes a closer look at self-reference and applies it more widely. We start with recursively-defined types, which are a natural parallel to recursively defined mathematical sets. While defining Peano Numbers, both abstractly and in an ML datatype, we implement even seemingly primitive operations like addition recursively. We also consider more advanced algorithmic topics that rely on recursively-defined types, such as the Huffman encoding. But the premier topic is proof by induction, both traditional mathematical induction for propositions quantified over whole numbers and structural induction for quantification over recursively defined sets. The students are well-prepared for inductive proofs from their experience with recursive algorithms. Figure 4 shows a typical proof problem about the relationship between the number of leaves and number of internal nodes in a full binary tree in parallel with a programming problem for computing the number of leaves. But the strongest connection induction has with programming is its use to prove the correctness of an algorithm. At this point in my course I give a quick introduction to imperative programming and loops for those who have never seen iteration, and we use mathematical induction in loop-invariant proofs. One could easily keep things purely functional, though, and use structural induction on the sequence of function calls to prove that a recursive function is correct. The precondition to the call serves a nearly identical role to a loop invariant.

In the seventh unit, the course again takes a closer look at an idea the students are by now familiar with. They have been writing functions the entire semester, but now we define functions mathematically. We consider properties that some func-

 

Figure 4: Sample problems for self-reference and functions