Termination and normalisation under strategies--Proofs in ELAN - Archive ouverte HAL Access content directly
Conference Papers Year : 2000

Termination and normalisation under strategies--Proofs in ELAN

(1) , (1)
1

Abstract

In this paper, we review several methods for proving termination of rewrite programs or answer questions about normal forms. We concentrate on the methods that have been designed in ELAN and which are useful for studying termination and normal forms of ELAN programs. We address several problems: general termination of a rewrite program, innermost termination on sets of ground terms, computation or approximation of the set of normal forms, modular termination of the union of rewrite systems, estimation of the number of normal forms for a non-deterministic rewrite program with strategies. For each point we briefly present one method, explain its scope and give references to other methods concerning the same problem, before describing the implementation in ELAN. We conclude with some open questions.
Fichier principal
Vignette du fichier
A00-R-307.pdf (471.72 Ko) Télécharger le fichier

Dates and versions

inria-00099059 , version 1 (26-09-2006)

Identifiers

  • HAL Id : inria-00099059 , version 1

Cite

Hélène Kirchner, Isabelle Gnaedig. Termination and normalisation under strategies--Proofs in ELAN. 3rd International Workshop on Rewriting Logic & Applications - WRLA'2000, 2000, Kanazawa, Japan, pp.93--115. ⟨inria-00099059⟩
77 View
56 Download

Share

Gmail Facebook Twitter LinkedIn More