消去法による項書換え系の停止性判定について  [in Japanese] On Proving Termination by General Dummy Elimination  [in Japanese]

Search this Article

Author(s)

Abstract

従来の停止性判定法を適用できない項書換えシステム(TRS)の停止性を示すために, Ferreiraは一般消去法を提案した.一般消去法は, 規則に現れる適当な関数記号を消去することでより単純な構造のTRSに変換する.変換後のTRSが停止性を持つならば元のTRSも停止性を持つという性質があるため, 一般消去法は停止性判定に有効である.一方, ArtsとGieslは, TRSの規則に現れる関数定義記号の出現に注目し, 無限書換え列の本質を簡潔に記述できる依存対の概念を導入した.本稿では, 一般消去法が変換後に付け加える規則に注目し, 不必要な規則を除くことで一般消去法を改良する.改良一般消去法においても, 変換後のTRSが元のTRSの停止性を保証していることを依存対の概念を用いることで示す.

The general dummy elimination defined by Ferreira is a transformation on TRSs that eliminates a function symbol in rules of TRSs to prove termimation easier thsn the original one. Recently, Arts and Giesl introduced the notion of dependency pairs, which gives an effective method for analyzing an infinite reduction sequence. The purpose of this paper is to extend the general dummy elimination and to prove that the extended transformation is sound with respect to termination by the notion of dependency pairs.

Journal

  • IEICE technical report. Theoretical foundations of Computing

    IEICE technical report. Theoretical foundations of Computing 98(432), 57-64, 1999-11-16

    The Institute of Electronics, Information and Communication Engineers

References:  6

Codes

  • NII Article ID (NAID)
    110003191684
  • NII NACSIS-CAT ID (NCID)
    AN10013152
  • Text Lang
    JPN
  • Article Type
    ART
  • Data Source
    CJP  NII-ELS 
Page Top