計算理論・計算モデルを究める

Crossed Point Theorem

計算の理論,世界第1号は1930年頃にチャーチ博士によって作られました。その理論はラムダ計算と呼ばれています。その後、多くの研究者により様々な計算の理論やモデルが提案されてきました。今でも生き残っていてキチントした理屈は全てラムダ計算と同じ能力があります。広く使われている関数型プログラミング言語もこの理論によって支えられています。また、この様な理論のおかげで、計算、プログラム、情報システムなどの動作や性質を調べることができます。
 これまでの研究において、ラムダ式やプログラムの型(タイプ)を求める問題の計算可能性について明らかにしてきました。例えば,ある条件を満たすプログラムに対して、その型を求めるアルゴリズムは存在しますか?また別の条件を満たすプログラムについてはどうですか?という問題です。最近では、計算結果の一意性や無矛盾性に関する定理についても研究しています。(図:Crossed Point Theorem)
 さらに、この様な基礎理論は、情報社会を支えているソフトウェアやシステムの信頼性、安全性を保障するためにも様々な場面で活用・応用されています。