随伴関手を用いた圏論的結合子の導出  [in Japanese] Deriving Categorical Combinators from Adjoint Functors  [in Japanese]

Access this Article

Search this Article

Author(s)

Abstract

圏論的結合子(categorical vombinator)はラムダ計算の変数を含まない翻訳であることから、圏論的解釈を利用した関数型言語の実装に用いられている。本稿では圏の構造を随伴関手(adjointfunctor)で定義することで、圏論的結合子とその等式が圏論の基本概念から天下り的に導かれることを示す。圏論的結合子は随伴関手に付随する自然変換である単因子(unit)と余単因子(counit)として得られ、その等式は圏、関手、自然変換の定義、および随伴関手の三角可換図(triangular identity)から直接導かれる。まず最初にカルテシアン閉圏(cartesian closed category)のための圏論的結合子の導出について述べ、これを用いた自由圏の構成を示す。そして次に圏論的結合子の非外延的(non-extensional)な等武が半随伴関手(semi-adojoint functor)から導かれることを示す。最後に一般の極限対象(1imit object)や再帰的対象(recursive object)について考察し、その際に右随伴関手と左随伴関手の双対性(dua1ity)がどのように作用するかをみる。

Categorical combinators can be seen as variable-free translations of lambda-calculus and have been used in the implementation of functional languages based on their categorical interpretations. In this paper, we show that, if we define categorical structures by adjoint functors, we can derive categorical combinators and their equations uniformly from the basic concepts of category theory. Categorical combinators appear as the units and counits of adjoint functors, and their equations directly come from the definitions of categories, functors and natural transformations, and from the triangular identities of adjoint functors. We first show the derivation for cartesian closed categories and illustrate the construction of free categories in terms of categorical combinators. We next discuss the derivation of non-extensional categorical combinators from semi-adjoint functors. Finally we consider general limit objects and recursive objects with view to the duality between left and right adjoint functors.

Journal

  • IPSJ Journal

    IPSJ Journal 36(10), 2422-2432, 1995-10-15

    Information Processing Society of Japan (IPSJ)

References:  32

Codes

  • NII Article ID (NAID)
    110002721963
  • NII NACSIS-CAT ID (NCID)
    AN00116647
  • Text Lang
    JPN
  • Article Type
    Journal Article
  • ISSN
    1882-7764
  • Data Source
    CJP  NII-ELS  IPSJ 
Page Top