Abstract abstract reduction

被引：11

作者：

Struth, G ^{[1
]}

机构：

[1] Univ Bundeswehr Munchen, Fak Informat, D-85577 Neubiberg, Germany

来源：

JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING | 2006年 / 66卷 / 02期

关键词：

semirings; Kleene algebra; omega-algebra; rewriting; abstract reduction; lambda-calculus; Church-Rosser theorems; termination analysis; formal mathematics;

D O I：

10.1016/j.jlap.2005.04.001

中图分类号：

学科分类号：

摘要：

We propose novel algebraic proof techniques for rewrite systems. Church-Rosser theorems and further fundamental statements that do not mention termination are proved in Kleene algebra. Certain reduction and transformation theorems for termination that depend on abstract commutation, cooperation or simulation properties are proved in an extension with infinite iteration. Benefits of the algebraic approach are simple concise calculational proofs by equational reasoning, connection with automata-based decision procedures and a natural formal semantics for rewriting diagrams. It is therefore especially suited for mechanization and automation. (c) 2005 Elsevier Inc. All rights reserved.

引用

页码：239 / 270

页数：32

共 50 条

[21] Stable Relations and Abstract Interpretation of Higher-Order Programs
Montagu, Benoit
Jensen, Thomas
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (ICFP):
[22] Regaining cut admissibility in deduction modulo using abstract completion
Burel, Guillaume
Kirchner, Claude
INFORMATION AND COMPUTATION, 2010, 208 (02) : 140 - 164
[23] DERIVING LINEAR SIZE RELATIONS FOR LOGIC PROGRAMS BY ABSTRACT INTERPRETATION
DESCHREYE, D
VERSCHAETSE, K
NEW GENERATION COMPUTING, 1995, 13 (02) : 117 - 154
[24] Improving flow analyses via ΓCFA -: Abstract garbage collection and counting
Might, Matthew
Shivers, Olin
ACM SIGPLAN NOTICES, 2006, 41 (09) : 13 - 25
[25] Probabilistic Abstract Interpretation: From Trace Semantics to DTMC's and Linear Regression
Di Pierro, Alessandra
Wiklicky, Herbert
SEMANTICS, LOGICS, AND CALCULI: ESSAYS DEDICATED TO HANNE RIIS NIELSON AND FLEMMING NIELSON ON THE OCCASION OF THEIR 60TH BIRTHDAYS, 2016, 9560 : 111 - 139
[26] A functional correspondence between monadic evaluators and abstract machines for languages with computational effects
Ager, MS
Danvy, O
Midtgaard, J
THEORETICAL COMPUTER SCIENCE, 2005, 342 (01) : 149 - 172
[27] A faithful representation of non-associative lambek grammars in abstract categorial grammars
Retoré C.
Salvati S.
Journal of Logic, Language and Information, 2010, 19 (2) : 185 - 200
[28] On the Expressive Power of Abstract Categorial Grammars: Representing Context-Free Formalisms
Philippe de Groote
Sylvain Pogodalla
Journal of Logic, Language and Information, 2004, 13 (4) : 421 - 438
[29] About Parallel and Syntactocentric Formalisms: A Perspective from the Encoding of Convergent Grammar into Abstract Categorial Grammar
de Groote, Philippe
Pogodalla, Sylvain
Pollard, Carl
FUNDAMENTA INFORMATICAE, 2011, 106 (2-4) : 211 - 231
[30] Reachability-based acyclicity analysis by abstract interpretation (vol 474, pg 60, 2013)
Genaim, Samir
Zanardini, Damiano
THEORETICAL COMPUTER SCIENCE, 2013, 503 : 115 - 115

← 1 2 3 4 5 →