Computability and Logic

Fall 2003

Instructor: Professor Bob Keller, x 18483, keller@cs.hmc.edu

Office Hours: 1249 Olin, MTuW 4-5 p.m., or drop in other times

Graders: Alexander Popkin, Erika Rice (x74742)

Catalog Description:

An introduction to some of the mathematical foundations of computer science, particularly logic, automata, and computability theory. Develops skill in constructing and writing proofs, and demonstrates the applications of the aforementioned areas to problems of practical significance. Prerequisites: Math 55, Computer Science 60. 3 credit hours. (Both semesters.)

Further Description:

While we will use mathematical ideas from the prerequisite courses, we will pull them in as they become relevant, rather than spending a week going over all the background that you have.

We will begin by examining finite-state automata (computing machines) and their relationship to languages and regular expressions. We will look at the applications and limitations of these machines, then move on to the more powerful pushdown automata.

We will show how pushdown automata exactly characterize the larger family of languages known as context-free languages. These are the languages generated by grammars of the type you studied in CS 60. We will look at the applications of these automata, and also show their limitations.

Next we'll look at Turing machines, which are the most powerful, in some sense. We'll discover what kind of grammars are equivalent to Turing machines, and along the way look at the special subset of context sensitive grammars and their specialized Turing machines.

As with other families of machines, even Turing machines have their limitations. However, unlike the others, the limitations of Turing machines can't be overcome by introducing a more powerful model while staying with what can be realistically called computed. In other words, there are problems not solvable by Turing machines or any other family of computing machines. We will show how to prove that certain problems are in this class of unsolvable problems.

Finally we will look at logic in more depth. While we have been doing proofs all along, we will show how the proofs can be cast into a more formal framework, which is not unlike earlier ideas of grammars. In fact, there is a common notion "Formal Systems" which unifies all of the models discussed to this point. Loosely speaking, a formal system is any system of reckoning that can be mechanized by a computational process. We will gain some experience in doing proofs in such formal systems, particularly in a style known as "natural deduction". This will be helpful as a way of outlining proofs for the rest of our careers. Then we will show that determining whether or not a mathematical statement is provable in such a system is one of the unsolvable problems discovered earlier. This will help us shed some light on issues of completeness of formal systems. (A logic is complete if it permits the derivation of all valid statements.) In a certain sense, no sufficiently powerful logic will be complete.

Relationship to the old CS 80:

CS 80 was a course devoted almost exclusively to formal logic. While formal logic is important, there are other related topics that are equally important and but not previously covered in any required computer science course. The new course, CS 81, endeavors to give a broader view of the theoretical foundations of computation than does CS 80. The new course will provide exposure to logic, formal languages, and computability theory. The course will demonstrate how these three major areas of computer science are related to one another and are also useful in many application areas.

Grading: Homework 50%, Exams 50% (3 exams, including final)

Collaboration Policy: No collaboration, unless indicated by the instructor.

Exam Policy: Closed book.

Late Policy: No late work accepted, unless indicated by the instructor.

Texts:

John Martin, Introduction to Languages and the Theory of Computation, 3rd Edition, McGraw Hill, 2003.

Michael R A Huth and Mark D Ryan, Logic in Computer Science, Cambridge University Press, 2000.

	CS 81 Outline (Draft, 8/15/03)
Legend
	Mn = Chapter n of Martin text.

	Hn = Section n of Huth and Ryan text.

Day	Topics	Reading
1	Sets, strings, algebraic structures (monoids) Finite automata and their languages Closure properties Non-deterministic finite automata; transition systems Regular sets and expressions Application: text pattern matching	M3
2	Subset construction, Kleene's theorem Regular pumping lemma	M4
3	State minimization, homomorphisms Application: switching circuits Left-derivative of regular sets, Myhill-Nerode theorem Two-way finite automata	M5
4	Context-free grammars and languages Normal forms	M6
5	Pushdown automata Application: Parsing Cocke-Kasami-Younger algorithm	M7
6	Context-free pumping lemma Closure properties Ogden's lemma	M8
7	First Exam
8	Turing machines Context-sensitive languages Chomsky hierarchy Linear-bounded automata	M9
9	Recursively-Enumerable languages Decidability Equivalent models	M10
10	Unsolvable problems Post's Correspondence problem Reduction Rice's theorem	M11
11	Primitive and partial recursive functions While programs Post's Correspondence Problem Other computability formalisms	M12
12	Lambda calculus Fixed-point operators (Y)	notes
13	Second Exam
14	Review of propositional logic Natural deduction	H1.1-1.4.3
15	Soundness and completeness	H1.4.4-1.5.1
16	Predicate logic Natural deduction for predicate logic	H2.1-2.3.1
17	Examples of Logical Theories Partial Orders, Semigroups, Monoids, Groups, Peano Arithmetic, Rings, Fields, Number Theory	notes
18	Semantics Validity	H2.3.2-H2.4
19	Undecidability of predicate logic	H2.5
20	Completeness and Incompleteness of predicate logic	notes
21	Program verification Hoare logic Weakest precondition reasoning	H4, notes
22	Continuation of previous
23	Final Exam