メンバー

TOP > メンバー > 照井 一成

照井 一成

名前照井 一成 (Terui, Kazushige)
准教授
E-Mailterui (emailアドレスには@kurims.kyoto-u.ac.jp をつけてください)
研究内容数理論理学の研究
紹 介

 数理論理学の中でもコンピュータ科学と関係の深い部分の研究を行っている。 中でも興味あるのが(構造的)証明論である。証明は数学の手段であるが、 同時に数学の対象でもありうる。実際、 適切な表示を与えれば背後にある数学的構造が浮かび上がってくる。 また証明は、カリー・ハワード対応のもとで関数型プログラムと(ある程度) 同一視できることが知られている。それゆえ証明は 「正しさの保証」という静的側面に加えて、 「計算の媒体」としての動的側面も兼ね備えている。
多様な側面をもつ証明を理解するために、計算複雑性[1,5]、 ゲーム[2]、表示意味論、 代数意味論等さまざまな観点から研究を行っている。 具体的な研究成果は以下の通りである。
1. 非古典論理の代数的証明論を提唱し、 順序代数と証明論の対応関係を調べている[4,7,8]。 たとえば順序代数の完備化は、適切に一般化 すれば証明のカット除去に相当し、論理式の 複雑さを制限すれば正確な一致を証明する ことができる。この種の対応関係を調べることで、 順序代数の技法と証明論の技法が双方向に 利用可能になるというのが主眼である。
2. 論文[3]では、 単純型つきラムダ計算(直観主義命題論理) の計算複雑性について正確な特徴づけを 行った。重要なのは線形論理のスコット意味論 という表示意味論を用いている点である。意味論的評価により 単純な記号の書き換え(プログラム実行) では達成できない高速な計算が可能になり、計算複雑性の上限が 与えられる。
3. 最近の研究としては、伝統的証明論(順序数解析)における 重要技法の1つであるΩ規則をラムダ計算や構造的証明論の 文脈に取り込み、代数的解釈を与えたことが挙げられる[6,9]。 Ω規則の代数化により、算術理論における帰納的定義の階層(の一部)が 二階述語論理の階層と正確に一致することを示すのに成功した。

  1. Patrick Baillot and Kazushige Terui. Light types for polynomial time computation in lambda calculus. Inf. Comput, 207(1): 41-62, 2009.
  2. Kazushige Terui. Computational ludics. Theor. Comput. Sci. 412(20): 2048-2071, 2011.
  3. 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.
  4. 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.
  5. Damiano Mazza and Kazushige Terui. Parsimonious Types and Non-uniform Computation. Proceedings of ICALP 2015, 350-361, 2015.
  6. Ryota Akiyoshi and Kazushige Terui. Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule. Proceedings of FSCD 2016, 5:1-5:15, 2012.
  7. Paolo Baldi and Kazushige Terui. Densification of FL chains via residuated frames. Algebra Universalis, 75(2): 169-195, 2016.
  8. Agata Ciabattoni, Nikolaos Galatos and Kazushige Terui. Algebraic proof theory: Hypersequents and hypercompletions. Ann. Pure Appl. Logic, 168(3): 693-737, 2017.
  9. Kazushige Terui. MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics. Proceedings of CSL 2018, 37:1-19, 2018.
  10. 照井一成.コンピュータは数学者になれるのか  数学基礎論から証明とプログラムの理論へ, 青土社,2015年.

← BACK TO THE TOP

← BACK TO THE TOP

  • Follow on

Research Institute for Mathematical Sciences (RIMS)