We propose hyper-lambda calculi, the typed lambda calculi based on hypersequent calculi. A hyper-lambda term is a finite sequence of lambda terms, representing concurrent processes. We give two concrete hyper-lambda calculi: synchronous and asynchronous. Both employ a pair of communication primitives exchanging their inputs. In the synchronous case, both sides succeed. In the asynchronous case, at least one side obtains the other side's input. The synchronous calculus implements message-passing communication and session types; the asynchronous calculus characterizes shared-memory waitfree communication. Among processes of a typed hyper-lambda term, all succeed in the synchronous case while at least one succeeds in the asynchronous case. Logically, the processes are interpreted conjunctively in the synchronous case but disjunctively in the asynchronous case. The synchronous calculus is based on Abelian logic: (ϕ ⊸ ψ) ⊗ (ψ ⊸ ϕ) on top of multiplicative additive fragment of intuitionistic linear logic (without some units); the asynchronous calculus is based on Godel–Dummett logic: (ϕ ⊃ ψ) ∨ (ψ ⊃ ϕ) on top of intuitionistic logic. The hyper-lambda calculi are in Curry–Howard correspondence with the deduction systems for these logics. We also treat another variant based on monoidal t-norm logic and an implementation using Haskell.

Meanwhile, we discover a new representation of Abelian logic proofs called Amida nets. Amida nets are based on a special kind of directed graphs called Lamarche's essential nets. On top of Lamarche's essential nets, we add a new kind of undirected edges called Amida edges. Similarly to the Amida lotteries used by Japanese children, when we follow a directed path in an Amida net, whenever we meet an Amida edge, we have to cross the Amida edge. While Lamarche's essential nets characterize fragments of intuitionistic linear logic, our Amida nets characterize Abelian logic. The name Amida calculus comes from the Amida lotteries.

The logics treated in this thesis, Godel–Dummett, monoidal t-norm and Abelian logics were initially developed for algebraic interests, but we reveal that these logics have computational applications as type systems for concurrent processes.

論文の概略

カリー・ハワード対応とは,形式論理における証明と,(ラムダ項に代表されるような,関数型の)プログラムとの間の対応関係のことを指す.これは,論理学と計算・プログラミング言語の理論との間にテクニカルなレベルの橋渡しを与えるのみならず,論理における証明の計算論的解釈を可能にするという,大きな哲学的な意味をも持つ.カリー・ハワード対応のそもそもは直観主義論理と単純型付きラムダ計算の間に1974年に発見されたが,その後さまざまな形に拡張され,盛んに研究されてきた(たとえば古典論理とラムダ・ミュー計算の間のそれなど).本論文はこの研究の流れに,ハイパーシーケント系と並列計算という全く新しい視点を導入するものである.

ハイパーシーケント系はゲーデル・ダメット論理とよばれる論理に対して Avron によって導入された形式的証明系である.シーケント一つだけを導出していく通常のシーケント系とは異なり,シーケントを複数並べたハイパーシーケントを導出していくことに特徴がある.本論文の基本アイデアは,このようなハイパーシーケントにおけるシーケントのそれぞれを,カリー・ハワード対応を通じて一つの計算プロセスと同一視することで,ハイパーシーケントを並列に動作している複数の計算プロセス(ハイパーラムダ項)として解釈することである.

本論文では3つの論理(ゲーデル・ダメット論理,アーベル論理,monoidal t-Norm 論理)について考え,それぞれのハイパーシーケント系と,それらとカリー・ハワード対応するハイパーラムダ計算を導入した.特にゲーデル・ダメット論理については,対応するハイパーラムダ計算が,ちょうど waitfree 計算とよばれる並列計算のクラスと一致することが示される.Waitfree 計算とは並列プロセスの間の同期機構の強さによって特徴づけられる並列計算のクラスであり(「プロセスが他のプロセスの実行を待つ」ことが必要ない計算タスクのクラス),この位相幾何学的特徴付け(Herlihy らによる)が理論計算機科学の主要な賞であるゲーデル賞を2004年に受賞したことからもわかるように,理論・応用の両面から活発な研究の対象となっている.

本論文ではこの他にも種々の結果が示される.たとえばハイパーシーケントと並列計算の間の対応というアイデアから,アーベル論理のためのハイパーシーケントによる新たな証明系が導かれた.ここにおける公理(アミダ公理とよばれる)は,プロセス間の通信が完全に同期されていることを表現しており,並列計算の検証手法の一つであるセッション型のエンコードを可能にしている.また,ハイパーラムダ計算の Haskell による実装も行われ,議論が行われる.

総合評価

並列計算は近年の計算機の使用シナリオにおいて必ず現れる現象であるが(大きなスケールではインターネット,小さなスケールではマルチコア・プロセッサ),その本質的な複雑さゆえに,並列計算を「正しく」動作させることが非常に難しいことが知られている.一方で,型システム(すなわちカリー・ハワード対応)によってプログラムの安全性を保証することはプログラミング言語の理論における基本的な手法である.本論文はこの手法の適用可能性を,ハイパーシーケントと並列プロセスの対応という明確なアイデアをもとにして,応用上重要かつ難しい並列計算の問題に押し広げたものと言える.これは論理学とプログラミング言語の理論,さらに並列計算の理論のすべてにまたがる大きな成果であると考える.

本論文のさらに評価できる点として, (1) 論理・計算双方にわたる理論的な諸結果, (2) 既存の検証手法との対応や実装による応用上の貢献, (3) 多数の既存研究のサーベイによる研究の歴史の中の位置づけ,の3つを通じて,上に述べたアイデアを体系化したことがあげられる.また口頭試問においては,特にカリー・ハワード対応のそれぞれの側面の専門家の両方(論理学の小野教授,プログラミング言語理論の小林教授)からの,詳細かつ視点の異なる多数の質問に対して,候補者は明確かつ建設的な回答・議論を行った.このことも高く評価できる.

以上により本論文は博士(情報理工学)の学位請求論文として合格と認められる。