Spring, 2006
In this class we use a formal first-order logic of recursive functions to study fundamental ideas in computing. The logic is a subset of applicative Common Lisp. However, no familiarity with Lisp is assumed.
The logic could be replaced with practically any other formalization of primitive recursive arithmetic with lists without changing the character of the course.
You use the logic, formally, day after day. In the Socratic style, you will prove interesting but elementary theorems about arithmetic and list processing to familiarize yourself with the logic and the mathematical notion of proof.
You will learn to use a tiny fraction of the features in a mechanized theorem proving program called ACL2 to check your proofs.
You will then use the logic and proof checker to model and prove theorems about selected applications in computer science, including the semantics of programming languages and computing engines (e.g., the JVM) and properties of interesting algorithms.
While only graduate standing is required, this course is a `diversity course' in the Theory area of our Ph.D. program. Historically, almost all of the students who have taken the course have been in the Ph.D. program.
There is no textbook.
For the first half of the semester we will use notes handed out on the first day of class. The notes contain many problems for you to work. The answers to these problems are on the web. But do not look at the answer to a problem until you have worked for days on the problem and are truly stuck! You will learn much more by trying to solve the problems yourself!
This course is taught in the style of R.L. Moore, after whom the UT mathematics building was named (and who was of no relation to me).
Problems are posed in class, often by me but sometimes by students.
Solutions are presented in class at the board by students, who answer the questions and criticisms of fellow students. I keep a record of who participates in class --- at the board and from the audience --- and this record is used to determine a ``class participation'' grade.
Note-taking in class is often counter-productive in this course. If the student at the board is on the wrong track, you are better served by discovering that and asking the appropriate question than by rotely recording what is being said. Therefore, I encourage you to listen critically to your fellows when they are presenting material and spend your time in class thinking, not writing.
You are expected to figure out the solutions to the problems by yourself, not by reading books or talking to others or looking them up on the web! If you have found the answer to a problem by one of these prohibited methods you will not be able to do the exams! Please do not offer to present the proofs in class unless you discovered the proof yourself.
The logic we use is one with which I am intimately familiar since I am one of its ``inventors.'' It is known to be of practical value: it has been used to solve complex problems of industrial interest, including the correctness of important algorithms and the analysis of microprocessor designs. Hundreds of pages of formalism in the logic have been written to model industrial problems and thousands of theorems have been proved about those models. The logic is one of only a few formal logics in history which have been so used. That said, I should hasten to add that the logic is more elaborate and complicated than most formal logics and you may feel lost for a while. Please be patient, read the notes carefully, ask questions in class, and talk to me. Your efforts will be rewarded by a clearer understanding of much that is important in computing.
I will keep track of class participation, which reflects how often you present solutions (or attempts) in class, ask probing questions or make cogent remarks about other solutions. Visits during office hours count as class participation.
There will be two exams: a midterm and a final. The exams will primarily test your ability to formalize and prove theorems. You may refer to your notes during the tests.
Thus, at the conclusion of the course you will have three grades: the class participation grade and two exam grades.
I will compute your grade in the class by averaging the two highest of these three grades. Students who have an A in class participation and an A on the midterm need not take the final. I will make the class participation grade available on or before the last day of class.