本文へジャンプ

計算から論証へ

石原研究室 ISHIHARA Laboratory
教授:石原 哉(Ishihara Hajime)

E-mail:ishiharajaist.ac.jp
[研究分野]
情報科学・情報学基礎・数理論理学・計算理論
[キーワード]
直観主義論理、構成的数学、証明論、逆数学

研究を始めるのに必要な知識・能力

数学としては高校・大学初年程度で学習する(数学的)帰納法や集合に関する理解、発展的には授業科目「基礎論理数学」に関する理解、しかし何よりも数学を使って世界を理解することに興味を持っていること。

この研究で身につく能力

この研究で身につく能力を一言でいうと「論証」力である。高校や大学では、計算や式の変形によって解答を導くことが多かったと思うが、それとは次元の異なる問題解決の手法である論証を自由に使いこなすことを目指す。基礎的な英語の教科書を読むことを通して、論証を身につけるとともに数学をはじめとする理論分野の文献を正しく読む力を養う。ついでに、英語の文献を読む能力を養う。また、論証を「証明」として書き下す経験を通して、論理的に表現する能力や論理的な文章を書く能力を身につける。さらに、研究発表においては(論理的な)プレゼンテーション能力の訓練を行う。

【就職先企業・職種】 情報通信・情報処理・出版など

研究内容

 数学と情報科学にまたがる学際的領域の研究を行っています。数学としては、数理論理学、数学基礎論、情報科学としては、数理情報科学、理論計算機科学に分類されます。特に、構成的数学、数理論理学、計算の理論を中心に研究を行っています。

構成的数学

 ある解を求めるコンピュータ・プログラムはその解の存在の証明と見ることができます。しかしながら、通常の数学での解の存在証明はその解を求めるプログラムが実装できることを保証しません。解の存在証明がそのまま解を求めるプログラムに対応する数学として構成的数学があります。構成的数学は、Brouwerの直観主義数学に始まり、HeytingやKolmogorovにより形式化された直観主義論理を用いています。Hilbert空間、Banach空間、超関数論などの関数解析学や、その基礎を与えるneighbourhood space、formal topology、basic pairなどの位相空間論を構成的数学の枠組みで研究しています。また、構成的数学の基礎付けとして、構成的集合論、特にMartin-Löfの型理論で自然に解釈できる可術的な集合論CZFを中心に研究を行っています。さらに、通常の数学(古典的数学)、Brouwerの直観主義数学、Markovの構成的数学など様々な哲学のもとに展開された数学を、統一的な視点から論理的原理や関数の存在公理により分類し、整理し、体系化することを目指して構成的逆数学を提唱し、研究を推進しています。

数理論理学

 構成的数学で用いる直観主義論理の証明論や意味論を研究しています。直観主義論理の証明とプログラム(ラムダ計算の項)の間には、Curry-Howardの対応と呼ばれる自然な対応があり、証明からプログラムを合成できます。そのためのシステム(ミュンヘン大学のMinlogシステムなど)が開発されています。古典論理と直観主義論理の関係を明らかにし、古典論理の証明から直観主義論理の証明を取り出し、プログラム合成を行うための基礎研究を行っています。また、線形論理に代表される、部分構造論理の証明論や意味論の研究も行っています。

計算の理論

 計算可能性理論や計算の複雑さ理論の研究と、それらと構成的数学の関係の研究を行っています。多項式時間計算可能関数などの計算可能関数のfunction algebraによる特徴づけ、計算の複雑さや決定不可能次数と構成的逆数学における論理的原理や関数の存在公理の関係を明らかにする研究を目指しています。また、ラムダ計算と単純型、共通部分型、和集合型などの型理論の研究も行っています。

主な研究業績

  1. Hajime Ishihara and Takako Nemoto, A note on the independence of premiss rule, MLQ Math. Log. Q. 62 (2016), 72-76.
  2. Hajime Ishihara and Tatsuji Kawai, Completeness and cocompleteness of the categories of basic pairs and concrete spaces, Math. Structures Comput. Sci. 25(2015), 1626-1648.
  3. Hajime Ishihara,Some conservative extension results on classical and intuitionistic sequent calculi,In: U. Berger et al. eds., Logic, Construction, Computation, Ontos Verlag, 2012, 289-304

研究室の指導方針

本研究室は学問をする場です。研究室が組織として研究課題を決め研究費・学生を配して研究を進めてはいません。研究はメンバーの社会への貢献に対する責任の自覚に基づいた、情熱と自由な発想によって行われています。研究室として行うセミナーは、論証力・表現力を身につけることに重点を置いています。また、研究の成果は社会に論文・講演などの形で公表しなくてはなりません。社会に広く受け入れられ、利用される形で公表するための、文章表現、口頭表現などプレゼンテーション技術などの表現を身につけることを目指しています。

[研究室HP] URL:http://www.jaist.ac.jp/is/labs/ishihara-lab/www/index.html

ページの先頭へもどる