COMP9103:

Computational Complexity Theory

 

07s2

 

Lecturer: Aleks Ignjatovic

 

Friday 3-6 in Webster 251 (K-G14-251)

 

 

Lecture Notes 1 (30-07-2007)

Lecture Notes 2 (14-08-2007)

Lecture Notes 3 (31-08-2007)

Lecture Notes 4 (03-09-2007)

Lecture Notes 5 (31-10-2007)

 

 

 


Course description:

 

All important problems in computational complexity theory (over natural numbers, or equivalently, over finite strings) such as the famous "P=NP?" problem, remain open despite several decades of resolute effort on the part of many famous mathematicians and computer scientists. One possible reason for the lack of progress in this field, besides the inherent difficulty of the problems, is that there is no unified foundational framework in which one can systematically develop powerful methods and prove deep general theorems that apply to computational complexity problems; most of the attempts to solve such problems are ad hoc and combinatorial. There is no theory that corresponds to what Galois Theory is for algebraic equations, what the theory of linear operators on a Hilbert space is for integral equations, or what mathematical logic with Goedel's constructibility and Cohen's forcing are for the classical set theoretic problems, such as the status of the Axiom of Choice or the Continuum Hypothesis.  

 

In the past two decades some researchers were hopeful that, just like for set theory, mathematical logic could also provide the necessary foundations for computational complexity theory, allowing the use of powerful proof theoretic, model theoretic and Goedel's incompleteness techniques to computational complexity problems. Unfortunately, logic still has not solved any major outstanding problems in complexity theory; however it did uncover some deep and intriguing connections between computational complexity and various proof systems that still motivate some of the research in this area.

 

The main aim of this course is to present some of the fundamental techniques of mathematical logic and their applications to computational complexity. The presentation will be fast paced but self contained, except that some elementary results will be given without proofs, which can be found in standard logic textbooks. It is aimed at enthusiastic 4th year students or PhD students interested in computational complexity theory from various perspectives.


Topics to be covered:

 

(I)            A brief introduction to Computational Complexity Theory (on integers):

a.    Non deterministic computations, computations with oracles;

b.    The Linear Time and the Polynomial Time Hierarchies;

c.    Space bounds; Savitch’s and Nepomnjaščij’s Theorems.

 

(II)        Basic Logic Tools:

a.    Gentzen and Tait style proof systems;

b.    Peano’s Arithmetic and its fragments;

c.    Limited Truth definitions and finite axiomatizability of Sigma_n induction;

d.    The Cut Elimination Theorem and Gentzen’s proof of consistency of  Peano arithmetic by transfinite induction up to the ordinal epsilon_0;

e.    Characterizing primitive recursive functions as provably total functions of Sigma_1 induction using the Cut Elimination Theorem; Herbrand Analysis of Sigma_1 induction; Weak Koenig Lemma;

f.    Models of fragments of arithmetic; obtaining e. above by model theoretic means;

g.    Coding sequences and formalization of syntax; Goedel Incompleteness;

 

(III)    Fragments of bounded arithmetic and the computational complexity classes:

a.    Theories of bounded arithmetic;

b.    Herbrand Analysis of fragments of bounded arithmetic;

c.    Characterizing Polynomial Time Hierarchy as classes of provably total functions of some fragments of bounded arithmetic;

d.    Separability of fragments of bounded arithmetic and possible collapse of the Polynomial Hierarchy.

 


Assessment: A take home final or in class presentation


Texts: (not all necessary but useful)

 

  1. S. Cook and P. Nguyen, Foundations of Proof Complexity: Bounded Arithmetic and Propositional Translations, available on the web for free at: http://www.cs.toronto.edu/~sacook/csc2429h/book/

 

  1. S.Buss, Bounded Arithmetic, Bibliopolis, 1986.

 

  1. Wilfried Sieg: Fragments of Arithmetic, Annals of Pure and Applied Logic 28 (1985), pp. 33-71, North-Holland.

 

  1. Wilfried Sieg: Herbrand Analyses, Archive for Mathematical Logic 30(1991), pp. 409-441, Springer-Verlag.

 

  1. J. Krajcek, Bounded Arithmetic, Propositional Logic and Complexity Theory, Cambridge University Press 1995.

 

  1. P. Hajek and P. Pudlak, Metamathematics of First Order Arithmetic, Springer – Verlag, 1993.

 

I will also provide some lecture notes and a collection of papers. We will also look at some of my own work in this area, with a hope of extending it during or after this course, for example:

 

  1. A. Ignjatovic: Delineating Classes of Computational Complexity via Second Order Theories with Weak Set Existence Principles, The Journal of Symbolic Logic, vol. 60, Number 1, March 1995, pp. 103-121.

 

  1. S. Buss and A. Ignjatovic: Unprovability of Consistency Statements in Fragments of Bounded Arithmetic, Annals of Pure and Applied Logic, vol. 38, Number 2, June 1995, pp 1-31.

 

  1. A. Ignjatovic and A. Sharma: Some applications of logic to feasibility in higher types, ACM Transactions on Computational Logic (ToCL), Volume 5, Number 2, 2004

 

  1. A. Ignjatovic, P. Nguyen: Characterizing Polynomial Time Computable Functions Using Set Theories with Weak Set Existence Principles (II), Computing: The Australasian Theory Symposium (CATS) 2003, Electronic Notes in Computer Science 78, Elsevier, Netherlands.

 

  1. P. Clote, A. Ignjatovic and B. Kapron: Parallel Computable Higher Type Functionals, Proceedings of the IEEE 34th Annual Symposium on Foundations of Computer Science (FOCS), 1993, Stanford.

 

 

 


 

Maintained by Aleksandar Ignjatovic. Enquiries to: ignjat@cse.unsw.edu.au