関数プログラムの停止性証明のための辞書式経路順序  [in Japanese] Lexicographic Path Ordering for Proving Termination of Functional Programs  [in Japanese]

Search this Article

Author(s)

Abstract

項書き換え系は関数プログラムの計算モデルであり,停止性はその重要な性質の一つである.停止性証明法の一つに簡約化順序によって順序付ける方法がある.代表的な簡約化順序としては辞書式経路順序が知られており,その整礎性は単純化順序の概念を用いて保証される.本稿では,高階関数を扱うことができるように拡張した辞書式経路順序を3種類提案する.そして,様々な項の集合上でそれらが持つ性質を明らかにする.

Term rewriting system is a computational model of functional programs, and termination is one of the important properties. Reduction order is an important tool for proving termination. As typical reduction orders, we know lexicographic path orderings whose well-foundedness are ensured by the notion of simplification order. In this paper, we propose three extended lexicographic path orderings in order to deal with higher-order functions. Additionally, we analyze their properties under several constraints.

Journal

  • IEICE technical report

    IEICE technical report 105(597), 13-18, 2006-02-03

    The Institute of Electronics, Information and Communication Engineers

References:  4

Codes

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