数理論理学・形式言語理論分野 応用論理・数理言語学研究室

数理論理学と形式言語理論について研究しています。この２つは、比較的歴史の浅い数学の分野で、コンピュータ科学のための基礎理論にもなっています。実数や関数のような高校数学でおなじみの対象ではなく、記号列の解釈や記号列の集合の規則性の表現などのより抽象的な対象を扱います。研究室では、数理論理学の応用の一つである「証明プログラミング」についても学びます。証明プログラミングとは、数学の定理の証明や、プログラムが仕様を満たしていることの証明を定理証明支援系と呼ばれるソフトウェアを用いて形式的に書き下すことによって、その正しさを保証することです。

数理論理学は数学の厳密化・形式化の流れの中で20世紀前半に確立した分野で、数学基礎論と呼ばれることもありますが、過去数十年はコンピュータ科学へのさまざまな応用を通して新たな形で発展しています。形式言語理論はもともと1950年代に理論言語学の分野で人間の言語やその文法を抽象化し数学的対象として研究しようという考えから始まったものですが、その後コンピュータ科学の中で研究され、プログラミング言語処理系の理論的基盤にもなっています。このように、この分野の基礎理論はコンピュータ科学を通して現実の社会で大いに役立っているものです。研究室で力を入れている証明プログラミングも、ソフトウェアにバグが潜んでいないことを保証する手法として、広く用いられています。