SEQUENTIALITY IN ORTHOGONAL TERM REWRITING-SYSTEMS

被引：31

作者：

KLOP, JW ^{[1
]}

MIDDELDORP, A ^{[1
]}

机构：

[1] FREE UNIV AMSTERDAM,DEPT MATH & COMP SCI,1081 HV AMSTERDAM,NETHERLANDS

来源：

JOURNAL OF SYMBOLIC COMPUTATION | 1991年 / 12卷 / 02期

关键词：

D O I：

10.1016/S0747-7171(08)80124-1

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

For orthogonal term rewriting systems Q. Huet and J.-J. Lévy have introduced the property of ‘strong sequentiality’. A strongly sequential orthogonal term rewriting system admits an efficiently computable normalizing one-step reduction strategy. As shown by Huet and Lévy, strong sequentiality is a decidable property. In this paper we present an alternative analysis of strongly sequential term rewriting systems, leading to two simplified proofs of the decidability of this property. We also compare some related notions of sequentiality that recently have been proposed. © 1991, Academic Press Limited. All rights reserved.

引用

页码：161 / 195

页数：35

共 18 条

[1] NEEDED REDUCTION AND SPINE STRATEGIES FOR THE LAMBDA-CALCULUS [J].

BARENDREGT, HP ;

KENNAWAY, JR ;

KLOP, JW ;

SLEEP, MR .

INFORMATION AND COMPUTATION, 1987, 75 (03) :191-231

[2] CONDITIONAL REWRITE RULES - CONFLUENCE AND TERMINATION [J].

BERGSTRA, JA ;

KLOP, JW .

JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1986, 32 (03) :323-362

[3] MINIMAL AND OPTIMAL COMPUTATIONS OF RECURSIVE PROGRAMS [J].

BERRY, G ;

LEVY, JJ .

JOURNAL OF THE ACM, 1979, 26 (01) :148-175

[4]

BOUDOL G, 1985, ALGEBRAIC METHODS SE, P169

[5]

Dershowitz Nachum., 1990, HDB THEORETICAL COMP, P243

[6]

HOFFMANN CM, 1984, 11TH P ACM S PRINC P

[7] CONFLUENT REDUCTIONS - ABSTRACT PROPERTIES AND APPLICATIONS TO TERM REWRITING SYSTEMS [J].

HUET, G .

JOURNAL OF THE ACM, 1980, 27 (04) :797-821

[8]

HUET G, 1986, WORKING MATERIAL INT

[9]

HUET G, 1980, FORMAL LANGUAGE THEO, P349

[10]

HUET G, 1991, COMPUTATIONAL LOGIC

← 1 2 →