書き換え論理(rewriting logic)とは,様々な並行計算系を記述するための一般的な枠組みとしてJ.Meseguerによって提案されたものである.これは,代数(の項モデル)とそれに対する基本的な条件付き書き換え規則,そして書き換え規則から新たな書き換え規則を演繹するための推論規則から成る.並行計算系のモデル化として見たとき,代数の元は(空間的な)状態の分散を表現しており,書き換え規則は(時間的な)状態の遷移であり,書き換え規則の演繹及びその同値関係は,演繹の前提である書き換え規則の間で可能な真並行性(true concurrency)を反映するようになっている.このことにより書き換え全体が圏論的構造を取る.

　この体系は強力な記述力を持っており,ラベル付き遷移系,ぺトリネット,Cham,CCSなどの比較的単純な計算系だけでなく,アクター系,並行オブジェクト指向計算系などの複雑な計算系も記述することができる.彼のグループではこの体系に基づいでMaudeと呼ばれるマルチパラダイムプログラミング言語の設計と実装を行っている.また,状態の各部分の書き換えが真並行的であるので,これを生かして項書き換えを効率よく実行できる並列アーキテクチャを設計し,さらに,この枠組みによる記述を大規模な分散計算系にまで拡張することを提案している.また,条件付き書き換え論理は,条件付き等式論理の一般化としてとらえることもできる.実際,可逆な書き換え規則のみからなる書き換え系は等式系と同値となり,この意味で条件付き等式論理を含んでいる.

　この体系のモデルとして,Meseguerは条件付き書き換え理論Rに対して,代数の元と書き換えを函手と自然変換とみなし,条件付き書き換えのモデル化にサブイコライザ(subequalizer)を用いるモデルを構成し,これをRシステムと呼んでいる.そしてさらに2-圏におけるモデルの可能性についても考察を行っている.しかし,実はサブイコライザは2-圏における普通の2-極限にはならないのだが,そのことが議論されていないために,一般の2-圏におけるモデルを構成するまでには至っていない.

　そこで第1章では,まず,条件付き書き換え論理の概要を述べた後,2-圏およびび2-圏における重み付き極限の概念を導入し,サブイコライザが2-圏Catにおけるインサータと呼ばれるある重み付き極限と一致することを示す.このことから条件付き書き換え論理のMeseguerのモデルを2-圏に一般化し,そのモデルに対する健全性と完全性を証明する.

　次に,書き換えを高次元の圏の2-胞として捉えるという手法を様々な書き換え論理に適用して,その圏論的モデルを構築してゆく.まず,Corradini,Gadducci,and Montanariによってある種の逐次実行に相当する(条件のない)平坦書き換え論理(flat rewriting logic)が提案され,我々のものとは少し異なる形でsesqui圏という2次元の圏を用いたモデルが与えられているが,第2章では,その論理を条件付きの場合に拡張した上で,それに前章の手法を適用してsesqui圏を用いたモデルを与える.

　sesqui圏とは大まかに言えば2-圏の公理からinterchange則を取り除いたものであり,豊穣圏(enriched categories)としてみると,Catに入る二つの対称モノイダル閉構造のうちカルテシアン積によるもので豊穣化した圏が2-圏,もう一つの構造で豊穣化した圏がsesqui圏となる.重み付き極限は一般の重み付き極限について定義されるのでここではsesqui圏にinserterと類似の重み付き極限を定義し,それを用いて条件付き書き換えをモデル化する.そしてそのモデルに対する健全性と完全性を証明する.

　次にこれらの結果を踏まえて計算のモデルとして豊穣圏を使うというアイデアの拡張を試みる.小2-圏と2-函手からなる圏にはいくつかの対称モノイダル構造が入る.それらをSGray,Gray,Gray’とおいてそれらによる豊穣化を行うとそれらは3次元の圏となるが,3-胞の表すものが異なる.これらのモデルでは2-次元までの圏構造はsesqui圏モデルと同様のものを表すが,3-胞は,SGrayの場合,2-圏モデルで同一視されるような書き換え列の間の同値関係を与えるものとなる.Grayの場合は3-胞が外側優先の書き換えを示すような書き換え列間の順序を表し,Gray’の場合は内側優先の書き換えを表すものとなる.

