Exploring the Limits of Computation (ELC)

Implicit computational complexity (ICC) aims at giving a qualitative accout to various complexity classes. A typical approach to ICC is to consider a computational model (in finite model theory, recursion theory, term rewriting, functional programming, etc.) and propose a qualitative criterion/certificate for a program in the model to be executed within a given time/space bound (e.g. polynomial time). Here we are particularly interested in higher order functional programming languages, which are often modeled by lambda calculus. It is then types that give a criterion/certificate for the resource bound. Because of the Curry-Howard correspondence, it is also linked to constructive logics. Linear logic plays a prominent role in this context.

The purpose of this talk is to give a general overview of the type-theoretic approaches to ICC. It will be neither comprehensive nor detailed. I will just review some nice ideas in the past development, and discuss their future possibilities from my very personal (and sometimes critical) point of view. The topics will be chosen from the following list:
 • safe recursion in higher order
 • linearity and various modalities
 • arithmetic systems based on ICC
 • realizability semantics
 • denotational semantics
 • time-space tradeoff in lambda calculus

(joint work with Iddo Tzameret)

A classical result by Chvatal and Szemeredi states that with high probability, a given random 3CNF is unsatisfiable, if the clause-to-variable ratio is larger than 8 ln(2). On the other hand, on almost all unsatisfiable random 3CNF with a clause-to-variable ratio of less than n^0,5 (where n is the number of variables) Resolution fails to witness that unsatisfiability efficiently (due to Ben-sasson and Wigderson). On the other hand, Feige, Kim and Ofek constructed a witness for unsatisfiability that is polynomial-time constructable and works for random 3CNF with a clause-to-variable ratio above n^0,4.

Iddo Tzameret and me formalized this witness in a weak bounded arithmetic theory called VTC⁰. I will explain this result and sketch the main steps of the proof and later eloborate on the consequences for propositional proof system. As a direct consequence we receive efficient refutability of such formulas in TC⁰-Frege proof systems and, with the above, a separation between such systems and Resolution on a random, dense set.

(joint work with Ulrike Brandt and Klaus Ambos-Spies)
Promises are a standard way to formalize partial algorithms; and advice quantifies nonuniformity. For decision problems, the latter it is captured in common complexity classes such as P/poly, that is, with advice growing in size with that of the input. We advertise constant-size advice and explore its theoretical impact on the complexity of classification problems – a natural generalization of promise problems – and on real functions and operators. Specifically we exhibit problems that, without any advice, are decidable/computable but of high complexity while, with (each increase in the permitted size of) advice, (gradually) drop down to polynomial-time.