Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Journal Articles IEICE Transactions on Information and Systems Year : 2009

Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems

Keiichirou Kusakari
  • Function : Author
  • PersonId : 861355
Yasuo Isogai
  • Function : Author
  • PersonId : 861356
Masahiko Sakai
  • Function : Author
  • PersonId : 861357
Frédéric Blanqui

Abstract

Higher-order rewrite systems (HRSs) and simply-typed term rewriting systems (STRSs) are computational models of functional programs. We recently proposed an extremely powerful method, the static dependency pair method, which is based on the notion of strong computability, in order to prove termination in STRSs. In this paper, we extend the method to HRSs. Since HRSs include λ-abstraction but STRSs do not, we restructure the static dependency pair method to allow λ-abstraction, and show that the static dependency pair method also works well on HRSs without new restrictions.
Fichier principal
Vignette du fichier
main.pdf (205.94 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00397820 , version 1 (26-09-2011)

Identifiers

  • HAL Id : inria-00397820 , version 1
  • ARXIV : 1109.5468

Cite

Keiichirou Kusakari, Yasuo Isogai, Masahiko Sakai, Frédéric Blanqui. Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems. IEICE Transactions on Information and Systems, 2009. ⟨inria-00397820⟩
189 View
108 Download

Altmetric

Share

Gmail Facebook X LinkedIn More