[logic-ml] Seminar on Thu Feb 21

[Akitoshi Kawamura]

皆様

東京大の河村です
お世話になっております

新学術領域研究「計算限界解明」（ELC）A01班「数理論理学からの計算限界解析」では
2月21日（木）午後に東大本郷キャンパスで下記の講演会を開催致します
詳しくはウェブ頁を御覧下さい
http://www-imai.is.s.u-tokyo.ac.jp/~kawamura/elc/seminar_H250221.html
計算理論と数理論理学の両方から多くの皆様の参加をお待ちしております
講演会そのものに参加申込は不要ですが
懇親会に御参加の場合はウェブ頁よりお早めに申込をお願い致します（締切2/17または定員になるまで）

# なお「計算限界解明」のイベントとしましては
# 先日垂井先生からも案内のありました
# キックオフシンポジウム（3月14〜17日、東京品川）も是非御参加下さい
# こちらも参加費は（宴会等を除いて）ありませんが
# 登録をお願いしておりますのでお早めにお願い致します

-- 
河村彰星
東京大学大学院情報理工学系研究科コンピュータ科学専攻
助教（今井研究室）
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.)