[萩谷研助手さんインタビュー]
お話: 赤間陽二助手
(1996年に収録)
--- 赤間さんへのインタビューのはずが 途中から、偶然そこに通りかかった萩谷先生へのインタビューになっています。 あらかじめ御了承下さい。---
Q この研究室の目指しているものは何でしょうか?

赤間: 山本君、目指しているものは何?

山本: そういわれてもねぇ。

赤間: 鈴木さーん、ちょっと。えっと、いまD3の鈴木さんです。

Q この研究室で目指していることを伺っているんですけど?

鈴木: 私は本流ではないので…。多分、そこにいる山本君が一番詳しいのではないで しょうか。

山本: 私が本流なんでしょうか。^^;

Q じゃあ、具体的な話を先にして、話を進めたあとで、ということで

赤間: すみません。お願いします。

Q 具体的にこの研究室で進めているプロジェクトはどのようなものですか?

赤間: 関数型プログラミング言語の研究と、…

--- 萩谷先生登場 ---

赤間: 最初、この研究室の目指しているものはなんでしょうかって聞かれてどぎまぎ してしまいましたよ。この研究室のプロジェクトは何でしょう?

萩谷: 関数型言語、および論理型も多少は入るんですけど、そういう宣言的なプログ ラミング言語を中心に、型理論、カテゴリー理論、リニアロジックなどをベー スにした、プログラミング言語の基礎理論をやっております。変換とか導出み たいな理論も興味があってやってます。

もう一つは、定理証明とか証明検査の話で、形式的な証明というものをどうやっ て計算機で扱うかというのが1つの大きな柱で、それ自身1つの目標にもなって いるんですが、応用分野としては、形式的手法・プログラムの検証とか、あと プログラムの合成というものがあります。

これには研究のポイントが2つあって、1つは、形式化がしにくいような数学的 な概念をどうやって形式化するか、もう1つは、実際に定理を発見したりする、 要するに数学的思考をやっている段階で計算機の支援をやりたい、というもの です。2番目の視点っていうのは、数学の定理の間違いを見つけたりとか新し い定理を発見したりとか、そういうまだ定理のない段階で定理証明とかのツー ルを使って数学的な活動を支援したい、と。そういう2つの視点で研究をやっ ていますが、一般的には定理証明とか形式的手法とかいう分野として分類され ています。

もう一つ、ユーザインターフェース(UI)の話があって、今言った、数学的な思 考を支援する計算機環境というものに興味があるんですが、その1つの側面と して UI があります。UI はすごく面白い分野なので、もうちょっと広くやっ てもいいと思ってはいるのですが。

この UI に関して BoomBorg プロジェクトというのをやっていて、プログラム とか証明を作る環境を作る1つの方針として、文書編集のプロセスの中で自然 な形でプログラミングとか証明の構築をやろう、というのがこのプロジェクト の目標の1つです。

これについては、ホームページに説明がありますし…

Q これで何ができるかというのを教えていただけますか?

Boomborg 自身はある種のパラダイムというか、アプローチの仕方を言ってい て、実際にいくつか「もの」を作っているのですが、じゃあデモでもしましょ うか。

--- デモへ ---

これは、BoomBorg-Keisan といって、我々はフリーフォーマットのスプレッド シートと呼んでいるんですけれども、裏にそれなりの考えがあって、つまり、 エディタで編集しながら一緒に計算もやっていくと、結局、計算トレースを実 際に作れるわけです。これに対して繰り返しを表す記号を入れてやると、この 計算トレースがある意味でプログラムと思えるわけです。広い意味でプログラ ム合成システムといえるでしょう。検証とか証明とかそういう作業をこういう 環境の上でやろうというのが Boomborgプロジェクトと呼んでいるものなんで す。これはまあ、UI の分野なのですが、僕自身としては、定理証明とかの分 野と結び付けて考えたい、と。

あと、ゲノム情報というのがあります。これは他と少し毛色が違うのですが、 僕自身が興味があるは、形式的数学が数学的な知識をいかに計算機上で表現す るかということであるとすると、このゲノム情報で興味があるのは、「生物的 知識をどういう風に計算機上で表現しようか」ということなんです。感じとし ては、我々はソフトウェアとかハードウェアみたいな人工物を作って理解して ますよね、そういうものと同じような視点で生物というものも捉えられないか、 と思っています。

Q 先ほどの質問に戻りますが、目指しているものというと?

いや、ここは研究室の体(テイ)をなしていないので。別に、それぞれの人が勝 手にやればいいじゃないですか(笑)。私の目指しているものはございますが、 研究室としての目指すものはあまりありません。

一応、形式化の理論と応用、ということにしておきましょうか。いいじゃない ですかー、そういういい加減な研究室があっても(笑)。あと、プログラミング 言語の話とか、まあ、いろいろあります。

Q この研究室に来ると他と違って何かができるというものはありますか?

技術的には、検証系とか集めていて、そういうことに興味のある人はいいんじゃ ないかと。でも、理論的な話って、どこでもできるし…。

ここに来るといやというほど証明を書かされます(笑)。

関数型言語の関係とかやるにも環境としていいのではないかと思います。

Q どういう人は来て欲しいあるいは来て欲しくないですか?

何やりたいか分かんない人は来て欲しくない(笑)。「何でもやる」ならいいの かなあ。何でもやるって言って、で、こういうのやったらどうかって言って、 ちゃんとやる人はいいなぁ。こういうのどうですかって言って、やってもやん なっちゃって、こういうのどうですかって言ってもやんなっちゃって、結局な んにもやってくれない人は一番困ってしまいます。…って、そんなのどの研究 室でも同じじゃないですかー(笑)。

Q この研究室に来るならこういうのを勉強しておいた方がいい、 というのはありますか?

これは何をやるかにもよるんですけど、

検証の話はプログラミングに近いので、プログラミング能力は必要でしょう。 欲をいえば、プログラミング能力 + ちゃんと理論立てて議論していく能力が あると嬉しいですね。

理論的な分野は、自分の世界というものがないとやっていけませんね。たとえ ば「世の中はすべてカテゴリーだ」とかいうのでもいいですが、人に何をいわ れようが、その道を行く人じゃないと。

Q 高校生に一言お願いします。

赤間: 何かかっちょいいこと言わないとなー。

萩谷: 何なんでしょう。知の論理、とかいって。まあ、言いたいことは今まで言って きたようなことで、別に高校生だからといって特にどうとかいうことはありま せんね。

赤間: ちゃんと勉強しよう、とか、それぐらいしかないなあ。

Q 昔からやっているのは、どのような分野ですか?

萩谷: この研究室、そんなに古くないですから。僕がやってきたのは、関数型言語の 理論とか実装とか変換とかの話などです。特に部分計算というものをやってい ました。これもだから、ホームページに書いてあるので、興味があれば、見て ください。

あ、もう1つ全然別の話として、ウィンドウシステムを作っていたこともあり ます。そう、昔 Java のようなものを作っていたことがあるのですよ。でも、 あれは 80年代の技術なので、是非、90年代は新しいことをやりたいな、と。

Q 一歩先を行っている、というわけですね?

一歩先を行きたい。いや、ちょっと考えていることがあるんですが、まだ秘 密(笑)。すみません。


戻る