[logic-ml] Seminar on Thu Feb 21

-- 河村彰星 東京大学大学院情報理工学系研究科コンピュータ科学専攻 助教（今井研究室） 03-5841-4097 http://www-imai.is.s.u-tokyo.ac.jp/~kawamura/index_j.html 記 ELC Seminar on February 21, 2013 http://www-imai.is.s.u-tokyo.ac.jp/~kawamura/elc/seminar_H250221.html Speakers * Kazushige Terui (Kyoto University) * Sebastian Müller (Charles University) * Martin Ziegler (TU Darmstadt) Time Thursday 13:45-, February 21, 2013 Place Room 214, Science Building 7 (理学部七号館214室), University of Tokyo ---- 13:50-14:50 Kazushige Terui (Kyoto University) Type Theoretic Approaches to Implicit Computational Complexity 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 ---- 15:10-16:10 Sebastian Müller (Charles University) Short Refutations of Random 3CNF in TC0-Frege (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^0. 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^0-Frege proof systems and, with the above, a separation between such systems and Resolution on a random, dense set. ---- 16:30-17:30 Martin Ziegler (TU Darmstadt) Real Benefit of Promises and Advice (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. ---- 18:00- Dinner (Please register on the webpage if you are coming to the dinner.)