2014 Fiscal Year Annual Research Report
| Project/Area Number |
24700012
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
勝股 審也 京都大学, 数理解析研究所, 助教 (30378963)
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Keywords | モナド / 論理関係 / ファイブレーション |
|---|
| Outline of Annual Research Achievements |
本年度は当初の計画から内容を変更し、TT-liftingの一般化について京都大学数理解析研究の佐藤哲也氏と共同で研究した。TT-liftingはカルテシアン閉構造を保つファイブレーションに沿ってモナドを持ち上げる圏論的技法であり、そのようなファイブレーションは型付きラムダ計算の論理関係を圏論的に定式化する際にしばしば現れるが、一方で「ファイブレーションが閉構造を保つ」という条件はTT-liftingの適用範囲を狭めていた。
状態遷移系を圏論的に扱う余代数の分野では、様相演算子および(双)模倣関係を、述語の圏および関係の圏からのファイブレーションに沿った余代数関手の持ち上げにより扱うことがある。多くの場合、余代数関手はモナドの関手部分を含むため、モナドの持ち上げ問題は余代数関手の持ち上げの問題の重要な部分となっている。しかしながら余代数では閉構造を持たない圏も扱うため、TT-liftingを適用できない状況が見られる。
この適用範囲に関する問題は、TT-liftingが閉構造に依存している事が原因である。そこで、本年度は「閉構造を用いないTT-lifting」を開発した。TT-liftingは継続モナドの持ち上げを標準的なモナド射(Haskellのbindに相当)で引き戻すという手順を踏む。この手順において、継続モナドを余稠密モナドで置き換え、右Kan拡張がファイブレーションで保たれると仮定することで、閉構造への依存を取り除いた。この状況でもbindの類似物が存在し、これで余稠密モナドを引き戻すことでモナドの持ち上げが導かれた。これを余稠密持ち上げと呼ぶ事にする。余稠密持ち上げは、適切にパラメータを選ぶことで、任意のモナドの持ち上げを導く事が可能である。また余稠密持ち上げは集合の圏の上のモナドを位相空間や可測空間の圏に持ち上げる事ができ(TT-liftingでは不可能であった)、その例をべき集合モナドで計算した。
|
