近年，ハードウェアやソフトウェアの不具合発見のために，数理的技法が使われてきている．とくにモデル検査という数理的技法では，検査したいシステムを状態遷移系として定式化し，検査したい性質を時相論理式として定式化しさえすれば，後は全自動で検査可能である．そのため，ハードウェアやソフトウェアの開発工程に取り入れられやすい．しかし，検査の仕組みが基本的に状態の網羅的探索であるため，大きすぎる状態遷移系の検査は現実的時間で終了しない．また，複雑すぎるシステムをそのまま定式化すると，定式化の時点で間違いが起こりやすい．そこで，システムのうち，検査に必要な情報だけを抽出して定式化する手法が必要とされる．これが抽象化と呼ばれている技法である．

この論文の目的は，その抽象化という技法を定式化することである．従来研究では，状態遷移系の性質を記述するための論理として，様相命題論理，CTL，様相μ計算，などが研究されてきた． 一方，論理とは独立に，抽象化技法の理論的枠組みとして，模倣，抽象解釈，詳細化といった数学的概念も研究されてきた．そして，各概念が，各論理の論理式を保存するかどうかが個別に議論されてきた．そのため，まだ発見されていない有効な抽象化技法があると考えられる．そこで我々は，この論文で，抽象化概念の研究を論理の意味論の研究の中に統一的に位置づける．すなわち，抽象化の概念は，論理を明示的に与えられた後にそれに対して定義されるべきということである．そのアイデアに従い，論理をできるだけ一般的な論理で固定し，その論理式を保存する抽象化の十分条件を，より一般的に求める．

我々の定式化の基本的なアプローチは，代数的アプローチである．論理と代数の間の関係は，長年研究されている．代数的意味論では，論理 L に対してある代数構造 T L を与え，T L 代数を用いて論理 L の解釈を与える．その際，L の構文や形式的体系が，自由 T L 代数（特にリンデンバウム代数とも呼ばれる）をなすような T L をとることが重要である．というのも，そのことから，この意味論の健全性，完全性は直ちに証明できるからである．例として，古典命題論理，直観主義命題論理，様相命題論理には，それぞれブール代数，ハイティンク代数，様相代数といった代数構造が対応することが知られている．

Chapter1では，以上のような背景を述べ，本研究の位置づけと貢献についてまとめる．本論文の構成についても述べる．

Chapter2では，Lawvere理論の概念を拡張し，Lawvere A理論の定義を与える． Lawvere理論は等式理論で記述される代数構造の多くを例にもつ．我々はこれを拡張し，豊穣圏の上の代数構造を例に持つようにする．この論文の残りの Chapterでは，圏の上の代数構造や2-圏の上の代数構造をいくつか与えるが，我々はそのための統一的な道具としてLawvere A理論を用いる．

Chapter3では，様相不動点論理 Rμ と，代数構造 RMu を与える．代数構造 RMu を与えるために，通常の意味の代数構造の一般化である，圏の上の代数構造という概念を用いる．圏の上の代数構造を用いれば，クリーネ代数の一般化であるクリーネ圏を，局所順序圏の圏の上の代数構造とみなすことができる．ここで局所順序圏の圏とは，局所順序圏を対象とし，局所順序函手を射とするような，圏のことである．これを参考に，クリーネ圏の構造を弱めたものに，束や最大不動点演算の構造を入れたものを RMu 代数とする．Rμ の解釈は，RMu 代数を用いて定義する．そして Rμ の構文と形式的体系が自由 RMu 代数をなすことを示し，そのことによって健全性，完全性を直ちに示す．様相不動点論理に対応する代数構造を与えることは従来では困難だと思われていたが，この論文では，一般化された代数構造の概念を用いることにより，それを解決した．これがこの論文の第一の貢献である．

Chapter4では，その論理における抽象化の，自然な定義を与える．我々は 2-圏の概念を用いる．2-圏は，射の間に 2-cell という構造が入った圏である．また，2-圏の上の代数構造の概念も知られており，圏の上の代数構造の自然な拡張になっている．そこで，局所順序圏の2-圏で，右随伴緩変換を2-cellとするものを考え， その 2-cell を抽象化の定義とする．すると，局所順序圏の圏の上の代数構造 RMu をその 2-圏の上の代数構造に一意的に拡張できることがわかる．さらにその自由代数を用いると，抽象化による論理式保存定理も直ちに示すことができる． また，具体解釈から抽象化と抽象解釈を構成できる可能性についても論じる．状態遷移系のモデル検査などの応用例では，具体解釈から，抽象解釈と抽象化を半自動的に構成することが重要となる．我々は，不必要な条件を仮定せず，具体解釈から抽象化と抽象解釈を構成するための十分条件を明らかにする．このように定式化された，論理 Rμ と抽象化は，従来研究の結果の多くを例に持つ．様相記号をパラメータとして変える事によって，抽象化の概念と論理式の全体集合がそれぞれ同時に変化する．そして，どの様相記号の場合も，抽象化はすべての論理式を保存する．このように，抽象化を，論理に依存して定義したことによって，従来の抽象化を含むより統一的な定式化を与えたことが，この論文の第二の貢献である．さらに，この定式化は統一的であるだけでなく，一般化されている．よって，これらは，具体解釈が Kripke モデルであるにもかかわらず，Kripke 構造でない抽象解釈を構成するような新しい構成法も含む． しかし当然，この抽象化はすべての論理式を保存する． この新奇性がこの論文の第三の貢献である．そして，解釈の定義，健全性定理と完全性定理，抽象化の定義，論理式保存の定理が，代数的に深い関係にあることがわかる．この知見が，この論文の第四の貢献である．

