随伴関手を用いた圏論的結合子の導出
スポンサーリンク
概要
- 論文の詳細を見る
圏論的結合子(categorical combinator)はラムダ計算の変数を含まない翻訳であることから,圏論的解釈を利用した関数型言語の実装に用いられている.本稿では圏の構造を随伴関手(adjoint functor)で定義することで,圏論的結合子とその等式が圏論の基本概念から天下り的に導かれることを示す.圏論的結合子は随伴関手に付随する自然変換である単因子(unit)と余単因子(counit)として得られ,その等式は圏,関手,自然変換の定義,および随伴関手の三角可換図(triangular identity)から直接導かれる.まず最初にカルテシアン閉圏(cartesian closed category)のための圏論的結合子の導出について述べ,これを用いた自由圏の構成を示す.そして次に圏論的結合子の非外延的(non-extensional)な等式が半随伴関手(semi-adjoint functor)から導かれることを示す.最後に一般の極限対象(limit object)や再帰的対象(recursive object)について考察し,その際に右随伴関手と左随伴関手の双対性(duality)がどのように作用するかをみる.
- 一般社団法人情報処理学会の論文
- 1995-10-15
著者
関連論文
- PCTE : ソフトウェアツールを移植可能にし, 共通に利用するための環境
- ソフトウエア仕様記述におけるカテゴリ論の応用について
- 部分計算を用いた等式仕様の変換と実行
- 随伴関手を用いた圏論的結合子の導出
- 圏によるソフトウェア意味の可視化 ( 情報の可視化)
- 圏論的結合子の操作的意味について
- 複雑系として技術史を観る
- ソフトウェアプロジェクトにおける協力と協調を支援する計算機環境