九州大学 論理と計算研究室 関係計算の形式化を用いた数学とソフトウェア検証のための理論構築

Introduction

Yoshihiro Mizoguchi was born in Fukuoka on June 20, 1960. He received B.S. in 1983, the M.S. 1985 in Mathematics and the Dr. Sci. in 1992 in Information Systems from Kyushu University. Presently, he is a professor of Institute of Mathematics for Industry, Kyushu University at Fukuoka. His research interests are theoretical aspects in computer science, including logic of programming language, cellular automata, computer graphics, category theories and network securities.

Cf. Research Information (Kyushu Uiversity, JAPAN)

研究の背景

計算について論理的・数学的に考察する研究を行っています。1930年代 Alan Turingは「チューリング機械」と呼ばれる形式的な計算モデルを構成し、計算可能性、万能性に関する計算理論の礎を築きました。数の計算の実現に計算モデルのテープ上に記述された文字列が重要な役割を果たしました。計算モデル「有限オートマトン」の研究では1950年代に入り文字列集合の認識機械としての考察が始まり言語との重要な関係が導かれました。

その後、形式言語の研究は「自然言語の機械翻訳」「文献データベース」「人工知能」などの研究へと発展しています。数学(代数学)は「群」「環」「体」などの一種の集合上の演算を持つ代数系を対象とします。代数系はモナドと呼ばれる圏の間の関手たちにより多種の集合間の関数を演算として持つ系に一般化されます。多種代数系は「スタック」「木」「グラフ」などのプログラミングに必要なデータ構造を含みますので、多種代数系やモナドの研究成果は計算の性質を考察するための強力な武器になります。

近年の計算機の発展と普及により、社会システムは計算機(プログラム)にますます依存して来ています。システムに要求される仕様をプログラムで実現し計算機で実行します。 プログラムが仕様を正しく実現していることは、数理論理学において証明が定理を正しく導いていることに対応します。論理的に誤りがないプログラムのための仕様記述、開発、検証の技術は形式手法と呼ばれます。証券取引、交通網、航空宇宙工学、マイクロプロセッサなどプログラムの誤りにより多大な損失が生じるシステムに形式手法は活用されています。

最近は論理的・数学的な考察そのものにも計算機が利用され、形式手法のための数学理論の構築と実現がますます重要になっています。数の取り扱いのための文字列の研究のように、計算に必要な数学概念の計算モデルの研究を続けています。最近では、デジタル映像分野における計算のための新しい計算モデルも模索しています。

お知らせ