2006年に東京大学理科一類に入学して2008年に理学部情報科学科に進学しそこから私はコンピュータサイエンスを志すようになった。 数学的思考とは何か分析することに興味を持っていた私は、学科に進学してからはコンピュータ上で数学的推論するプログラムを動かしたいと考えるようになった。
大学4年の冬学期に萩谷研究室に入って研究を始めた。 整数論や初等幾何学の問題を自動で解くようなプログラムを考えるような研究をしたいと考えていた私は、そのような研究を卒業研究で萩谷先生の指導を受けながら行った。 この卒業研究には苦労した。 東大の情報科学科の卒業研究は期間が半年しかないため、基本的に既存の研究を少し拡張するだけという研究をすることが多い。 私もそのように研究を行い、萩谷先生から既存の自動推論の研究を毎週紹介して頂いていた。 ただ毎回紹介された既存研究に対してこんなセンスのない研究の拡張なんてできないと文句を言っていたおかげで、研究を一切進めないまま、締め切りまで残り1,2ヶ月という状態になった。 最終的には、萩谷先生からもう絶対このテーマでやってくれと頼まれながら命題論理の本を渡された。 そして、いくつかの具体的な事実を記述した命題論理式から、一般的な法則を予想し、その予想を表現する命題論理式を出力する自動定理予想プログラムを書いて卒業研究を切り抜けた。
既存の研究にセンスがないと感じた理由は全て推論の表現形式によるものだった。 この卒業研究をしたときに、論理式による推論の表現は、論理自体の性質を論じるのには確かに便利だが、人間の推論を表現するのに適していないという認識を私は得た。 例えば、非常に初歩的な定理である素因数分解の一意性を論理式で記述するのはものすごく大変だ。 このような表現形式の上で推論について考えても意味のある結果は得られないと私は考えた。
そして表現形式のどこに問題があるのか考えた時、集合を扱う表現に大きな問題があると認識した。 集合の扱いを直感的に表現できないから、素因数分解の一意性の定理などのような数学の定理が直感的に表現できないと考えた。 そうして集合のようなデータのパターンマッチも直感的に行える新しい強力なパターンマッチの表現について考え始めたのだった。
[Top]