NATURAL TERMINATION

被引：37

作者：

DERSHOWITZ, N

HOOT, C

机构：

[1] Department of Computer Science, University of Illinois at Urbana - Champaign, Urbana, IL 61801-2987

来源：

THEORETICAL COMPUTER SCIENCE | 1995年 / 142卷 / 02期

基金：

美国国家科学基金会;

关键词：

D O I：

10.1016/0304-3975(94)00275-4

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Two techniques are examined for showing termination of rewrite systems when simplification orderings are insufficient. The first approach generalizes the various path orderings and the conditions under which they work. Examples of its use are given and a brief description of an implementation is presented. The second approach uses restricted derivations, called ''forward closures'', for proving termination of orthogonal and overlaying systems. Both approaches allow the use of ''natural'' interpretations under which rules rewrite terms to terms of the same value.

引用

页码：179 / 207

页数：29

共 38 条

[1] EQUATIONAL INFERENCE, CANONICAL PROOFS, AND PROOF ORDERINGS [J].