Fall, 2011
PLUS, TIMES, MOVE-DISKS, HANOI, and the definition of QUICKSORT
QUICKSORT produces ordered output
QUICKSORT produces a PERM of its argument -- yet!
Instead, define (HM E X) to count how many times E occurs as an element of X and
prove that (hm e (quicksort x)) is (hm e x).
HM and QUICKSORT
PERM and HM
PERM-HM to convert a
PERM problem into a ``how-many'' problem. Then I showed how to
exploit that converstion to prove that QUICKSORT produces a
permutation of its input, by proving that it preserves the ``how-many''
question on an arbitrary E. Here is the promised
script, perm-quicksort-via-hm.lisp.
PERM
is an equivalence relation enjoying certain congruence properties. Here is the
PERM-QUICKSORT proof again, using that approach,
perm-quicksort-via-congruence.lisp.
set-equal
and tried to prove a particular theorem about it. I explained that his definition was correct and
reasonable, but not the way I would have defined set-equal. Nevertheless, we decided
to try to prove his theorem in class. The resulting script is here.
You will note that we failed to complete the proof. Search for (i-am-here) in the
script and figure out how to get ACL2 to prove the remaining checkpoint.
rev-app Matt worked in class.
In this class we use a formal 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 except for one major aspect of it: You will learn to use (a small subset of) ACL2, a mechanized formal modeling and verification tool.
The course will proceed in a top-down way: after a brief and, I hope, thought-provoking tour of some applications of machine-checked reasoning about hardware and software, we will discuss suggestions for what we might model and prove during the semester. These discussions will highlight strengths and weaknesses of formality and the mechanization of mathematical reasoning. We will ultimately settle on some team projects. The bulk of the semester will consist of individuals and teams discussing their problems with modeling and proving things. These discussions will most often lead to mathematical insights about formal specification and inductive proof techniques, e.g., the role of recursion, definition, termination, appropriate inductive hypotheses, generalizations, invention of auxiliary concepts necessary to state inductively provable facts, meta-reasoning, useful lemmas about domain-specific concepts, etc.
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.
While I tend to use ACL2 running in a shell buffer under Emacs, many find it convenient to use the Eclipse interface to ACL2, known as the The ACL2 Sedan for Eclipse or ACL2s. It's called the “sedan” for good reason: driving full ACL2 is like driving a race car; one mistake and you're in the ditch.
ACL2s is installed on all the department's public machines. See for explicit instructions on using the Sedan on department machines.
You may wish to install ACL2s on your own laptop. See also this ACL2s Installation FAQ.
I will assign reading from the textbook above weekly. I regard your reading as a critical background activity: no formal logic can be “picked up” by random trial-and-error. And you must learn how to express yourself in the logic in order to use it to model and prove anything.
The textbook is full of problems and I expect you to do a representative sample of them from the reading. I will call upon students in class to present solutions to unannounced problems from the assigned reading, especially if no team needs to discuss their current difficulties!
But learning the logic should be a background activity for you. Each student will be in a team working on some half-semester-scale project and most class sessions should consist of team members discussing problems with the entire class. The projects are not meant to be competitive with each other. A student's contribution of some key insight to another team's project is highly valued. Successfully proving the ``goal theorem'' of a project matters less to me than what the class learned along the way from the attempt.
I will keep track of class participation, which reflects how often you contribute usefully in class. Asking probing questions, advancing toward a solution, identifying obstacles, suggesting useful strategies, showing counterexamples, explaining dead ends, visiting me during office hours, and other such positive contributions will be counted.
Attendance will be taken in every class meeting. Unexcused absence from any regularly scheduled (TT 3:30-5:00) class meeting is the only activity that will count negatively against your class participation!
There will be a midterm exam in which you will be tested on your ability to use the logic to model and prove (“by hand”) some simple properties.
At the end of the semester, teams will make presentations on their projects. In addition, each team member will be asked to write a one paragraph description of what each other team member did.
I will therefore have three assessments of each student: class participation, midterm, and team participation. I will throw out the lowest of these three and base the final grade on the other two.