Section A: MWF 11:00 - 11:50
Section B: MWF 2:30 - 3:20
Classroom: Olin 129; we will occasionally meet in Olin 124 (lab hours)
Instructor: Janet Davis (davisj@whitman.edu)
Office hours: As posted and by appointment
Class mentor: George Ashley (Sundays 8-9, Thursdays 5-6)

See also course policies and learning activities

About this course

Welcome to CS/MATH 220! The official course description:

I am excited to bring together so many beautiful ideas in this course. 

Course goals

By the end of this class, you will be able to:

• Manipulate forms in symbolic logic, including forms that use universal and existential quantifiers;
• Apply several techniques for proving propositions about sets, relations, functions, and the correctness of algorithms;
• Appreciate two proofs that some problems cannot be solved algorithmically;
• Write simple programs in the SML programming language;
• Model phenomena in nature or culture using sets, relations, and functions, as well as SML datatypes;
• Devise, implement, and test solutions to algorithmic problems, using symbolic logic to analyze the problem and synthesize a solution.

Recurring themes include:

• Writing and using formal definitions. We look carefully at formal, rigorous definitions of mathematical ideas, built from primitive terms.
• Thinking recursively. Recursion is defining something in terms of itself. This technique is crucial to some kinds of algorithms and to some kinds of mathematical definitions and proofs.
• Analysis and synthesis. Many of our proofs and programs comprise two main steps: Breaking something apart and putting something else together.

Overview

For a detailed outline, see the table of contents for the first seven chapters in your textbook. 

Set and List.

We meet the basic mathematical concepts of set, element, set operations, cardinality, Cartesian product, and powerset. We learn the basics of the ML programming language including functions and datatypes. We learn to use ML's main composite type, the list.

Preposition.

We explore the system of Boolean logic (the "first-order predicate calculus"). This heading is characterized by three "games" to exercise your understanding of symbolic logic: 1. verifying logical equivalences; 2. verifying argument forms; 3. verifying argument forms with quantification. We also write ML programs that use Boolean operators and consider how the quantification of a problem specification affects the algorithm to solve it.

Proof.

We learn to write careful proofs of set-theoretical propositions. This includes one of the most challenging sections, proofs about powersets. We also consider the connections between proofs and algorithms.

Relation.

We build on our understanding of sets to consider the definition of mathematical relations and their properties, propositions about them, and programs that manipulate them. The relation is a useful concept in itself, but this heading also lets us practice further the proof and programming techniques we have learned so far.

Self-reference.

Earlier parts of our study will have introduced recursive definitions, but here we tackle the idea head-on. Specific topics are recursive types in ML programming and proofs using structural and mathematical induction.

Function.

We study functions as mathematical objects built on set theory. These proofs will build on all the techniques you have learned so far. We also learn programming idioms that build on the theory of functions as mathematical objects.

Acknowledgments

Thanks to Thomas VanDrunen and John David Stone for informing my development of the course.