2024-03-29T16:44:02Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:001827012024-03-29T05:26:34Z01164:01384:09129:09211
制約付き項書換え系の依存鎖を上限付き整数増加列に変換する多項式解釈Polynomial Interpretations to Convert Dependency Chains of Constrained Term Rewriting Systems to Bounded Increasing Sequences of Intergersjpnhttp://id.nii.ac.jp/1001/00182613/Technical Reporthttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=182701&item_no=1&attribute_id=1&file_no=1Copyright (c) 2017 by the Institute of Electronics, Information and Communication Engineers This SIG report is only available to those in membership of the SIG.名古屋大学大学院情報科学研究科名古屋大学大学院情報学研究科名古屋大学大学院情報学研究科名古屋大学大学院情報科学研究科笹野, 智裕西田, 直樹酒井, 正彦上山, 智也制約付き項書換え系の停止性証明の枠組みである依存対フレームワークでは,関数呼び出しの関係を表現した依存鎖を下限付き整数減少列に変換する多項式解釈が証明の成否を左右する重要な役割を果たす.本稿では,依存鎖を下限付き整数減少列に変換する一方で,書換え規則による書換え系列を整数増加列に変換する多項式解釈による停止性証明機能を依存対フレームワークに導入する.さらに,依存鎖を上限付き整数増加列に変換する多項式解釈による停止性証明機能を導入し,比較実験の結果を報告する.In dependency pair framework for proving termination of constrained term rewriting systems, polynomial interpretations that transform dependency chains representing sequences of relevant function calls into bounded decreasing sequences of integers play an important role for the success of proving termination. In this article, we propose polynomial interpretations that transform dependency chains into bounded decreasing sequences but transform rewrite sequences of the original system into increasing sequences. We also propose polynomial interpretations that transform dependency chains into bounded increasing sequences of integers. We report empirical comparison results between the proposed polynomial interpretations.AN10112981研究報告ソフトウェア工学(SE)2017-SE-19623162017-07-122188-88252017-07-07