強計算依存対法による高階書換え系の停止性証明  [in Japanese] Proving Termination of Higher-Order Rewrite Systems based on Strongly Computable Dependency Pair Method  [in Japanese]

Search this Article

Author(s)

Abstract

項書換え系は関数プログラムの計算モデルであり,その停止性は重要な性質の1つである.停止性証明法の1つに依存対法と呼ばれる再起構造解析法があるが,これを高階書換え系に適用するこれまでの手法は能力が低い.本論文では単純型項書換え系のための強計算依存対法の高階書換え系への拡張を提案する.これにより,既存の手法では証明できなかった高階書換え系の停止性の証明が可能となった.

The higher-order rewrite systems (HRS for short) [14] are a computation model of functional programming languages, and hence the termination is one of the most important properties of them. While the dependency pair method is very useful for proving termination of term rewriting systems, previous methods to apply it for HRSs do not have enough power. In this paper, we extend the strongly computable dependency-pairs method for HRSs. There are some HRSs of which termination can be proved by our method but by no known methods.

Journal

  • IEICE technical report

    IEICE technical report 106(15), 31-36, 2006-04-13

    The Institute of Electronics, Information and Communication Engineers

References:  9

Cited by:  2

Codes

  • NII Article ID (NAID)
    110004718943
  • NII NACSIS-CAT ID (NCID)
    AN10013287
  • Text Lang
    JPN
  • Article Type
    Journal Article
  • ISSN
    09135685
  • NDL Article ID
    7903173
  • NDL Source Classification
    ZN33(科学技術--電気工学・電気機械工業--電子工学・電気通信)
  • NDL Call No.
    Z16-940
  • Data Source
    CJP  CJPref  NDL  NII-ELS 
Page Top