Chapter5では，具体解釈を，その構成要素となる部品から構成できる可能性について論じる．たとえば while プログラムの関係意味論では，基本コマンドの意味を定めれば，それを用いたどんなプログラムにも意味が割り当てられる．我々は同様の性質を圏の上の代数構造を用いて示す．まず，完備ファイブレーション，余完備ファイブレーション，ファイバーデカルト閉圏を，函手の圏の上の代数構造として書く．その代数を用いて GLTS（ラベルつき状態遷移系の一般化）代数という代数構造を定義し，その自由 GLTS 代数を GLTS の記述言語体系とみなす．そして GLTS 代数を用いて，GLTS の状態とラベルに対する解釈を定義する．するとただちに，状態とラベルの解釈が，それを用いた任意の GLTS の解釈に一意的に拡張されることを示せる．さらに，状態とラベルの解釈の間に，抽象化を定義する．そのため，函手の2-圏をひとつ与え，代数構造 GLTS をその2-圏の上の代数構造に一意的に拡張できることを示す．その自由代数を用いて，状態とラベルの解釈の間の抽象化も GLTS の解釈の間の抽象化に拡張できることを示す．従来から研究されてきた，データの解釈から決まるプログラムの抽象化は，その例として説明できる．最後に，GLTS の解釈から Rμ の解釈を構成する方法と，GLTS の解釈の間の抽象化から Rμ での抽象化を構成する方法を与える．これらの構成を総合することにより，論理式保存の条件を，さらに分割された問題に帰着できる．

近年，ハードウェアやソフトウェアの不具合発見のために，数理的技法が使われてきている．とくにモデル検査という数理的技法では，検査したいシステムを状態遷移系として定式化し，検査したい性質を時相論理式として定式化しさえすれば，後は全自動で検査可能である．そのため，ハードウェアやソフトウェアの開発工程に取り入れられやすい．しかし，検査の仕組みが基本的に状態の網羅的探索であるため，大きすぎる状態遷移系の検査は現実的時間で終了しない．また，複雑すぎるシステムをそのまま定式化すると，定式化の時点で間違いが起こりやすい．そこで，システムのうち，検査に必要な情報だけを抽出して定式化する手法が必要とされる．これが抽象化と呼ばれている技法である．

この論文の目的は，その抽象化という技法を定式化することである．従来研究では，状態遷移系の性質を記述するための論理として，様相命題論理，CTL，様相μ計算，などが研究されてきた． 一方，論理とは独立に，抽象化技法の理論的枠組みとして，模倣，抽象解釈，詳細化といった数学的概念も研究されてきた．そして，各概念が，各論理の論理式を保存するかどうかが個別に議論されてきた．そのため，まだ発見されていない有効な抽象化技法があると考えられる．この論文では，抽象化概念の研究を論理の意味論の研究の中に統一的に位置づける．すなわち，抽象化の概念は，論理を明示的に与えられた後にそれに対して定義されるべきということである．そのアイデアに従い，論理をできるだけ一般的な論理で固定し，その論理式を保存する抽象化の十分条件を，より一般的に求める．

本論文の定式化の基本的なアプローチは，代数的アプローチである．論理と代数の間の関係は，長年研究されている．代数的意味論では，論理 L に対してある代数構造 T L を与え，T L 代数を用いて論理 L の解釈を与える．その際，L の構文や形式的体系が，自由 T L 代数（特にリンデンバウム代数とも呼ばれる）をなすような T L をとることが重要である．というのも，そのことから，この意味論の健全性，完全性は直ちに証明できるからである．例として，古典命題論理，直観主義命題論理，様相命題論理には，それぞれブール代数，ハイティンク代数，様相代数といった代数構造が対応することが知られている．

Chapter1では，以上のような背景，本研究の位置づけと貢献についてまとめている．本論文の構成についても述べられている．

