ELC Seminar, Thu Feb 21, 2013

[Feb 18] Two more talks in the morning
[Feb 7] Please register if you are coming to the dinner (at a nearby izakaya).
[Feb 4] The second and the third talks have been switched.

Kazushige Terui (Kyoto University)
Sebastian Müller (Charles University)
Martin Ziegler (TU Darmstadt)
Thursday 13:45–, February 21, 2013
(This is the day after the CTFM workshop and before Sendai Logic School.) 上野駅時刻表
セミナーは参加申込不要ですが懇親会に来られる方は2月18日(月)までにこちらからお願い致します←Register here for the dinner (the fields are: name, affiliation, email)
Room 214, Science Building 7 (理学部七号館), University of Tokyo
15 min walk from Todaimae 東大前 [N12], Nezu 根津 [C14], Hongo-Sanchome 本郷三丁目 [E08/M21], or Yushima 湯島 [C13]; 20 min from Ueno 上野 [G16/H17/JR]

Campus Map

Timetable and Abstracts

10:30–12:30 Another seminar in the morning
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 n0,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 n0,4.

Iddo Tzameret and me formalized this witness in a weak bounded arithmetic theory called VTC0. 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 TC0-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 here by Feb 18

ELC Research Group A01「数理論理学からの計算限界解析」Exploring the limits of computation through Mathematical Logic