圏論に基づく正則項上の単一化の形式化

• Item type: Trans(1)
• 公開日: 2021-05-12
• タイトル: 圏論に基づく正則項上の単一化の形式化
• タイトル / 言語: en
• タイトル: A Category-theoretic Formalization of Unification over Rational Terms
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [通常論文] 正則項，終余代数，単一化，モナド，クライスリ圏
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 新潟大学大学院自然科学研究科
• 著者所属: 新潟大学大学院自然科学研究科
• 著者所属(英): en
• 著者所属(英): Graduate School of Science and Technology, Niigata University
• 著者所属(英): en
• 著者所属(英): Graduate School of Science and Technology, Niigata University
• 著者名: 宮前, 海里; 青戸, 等人
• 著者名(英): Kairi, Miyamae; Takahito, Aoto
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 自動推論において単一化は重要な役割を果たす．さまざま形式体系では，通常，有限項を対象とすることが多いが，遅延リストやストリームなどの仮想的に無限長と見なされるデータを扱うために対象を無限項に拡張した体系が提案されている．無限項の中でも部分項が有限個のみの項を正則項とよぶ(Courcelle，1983)．正則項は有限項の等式集合である再帰式表現を用いて記述することができる．正則項の単一化について岩見と青戸(2012)によって以下が示されている．(1)再帰式表現の解が再帰式表現の最汎単一化子である．(2)正則項の単一化子が再帰式表現から構成できる等式の単一化子と対応する．本論文ではこれらの結果を圏論を用いて一般化する．正則項の圏論を用いた定式化について，Aczelら(2003)は，反復可能な関手によって特徴付けられる終余代数を考え，正則項を表す射が再帰式表現から一意的に定まることを示している．また，RydeheardとBurstall (1986)により，余等化子を用いた最汎単一化子の圏論上での定式化が与えられている．上記の(1)，(2)の結果を一般化するために，最汎単一化子をクライスリ圏上の余等化子として与えて，再帰式表現の解が余等化子になることを示す．圏論上で一般化することにより，集合の圏と多項式的な関手を用いれば元の結果が得られるばかりでなく，たとえば，完備半順序の圏や有限部分集合を返す関手についても本結果を適用することができる．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Unification plays an important role in automated reasoning. Various formal systems usually deal with finite terms; on the other hand, in order to deal with lazy lists or streams, which can be virtually regarded as infinite data, infinite terms are considered in some systems. A rational term is an infinite term which has only finite many subterms (Courcelle, 1983). A rational term can be given finitely by using regular systems. On the unification over rational terms, the following facts are given by Iwami and Aoto (2012). (1) The solution of a regular system is the most general unifier of that regular system. (2) A unifier of rational terms corresponds a unifier of equations constructed by the regular systems specifying those terms. In this paper, we generalize these results using category theory. In their category-theoretic formalization of rational terms, Aczel et al. (2003) considered final coalgebras characterized by iteratable functors, and showed that arrows which represent rational terms are uniquely determined by guarded equations. In addition, the category-theoretic formalization of most general unifier using coequalizer was given by Rydeheard and Burstall (1986). To generalize the results (1) and (2) above, we formalize a most general unifier as a coequalizer in a Kleisli category and show that the solution of guarded equation becomes a coequalizer. Thanks to the formalization based on category theory, not only the original results on rational terms are obtained by considering the category of sets and a polynomial functor, but we can also apply our results, for example, to the category of completely partially ordered sets or the functor that returns finite subsets for each given set.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 14, 号 2, p. 1-14, 発行日 2021-05-12
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会