Layer Systems for Proving Confluence

被引：3

作者：

Felgenhauer, Bertram ^{[1
]}

Zankl, Harald ^{[1
]}

Middeldorp, Aart ^{[1
]}

机构：

[1] Univ Innsbruck, Inst Comp Sci, A-6020 Innsbruck, Austria

来源：

IARCS ANNUAL CONFERENCE ON FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE (FSTTCS 2011) | 2011年 / 13卷

基金：

奥地利科学基金会;

关键词：

Term rewriting; Confluence; Modularity; Persistence; TERM-REWRITING-SYSTEMS; MODULARITY; PROOF;

D O I：

10.4230/LIPIcs.FSTTCS.2011.288

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We introduce layer systems for proving generalizations of the modularity of confluence for first-order rewrite systems. Layer systems specify how terms can be divided into layers. We establish structural conditions on those systems that imply confluence. Our abstract framework covers known results like many-sorted persistence, layer-preservation and currying. We present a counterexample to an extension of the former to order-sorted rewriting and derive new sufficient conditions for the extension to hold.

引用

页码：288 / 299

页数：12

共 16 条

[1]

Aoto T., 1996, ISRR960025F JAIST SC

[2]

Aoto T., 1997, Journal of Universal Computer Science, V3, P1134, DOI [10.3217/jucs-003-11-1134, DOI 10.3217/JUCS-003-11-1134]

[3]

Baader F., 1998, Term rewriting and all that

[4] The confluence of ground term rewrite systems is decidable in polynomial time [J].

Comon, H ;

Godoy, G ;

Nieuwenhuis, R .

42ND ANNUAL SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE, PROCEEDINGS, 2001, :298-307

[5]

Felgenhauer B., 2011, TECHNICAL REPORT

[6]

Jouannaud J.P., 2008, INT J SOFTW INFORM, V2, P61

[7] Confluence of curried term-rewriting systems [J].

Kahrs, S .

JOURNAL OF SYMBOLIC COMPUTATION, 1995, 19 (06) :601-623

[8] Comparing curried and uncurried rewriting [J].

Kennaway, R ;

Klop, JW ;

Sleep, R ;

DeVries, FJ .

JOURNAL OF SYMBOLIC COMPUTATION, 1996, 21 (01) :15-39

[9] MODULARITY OF CONFLUENCE - A SIMPLIFIED PROOF [J].

KLOP, JW ;

MIDDELDORP, A ;

TOYAMA, Y ;

DEVRIJER, R .

INFORMATION PROCESSING LETTERS, 1994, 49 (02) :101-109

[10]

Luth C, 1996, LECT NOTES COMPUT SC, V1103, P261

← 1 2 →