理論情報科学領域【石原研究室】
■ 研究概要
本研究室では，計算可能性理論，計算の複雑さ理論，数理論理学に関する研究を行うとともに，現代数学の結果を，計算可能性・複雑さ理論の視点から数理論理学を用いて，見直す研究を行っています。また，その研究を推進するため，現代数学で用いる論理（古典論理）より弱い論理（直観主義論理）を用いた構成的数学の研究も行っています。
■ 数学と計算機科学の境界領域
研究分野は，簡単に言えば数学と計算機科学の境界領域に，属しています。
計算できること・できないこと
現代数学で扱う関数には，計算機で原理的に計算できる（計算可能な）ものと，計算できない（計算不可能な）ものがあることが分かっています。実は計算可能な関数は，全体のほんの一握りです。プログラムと入力が与えられたとき，そのプログラムがその入力で停止するか否かの判定（停止性問題）は計算不可能な関数の代表例です。
計算の難しさ・複雑さ
さらに計算不可能な関数にも，その難しさ（不可能さ）に様々なレベルがあること，計算可能な関数にも，その複雑さ（手間）に様々なレベルがあることが分かっています。関数は計算の難しさ・複雑さによって，たくさんのクラスに分類することができます。クラスPやNPは計算の複雑さによる分類です。
証明＝プログラム
ある方程式に解が存在することが証明できたとき，その証明から解を求めるプログラムが取り出せたらすばらしいことです。残念ながら（古典論理を用いた）現代数学でこれはできません。しかし（直観主義論理を用いた）構成的数学ではできます。
定理の計算可能性・複雑さ
現代数学の定理の中には，計算と相性のよい構成的数学で証明できないものがあります。そのような定理を構成的数学で証明するために必要十分な公理を見つける研究があります。定理の証明に必要十分な公理は，その定理の計算の難しさを表していると考えられます。この研究に数理論理学を用いて，現代数学の定理を計算可能性・複雑さにより分類する研究（構成的逆数学）が始まりました。
■ 最近の研究
ちょっと難しくなるかもしれませんが，閉区間［０，１］に対して現代数学で成立する性質・定理を研究しています。完備かつ全有界（CTB），ハイネ−ボレルの定理（HBT），カントルの共通部分定理（CIT），ボルツァノ−ワイエルストラスの定理（BWT），点列コンパクト性（SCP）の５つで，これらの性質・定理は現代数学ではすべて成り立ちますが，構成的数学ではCTB以外成り立ちません。数理論理学を用いて詳しく調べると，実は
SCP ⇒BWT ⇒ CIT ⇒ HBT ⇒ CTB
という関係になっていて，それぞれ異なる計算可能性・複雑さに分類されることが分かってきました。
また，２００３年５月にはイタリアのヴェニスで開催された国際研究集会で，Constructive Reverse Mathematics（構成的逆数学）について講演しました。直観主義発祥地で今も研究が盛んなオランダからの参加者が，直観主義数学の立場から同様の研究を始めたところで，今後意見交換と共同研究を進めることになりました。またドイツ，イタリア，スウェーデン，ルーマニア，ニュージーランドからの参加者とも意見交換をし，将来共同研究を予定しています。
■代表的な著書・論文
- D. Bridges, H. Ishihara, P. Schuster and L. Vita : Strong
continuity implies uniform sequential continuity, Arch. Math,
Logic 44（2005）, 139-153
- L. Crosilla, H. Ishihara, and P. Schuster : On constructing
completions, J. Symbolic Logic 70（2005）, 969-978
- H. Ishihara : Constructive reverse mathematics : compactness
properties, In : L. Crosilla and P. Schuster eds., From Sets
and Types to Analysis and Topology : Towards Practicable Foundations
for Constructive Mathematics, Oxford Univ. Press, 2005, 245-267
- D. Bridges, D. van Dalen and H. Ishihara : Ishihara's proof
technique in constructive analysis, Indag. Math. 14（2003）,
163-168
- H. Ishihara and S. Yoshida : A constructive look at the completeness
of D（R）, J. Symbolic Logic 67（2002）, 1511-1519