　第3章では,書き換え論理の別の変形と拡張を考える.書き換え論理は等式論理を真に含む柔軟な体系であるが,さらに必要と思われる機能もある.例えばオブジェクト指向計算系においてはオブジェクトの識別と自己参照が重要であるが,これらを直接記述するためには共有と巡回を含むような項を取り扱えることが望ましい.オブジェクトの識別や自己参照は識別子を介して行うのがよく行われる方法であるが,意味論としては,識別子の解析などむしろ実装と考えられる点が入ってくるのであまり望ましくない.参照の取り扱いもかなり面倒である.むしろ共有と巡回を直接取り扱えるようなモデルを与える方が意味論としては単純になる.そこで,そのような特徴を持つ巡回書き換え論理(cyclic rewriting logic)を考えて圏論的な意味を与える.

　巡回書き換え論理は書き換えの順序構造のみを捉える形で,明示はされていないが長谷川真人の学位論文に現れている.ここでは,書き換えを2-胞とみなし一般の2-圏によるモデルが与えられるようにその定義を拡張する.巡回と共有の両方を表すための構文としてletrecを用い,代入もletrecを用いて表現することにして構文を単純化する.

　一方で共有と巡回を持つ項を圏論的にどのように表すかを考える.先行研究としてはGadduciとCorradiniの研究とやはり長谷川の研究が挙げられる.GadduciとCorradiniはストリクトな対称モノイダル圏に複製と消去の二つの機能に対応する結合子を導入しそれらに対する公理を与えることにより,共有をモデル化している.一方,長谷川はカルテシアン圏からストリクトな対称モノイダル圏への函手により共有をモデル化している.しかし両者の共有の表現は実は本質的に同じ考えに基づいている.

　さらに長谷川は巡回を表現するのにtraced monoidal categoryの構造を用いるというアイデアにより上のモデルを拡張して,巡回のモデル化を行っている.一方,GadduciとCorradiniは彼らのモデルを2-圏化して2-胞で書き換えを表現することを行っている.ただしそこでは書き換え論理については取り扱っていない.

　ここではこれらの両者の特徴を取り入れて巡回書き換え論理のモデルを構築する.まず共有を表現するにはGadduciとCorradiniの手法と同様に複製と消去の二つの機能に対応する結合子とそれらに対する公理を与える,そして巡回を記述するには長谷川のアイデアに基づきトレース付きモノイダル圏の構造を導入する.また書き換えは2-胞として表現し,全体が2-圏をなすものとする.これらの要請を満たすような2-圏として我々はtraced gs-monoidal2-圏を定義する.そしてこの2-圏を用いてモデルと翻訳を定義し,健全性と完全性を証明する.

　第2部においては弱高次元圏の理論の現状および理論を構築するために著者が行ったいくつかの試みを述べる.これまで見てきたように高次元の圏の理論は書き換えをモデル化するための基礎理論として重要と考えられる.ストリクトな場合のn-圏は[n-1]-次元の小圏全体からなる圏により豊穣化された圏と見なすことにより比較的良く理解されているが,ストリクトでない(弱い)高次元の圏の理論は実はまだよく分かっていない.弱高次元の圏の定義すらまだ決定的なものが与えられていない.

　弱高次元の定義として現状で有望なものにJ.BaezとJ.Dolanが与えたn-圏の定義が挙げられる.彼らの定義では型付きオペラッドと呼ばれる数学的道具を導入してからそれらを用いて定義しているが,しかし彼らの定義には型付きオペラッドの代数に対する作用についての議論が不正確なところがあり,また一方でglobularityを表現するために必要となる組み合わせ的対象についての議論が不十分である.

　そこで第5章では型付きオペラッドを使わずに,組み合わせ的議論によりBaez-Dolan型の弱高次元圏を定義する.まず圏の基底グラフに対応する対象として弱高次元圏に対しgrafting towerと呼ばれる対象を帰納的に定義する.そしてそれらに対し,universalityとbalancednessという概念を対称な形で相互余帰納的に定義する.そしてこれらの概念を用いて弱高次元圏を定義する.これは合成や恒等射を持ち適切な公理をみたすグラフを圏と定義することに対応すると考えてよい.我々の定義ではBaez-Dolanのものと異なり有限次元だけでなく可算無限次元まで自然に定義される.

