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

• 宮前, 海里

• 青戸, 等人

書誌事項

タイトル別名

• A Category-theoretic Formalization of Unification over Rational Terms

抄録

自動推論において単一化は重要な役割を果たす．さまざま形式体系では，通常，有限項を対象とすることが多いが，遅延リストやストリームなどの仮想的に無限長と見なされるデータを扱うために対象を無限項に拡張した体系が提案されている．無限項の中でも部分項が有限個のみの項を正則項とよぶ(Courcelle，1983)．正則項は有限項の等式集合である再帰式表現を用いて記述することができる．正則項の単一化について岩見と青戸(2012)によって以下が示されている．(1)再帰式表現の解が再帰式表現の最汎単一化子である．(2)正則項の単一化子が再帰式表現から構成できる等式の単一化子と対応する．本論文ではこれらの結果を圏論を用いて一般化する．正則項の圏論を用いた定式化について，Aczelら(2003)は，反復可能な関手によって特徴付けられる終余代数を考え，正則項を表す射が再帰式表現から一意的に定まることを示している．また，RydeheardとBurstall (1986)により，余等化子を用いた最汎単一化子の圏論上での定式化が与えられている．上記の(1)，(2)の結果を一般化するために，最汎単一化子をクライスリ圏上の余等化子として与えて，再帰式表現の解が余等化子になることを示す．圏論上で一般化することにより，集合の圏と多項式的な関手を用いれば元の結果が得られるばかりでなく，たとえば，完備半順序の圏や有限部分集合を返す関手についても本結果を適用することができる．

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.

収録刊行物

• 情報処理学会論文誌プログラミング（PRO）

  情報処理学会論文誌プログラミング（PRO） 14 (2), 1-14, 2021-05-12

キーワード

• [通常論文] 正則項，終余代数，単一化，モナド，クライスリ圏

詳細情報

• CRID: 1050288060479054720
• NII論文ID: 170000184922
• NII書誌ID: AA11464814
• ISSN: 18827802
• Web Site: http://id.nii.ac.jp/1001/00210955/
• 本文言語コード: ja
• 資料種別: article
• データソース種別:
  • IRDB
  • CiNii Articles
  • KAKEN