単純型付き項書換え系における停止性の自動証明

• Item type: Trans(1)
• 公開日: 2003-03-15
• タイトル: 単純型付き項書換え系における停止性の自動証明
• タイトル / 言語: en
• タイトル: Proving Termination of Simply Typed Term Rewriting Systems Automatically
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 通常論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 群馬大学工学部情報工学科
• 著者所属: 三重大学工学部情報工学科
• 著者所属(英): en
• 著者所属(英): Department of Computer Science, Faculty of Engineering, Gunma University
• 著者所属(英): en
• 著者所属(英): Department of Information Engineering, Faculty of Engineering, Mie University
• 著者名: 青戸, 等人; 山田, 俊行
• 著者名(英): Takahito, Aoto; Toshiyuki, Yamada
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 単純型付き項書換え系は，山田（RTA’01，2001）によって提案された，高階関数を利用できる項書換え系である．通常の高階項書換え系と異なり，この項書換え系は束縛変数を組み込んでいない．本論文では，単純型付き項書換え系の停止性証明法を提案する．まず，項書換え系の変換法を導入し，単純型付き項書換え系の停止性が，変換により得られる第1 階項書換え系の停止性から導かれることを示す．次に，変換で得られた第1 階項書換え系の停止性証明を容易にするラベリングを提案する．山田（RTA’01，2001）が与えた意味論的な停止性証明法とは対照的に，本論文で提案する停止性証明法は構文論的なため，停止性証明の自動化が容易である．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Simply typed term rewriting proposed by Yamada (RTA’01, 2001) is a framework of term rewriting allowing higher-order functions. In contrast to the usual higher-order term rewriting frameworks, simply typed term rewriting dispenses with bound variables. In this paper, we present a method to prove termination of simply typed term rewriting systems. We first give a transformation on term rewriting systems and show that termination of simply typed term rewriting systems is induced from that of the first-order term rewriting systems obtained by this transformation. We next introduce a labelling technique which facilitates termination proof of the first-order term rewriting systems obtained by our transformation. Contrary to the semantic method proposed by Yamada (RTA’01, 2001), our technique is based on a syntactic approach; and thus one can easily automate termination proof of simply typed term rewriting systems.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 44, 号 SIG04(PRO17), p. 67-77, 発行日 2003-03-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会