　本論文は5章より成る.第1章では書き換え論理の2-圏に基づく圏論的意味論が提示され,その健全性と完全性が証明されている.第2章では,モデルとしてsesqui圏を採用することにより,書き換え論理に対するより精密な意味論が与えられる.第3章では,共有と巡回を含む書き換え理論と,traced gs-monoidal2-圏を用いた圏論的意味論が提示される.第5章では,2-圏だけでなく,一般の高次元の圏に関する理論が述べられている.

　書き換え論理(rewriting logic)とは,様々な並行計算系を記述するための一般的な枠組みとしてJ.Meseguerによって提案されたものである.また,条件付き書き換え論理は,条件付き等式論理の一般化としてとらえることもできる.Meseguerは,代数の元と書き換えを函手と自然変換とみなし,サブイコライザ(subequalizer)を用いて条件付き書き換えのモデルを構成した.さらに2-圏におけるモデルの可能性についても考察を行っている.しかし,実はサブイコライザは2-圏における普通の2-極限にはならないのだが,そのことが議論されていないために,一般の2-圏におけるモデルを構成するまでには至っていない.

　第1章では,まず,条件付き書き換え論理の概要が述べられた後,2-圏およびび2-圏における重み付き極限の概念が導入され,サブイコライザが2-圏Catにおけるインサータと呼ばれるある重み付き極限と一致することが示される.このことから条件付き書き換え論理のMeseguerのモデルが2-圏に一般化され,そのモデルに対する健全性と完全性が証明される.

　次に,第2章では,sesqui圏を採用することにより,書き換え論理に対するより精密な意味論が与えられる.平坦書き換え論理(flat rewriting logic)を条件付きの場合に拡張した上で,それに前章の手法を適用してsesqui圏を用いたモデルが構成される.次にこれらの結果を踏まえて計算のモデルとして豊穣圏を使うというアイデアの拡張が試みられている.小2-圏と2-函手からなる圏にはいくつかの対称モノイダル構造が入る.それらをSGray,Gray,Gray’とおいてそれらによる豊穣化(enrich)を行うとそれらは3次元の圏となるが,3-胞の表すものが異なる.これらのモデルでは2-次元までの圏構造はsesqui圏モデルと同様のものを表すが,3-胞は,SGrayの場合,2-圏モデルで同一視されるような書き換え列の間の同値関係を与えるものとなる.Grayの場合は3-胞が外側優先の書き換えを示すような書き換え列間の順序を表し,Gray’の場合は内側優先の書き換えを表すものとなる.

　第3章では,書き換え論理の別の変形と拡張が与えられる.書き換え論理は等式論理を真に含む柔軟な体系であるが,さらに必要と思われる機能もある.例えばオブジェクト指向計算系においてはオブジェクトの識別と自己参照が重要であるが,これらを直接記述するためには共有と巡回を含むような項を取り扱えることが望ましい.そこで,そのような特徴を持つ巡回書き換え論理(cyclic rewriting logic)と圏論的な意味が与えられている.まず共有を表現するには複製と消去の二つの機能に対応する結合子とそれらに対する公理が与えられる.そして巡回を記述するためにはtraced gs-monoidal2-圏が定義される.そしてこの2-圏を用いてモデルと翻訳が定義され,健全性と完全性が証明されている.

　第5章においては弱高次元圏の理論の現状および理論を構築するために著者が行ったいくつかの試みが述べられている.これまで見てきたように高次元の圏の理論は書き換えをモデル化するための基礎理論として重要と考えられる.ストリクトな場合のn-圏は[n-1]-次元の小圏全体からなる圏により豊穣化された圏と見なすことにより比較的良く理解されているが,ストリクトでない(弱い)高次元の圏の理論は実はまだよく分かっていない.弱高次元の圏の定義すらまだ決定的なものが与えられていない.弱高次元の定義として現状で有望なものにJ.BaezとJ.Dolanが与えたn-圏の定義が挙げられる.彼らの定義では型付きオペラッドと呼ばれる数学的道具を導入してからそれらを用いて定義しているが,しかし彼らの定義には型付きオペラッドの代数に対する作用についての議論が不正確なところがあり,また一方でglobularityを表現するために必要となる組み合わせ的対象についての議論が不十分である.第5章では型付きオペラッドを使わずに,組み合わせ的議論によりBaez-Dolan型の弱高次元圏が定義される.著者の定義ではBaez-Dolanのものと異なり有限次元だけでなく可算無限次元まで自然に定義される.

　したがって,博士(理学)を授与できると認める.