所員 -照井 一成-

名前 照井 一成 (Terui, Kazushige)
准教授
E-Mail terui (emailアドレスには@kurims.kyoto-u.ac.jp をつけてください)
研究内容 数理論理学に関する研究
紹 介
 「古典論理を理解するための非古典論理学」を推進する一方, 計算量,プログラムの意味,評価戦略など,計算機科学にまつわる諸問題を 数理論理学によって解明することを目指している。かつて論理学といえば 「前提→結論」という推論の研究に範囲が限定されていたが, 現代においては「インプット→アウトプット」という計算や, 「エージェント↔エージェント」というコミュニケーションをも 十分視野に納めている。特に関心をもっているのは, (1)線形論理と(2)部分構造論理である。
 (1)線形論理,これは数学において線形代数が果たすのと同じ役割を 論理学において果たすものである。証明やプログラムは 線形的な部分と指数関数的な部分に分解できるというのがその核心である。 これまでは,線形論理に基づく計算量クラスの特徴付け[8,9],線形論理から派生 したルディクス(あそび)の理論に基づく計算論再構築の試みなどを行ってきた[3]。 またルディクスの枠組みで,伝統的な完全性定理(証明可能性 vs 反証可能性)を 証明-モデル間のコミュニケーションとして理解する試み[7], 再帰型の一意的解釈[6]等の研究を行った。 最近では,線形論理のモデルを用いて(単純型付き)ラムダ計算のプログラムを 高速に実行する方法を考案した。それによりシューベルトの問題 (ラムダ項の正規化にかかる計算量を項のオーダーn ごとに確定する問題: $n=2,3$ については 2001年に解決済み)に一定の条件付きではあるが 一般解を与えることに成功した[1]。
 (2)部分構造論理,これは構造規則を弱めることによって得られる 論理一般の系を考察することにより論理の本質に迫ろうという試みである。 主な成果としては,まず与えられた部分構造論理(のシークエント計算)について 証明論の基本定理("補題を用いて間接的に証明できることは直接的にも証明できる"こと) が成り立つための必要十分条件を代数的に与えたことがあげられる[10]。現在提唱 しているのは, 非古典論理における代数的証明論のプログラムであり,これはさまざまな論理的公理 を 証明論的難易度に従って階層づけ,そして証明論的手法と代数的手法の相互作用を通 じて 新しいタイプの結果を出していこうというものである[2]。 鍵となるのは,証明論の 基本定理は 代数の言葉でいえば完備化に相当するという洞察である。これにより証明論的研究と 代数的研究を結び付けることが可能になり,部分構造論理一般の可能性と限界を画定 するという 目標が一気に現実味を帯びてきた。具体的成果としては、まず 選言特性と計算量を関連付けることにより,多くの部分構造論理が PSPACE困難であることを証明した[4]。また証明論的手法を代数の文脈に直接適用 することにより、多くの剰余束の等式クラスが完備化について閉じていることを 証明した[5]。
  1. Kazushige Terui. Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus. Proceedings of 23rd International Conference on Rewriting Techniques and Applications (RTA'12), pp. 323-338, 2012.
  2. Agata Ciabattoni, Nikolaos Galatos and Kazushige Terui. Algebraic proof theory for substructural logics: Cut-elimination and completions. Annals of Pure and Applied Logic, 163, No. 3, pp. 266-290, 2012.
  3. Kazushige Terui. Computational ludics. Theorical Computer Science, 412, No. 20, pp. 2048-2071, 2011.
  4. Rostislav Horcik and Kazushige Terui. Disjunction property and complexity of substructural logics. Theoretical Computer Science, 412, No. 31, pp. 3992-4006, 2011.
  5. Agata Ciabattoni, Nikolaos Galatos and Kazushige Terui. MacNeille completions of FL-algebras. Algebra Universalis, 66, No. 4, pp. 405-420, 2011.
  6. Michele Basaldella and Kazushige Terui. Infinitary completeness in ludics. Proceedings of IEEE Annual Symposium on Logic in Computer Science (LICS'10), pp. 294-303, 2010.
  7. Michele Basaldella and Kazushige Terui. On the meaning of logical completeness. Logical Methods in Computer Science, 6, No. 4, 2010.
  8. Patrick Baillot and Kazushige Terui. Light types for polynomial time computation in lambda calculus. Information and Computation, 207, No. 1, pp. 41-62, 2009.
  9. Kazushige Terui. Light affine lambda calculus and polynomial time strong normalization. Archive for Mathematical Logic, 46, No. 3-4, pp. 253-280, 2007.
  10. Kazushige Terui. Which structural rules admit cut elimination? An algebraic criterion. Journal of Symbolic Logic, 72, No. 3, pp. 738-754, 2007.