Equational rules for rewriting logic

被引：71

作者：

Viry, P ^{[1
]}

机构：

[1] ASTEM RI, Kyoto 6008813, Japan

来源：

THEORETICAL COMPUTER SCIENCE | 2002年 / 285卷 / 02期

关键词：

rewriting; equational programming; coherence; building-in equality;

D O I：

10.1016/S0304-3975(01)00366-8

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

In addition to equations and rules, we introduce equational rules that are oriented while having an equational interpretation. Correspondence between operational behavior and intended semantics is guaranteed by a property of coherence, which can be checked by examination of critical pairs and linearity conditions. We present applications of this theory to three examples where the rewrite relation is interpreted, respectively, as equality, transition and deduction. 2002 Elsevier Science B.V. All rights reserved.

引用

页码：487 / 517

页数：31

共 43 条

[1] AC-UNIFICATION RACE - THE SYSTEM SOLVING APPROACH, IMPLEMENTATION AND BENCHMARKS [J].

ADI, M ;

KIRCHNER, C .

JOURNAL OF SYMBOLIC COMPUTATION, 1992, 14 (01) :51-70

[2]

[Anonymous], 2000, SOFTWARE ENG OBJ, DOI DOI 10.1007/978-1-4757-6541-0_1

[3]

Baader F., 1999, Term Rewriting and All that, P223

[4]

BENAISSA Z, 1995, 2477 INRIA

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

BERGSTRA, JA ;

KLOP, JW .

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

[6]

BOLOGNESI T, 1989, FORMAL DESCRIPTION T, P23

[7]

BOUSDIRA W, 1988, LECTURE NOTES COMPUT, V294, P193

[8]

BOUTIN S, 1997, LECT NOTES COMPUTER, V1281

[9]

COMON H, 1991, P 5 INT WORKSH UN BA

[10]

CURIEN PL, 1992, 1617 RR INRIA

← 1 2 3 4 5 →