Chapter2では，Lawvere理論の概念を拡張し，Lawvere A理論の定義を与えている． Lawvere理論は等式理論で記述される代数構造の多くを例にもつ．本論文はこれを拡張し，豊穣圏の上の代数構造を例に持つようにする．本論文の残りの Chapterでは，圏の上の代数構造や2-圏の上の代数構造をいくつか与えているが，そのための統一的な道具としてLawvere A理論を用いている．

Chapter3では，様相不動点論理 Rμ と，代数構造 RMu を与えている．代数構造 RMu を与えるために，通常の意味の代数構造の一般化である，圏の上の代数構造という概念を用いる．圏の上の代数構造を用いれば，クリーネ代数の一般化であるクリーネ圏を，局所順序圏の圏の上の代数構造とみなすことができる．ここで局所順序圏の圏とは，局所順序圏を対象とし，局所順序函手を射とするような，圏のことである．これを参考に，クリーネ圏の構造を弱めたものに，束や最大不動点演算の構造を入れたものを RMu 代数とする．Rμ の解釈は，RMu 代数を用いて定義する．そして Rμ の構文と形式的体系が自由 RMu 代数をなすことを示し，そのことによって健全性，完全性を直ちに示す．様相不動点論理に対応する代数構造を与えることは従来では困難だと思われていたが，この論文では，一般化された代数構造の概念を用いることにより，それを解決した．これがこの論文の第一の貢献である．

Chapter4では，その論理における抽象化の，自然な定義を与える．ここでは 2-圏の概念を用いている．2-圏は，射の間に 2-cell という構造が入った圏である．また，2-圏の上の代数構造の概念も知られており，圏の上の代数構造の自然な拡張になっている．そこで，局所順序圏の2-圏で，右随伴緩変換を2-cellとするものを考え， その 2-cell を抽象化の定義とする．すると，局所順序圏の圏の上の代数構造 RMu をその 2-圏の上の代数構造に一意的に拡張できることがわかる．さらにその自由代数を用いると，抽象化による論理式保存定理も直ちに示すことができる． また，具体解釈から抽象化と抽象解釈を構成できる可能性についても論じる．状態遷移系のモデル検査などの応用例では，具体解釈から，抽象解釈と抽象化を半自動的に構成することが重要となる．本論文では，不必要な条件を仮定せず，具体解釈から抽象化と抽象解釈を構成するための十分条件を明らかにする．このように定式化された，論理 Rμ と抽象化は，従来研究の結果の多くを例に持つ．様相記号をパラメータとして変える事によって，抽象化の概念と論理式の全体集合がそれぞれ同時に変化する．そして，どの様相記号の場合も，抽象化はすべての論理式を保存する．このように，抽象化を，論理に依存して定義したことによって，従来の抽象化を含むより統一的な定式化を与えたことが，この論文の第二の貢献である．さらに，この定式化は統一的であるだけでなく，一般化されている．よって，これらは，具体解釈が Kripke モデルであるにもかかわらず，Kripke 構造でない抽象解釈を構成するような新しい構成法も含む． しかし当然，この抽象化はすべての論理式を保存する． この新奇性がこの論文の第三の貢献である．そして，解釈の定義，健全性定理と完全性定理，抽象化の定義，論理式保存の定理が，代数的に深い関係にあることがわかる．この知見が，この論文の第四の貢献である．

Chapter5では，具体解釈を，その構成要素となる部品から構成できる可能性について論じている．たとえば while プログラムの関係意味論では，基本コマンドの意味を定めれば，それを用いたどんなプログラムにも意味が割り当てられる．本論文では同様の性質を圏の上の代数構造を用いて示している．まず，完備ファイブレーション，余完備ファイブレーション，ファイバーデカルト閉圏を，函手の圏の上の代数構造として書く．その代数を用いて GLTS（ラベルつき状態遷移系の一般化）代数という代数構造を定義し，その自由 GLTS 代数を GLTS の記述言語体系とみなす．そして GLTS 代数を用いて，GLTS の状態とラベルに対する解釈を定義する．するとただちに，状態とラベルの解釈が，それを用いた任意の GLTS の解釈に一意的に拡張されることを示せる．さらに，状態とラベルの解釈の間に，抽象化を定義する．そのため，函手の2-圏をひとつ与え，代数構造 GLTS をその2-圏の上の代数構造に一意的に拡張できることを示す．その自由代数を用いて，状態とラベルの解釈の間の抽象化も GLTS の解釈の間の抽象化に拡張できることを示す．従来から研究されてきた，データの解釈から決まるプログラムの抽象化は，その例として説明できる．最後に，GLTS の解釈から Rμ の解釈を構成する方法と，GLTS の解釈の間の抽象化から Rμ での抽象化を構成する方法を与える．これらの構成を総合することにより，論理式保存の条件を，さらに分割された問題に帰着できることが示された．

よって本論文は博士（情報理工学）の学位請求論文として合格と認められる。