静的依存対法による高階書換え系の停止性証明 Static Dependency Pair Method for Proving Termination of Higher-Order Rewriting Systems

Search this Article

Author(s)

Abstract

高階書換え系は関数型言語の計算モデルであり,依存対法は再帰構造解析に基づいた高階書換え系の停止性証明法である.近年提案された強計算性に基づく静的依存対法は非常に強力であり,停止性証明可能なクラスが劇的に広がった.本研究会において我々は強計算性に基づく静的依存対法を紹介した.しかしこの成果においては匿名関数の取り扱いに若干の制限が課されていた.本稿では,証明で利用するある種の部分項を表現する関数Candを改良することにより,匿名関数に関する制限を全て除去できることを示す.

A higher-order rewriting systems (HRS) is a computational model that provides operational semantics for functional programs. A dependency pair method is a proving one for the termination of rewriting systems. Recently, we proposed a extremely powerful method to prove termination of simply-typed term rewriting systems (STRSs), namely static dependency pair method, which is based on the notion of strong computability. In this technical committee, we extended the method to HRSs. In this report, we remove any restrictions for anonymous functions, which were requied in this result. We show that a slight improvement in the notion of candidate terms is connected with this significant benefit.

Journal

  • IEICE technical report

    IEICE technical report 107(99), 17-22, 2007-06-14

    The Institute of Electronics, Information and Communication Engineers

References:  11

Codes

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