藤田研究室 Fujita Lab.

群馬大学理工学部電子情報理工学科6号館6F

研究

モデル検査技法を活用した化学反応の解析: 線維芽細胞増殖因子FGF/FGFR生化学反応の過渡特性

state-machine

Church--Rosserの定理の計算量的複雑さ: 計算のステップ数,計算の道(軌跡)の長さと本数

Church--Rosserの定理(AMS1936)は,等式と計算(簡約)をつなぐ重要な性質を述べています. この存在定理が主張する合流点に至るまでに必要な計算ステップ数の上限について解析をしました.ここで,Grzegorczyk階層のレベル5に属する原始帰納的関数が上限を与えると予想されていました.ところが,この階層のレベル4に属する帰納的関数で抑えられることが明らかになりました.

研究成果の概要

合流性: 計算結果の一意性,道は枝分かれしてもその後いつかは交わる!

簡約グラフ: 計算の道・軌跡はどんな図形?

「ラムダ計算 = 図形・グラフ記述言語」,「ラムダ式 = 図形・グラフ描画プログラム」の新しい観点から研究しています.

型検査・型推論問題の決定可能性: 計算可能・計算不可能の境界

ラムダ式の定式化にはチャーチ流とカリー流{*1}の二種類の流儀が伝統的にあります. ここで,2階ラムダ計算(ポリモルフィックラムダ計算,多相型ラムダ計算)の型検査問題は,チャーチ流では決定可能であるがカリー流では決定不能になることが知られていました.そこで, カリー流とチャーチ流の中間的構造を持つラムダ式を系統的に導入して, ラムダ式中の どの情報が型問題の可解性・非可解性を本質的に特徴付けているのか解明してきました.
{*1}: カリーのファーストネイムはHaskell(1900--1982)です.あの関数型プログラミング言語の名前は彼のファーストネイムからもらったそうです.1993年のChalmers University of Technology(Sweden)滞在時にそのような経緯を教えてもらいました.

研究の枠組みと全体像

2階命題論理のモデルと証明可能性問題: 決定可能・決定不可能の境界

2階古典命題論理は決定可能です(PSPACE-complete). 一方,2階直観主義命題論理の論理式が証明可能かどうかの判定問題は一般的には 決定不能です.しかし,決定可能となる興味深い部分体系が幾つか発見されています.

直観主義論理のモデルとしてハイティング代数とクリプキモデル,及びその双対性が良く知られています.実際,ハイティング代数の素イディアルから可能世界が生成され,また可能世界の上に閉じている集合の族からハイティング代数が構成されます.さらに任意のハイティング代数は,イディアル完備化により完備なハイティング代数に埋め込まれて直観主義一階述語論理のモデルになります.Sobolev (1977)は2階直観主義命題論理のクリプキモデル(位相的モデル)を与えましたが,それに双対な束論的モデルとはどのようなモデルでしょうか?

カリー・ハワード同型: 論理体系と型付きラムダ計算の関係

直観主義論理と型付きラムダ計算の密接な関係はカリー・ハワード同型 (Propositions-as-Types, Formulae-as-Types, Proofs-as-Programs)と呼ばれています.この関係は,プログラムの生成・検証,プログラミング言語の設計などに応用されています.この観点から,論理学,ラムダ計算,プログラミング言語を対象に次の性質について明らかにしてきました.

(1) 高階多ソート直観主義述語論理とPTS(Pure Type System)との詳細な関係(Formulae-as-types)

(2) 古典論理から直観主義論理への埋め込みと計算戦略
(G \"{o}del-Gentzen, Kolmogorov, Kuroda negative-translations と call-by-name, call-by-value lambda-mu-calculi) (3) 古典論理の証明の計算的・プログラム的意味(Proofs-as-programs) (4) 複数の結論を持つ自然演繹体系と通信計算体系(Multiple-conclusion system, Communication calculus) (5) lambda計算,lambda-mu計算の継続による意味付け(Continuation, CPS-translation) (6) 多相型と抽象データ型の双対性(Polymorphic type, abstract data type, adjoint)
関連文献,参考図書:Logic, Lambda Calculi, Curry-Howard isomorphism

科学研究費 KAKEN