基本情報

所属
九州大学 マス・フォア・インダストリ研究所 教授
学位
博士(理学) (九州大学)

J-GLOBAL ID
200901071361574209
researchmap会員ID
1000041043

外部リンク

計算について論理的・数学的に考察する研究を行っています. 1930年代 Alan Turingは「チューリング機械」と呼ばれる形式的な計算モデルを構成し, 計算可能性, 万能性に関する計算理論の礎を築きました. 数の計算の実現に計算モデルのテープ上に記述された文字列が重要な役割を果たしました. 計算モデル「有限オートマトン」の研究では1950年代に入り文字列集合の認識機械としての考察が始まり言語との重要な関係が導かれました. その後, 形式言語の研究は「自然言語の機械翻訳」「文献データベース」「人工知能」などの研究へと発展しています.
数学(代数学)は「群」「環」「体」などの一種の集合上の演算を持つ代数系を対象とします. 代数系はモナドと呼ばれる圏の間の関手たちにより多種の集合間の関数を演算として持つ系に一般化されます. 多種代数系は「スタック」「木」「グラフ」などのプログラミングに必要なデータ構造を含みますので, 多種代数系やモナドの研究成果は計算の性質を考察するための強力な武器になります.
近年の計算機の発展と普及により, 社会システムは計算機(プログラム)にますます依存して来ています. システムに要求される仕様プログラムで実現し計算機で実行します. プログラムが仕様を正しく実現していることは, 数理論理学において証明定理を正しく導いていることに対応します. 論理的に誤りがないプログラムのための仕様記述, 開発, 検証の技術は形式手法と呼ばれます. 証券取引, 交通網, 航空宇宙工学, マイクロプロセッサなどプログラムの誤りにより多大な損失が生じるシステムに形式手法は活用されています.
最近は論理的・数学的な考察そのものにも計算機が利用され, 形式手法のための数学理論の構築と実現がますます重要になっています. 数の取り扱いのための文字列の研究のように, 計算に必要な数学概念の計算モデルの研究を続けています. 最近では, デジタル映像分野における計算のための新しい計算モデルも模索しています.


主要な論文

  14

主要なMISC

  24

主要な講演・口頭発表等

  16

Works(作品等)

  5

共同研究・競争的資金等の研究課題

  17

委員歴

  4

学術貢献活動

  12

社会貢献活動

  5