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 条
  • [31] On reduction and normalization in the computational core
    Faggian, Claudia
    Guerrieri, Giulio
    de' Liguoro, Ugo
    Treglia, Riccardo
    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2022, 32 (07) : 934 - 981
  • [32] A formal system of reduction paths for parallel reduction
    Fujita, Ken-etsu
    THEORETICAL COMPUTER SCIENCE, 2020, 813 : 327 - 340
  • [33] The search for a reduction in combinatory logic equivalent to λβ-reduction
    Seldin, Jonathan P.
    THEORETICAL COMPUTER SCIENCE, 2011, 412 (37) : 4905 - 4918
  • [34] INFINITARY COMBINATORY REDUCTION SYSTEMS: NORMALISING REDUCTION STRATEGIES
    Ketema, Jeroen
    Simonsen, Jakob Grue
    LOGICAL METHODS IN COMPUTER SCIENCE, 2010, 6 (01)
  • [35] Infinitary combinatory reduction systems: Normalising reduction strategies
    Ketema J.
    Simonsen J.G.
    Logical Methods in Computer Science, 2010, 6
  • [36] The search for a reduction in combinatory logic equivalent to λβ-reduction, Part II
    Seldin, Jonathan P.
    THEORETICAL COMPUTER SCIENCE, 2017, 663 : 34 - 58
  • [37] Reduction Monads and Their Signatures
    Ahrens, Benedikt
    Hirschowitz, Andre
    Lafont, Ambroise
    Maggesi, Marco
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (POPL):
  • [38] Full Reduction in the Face of Absurdity
    Scherer, Gabriel
    Remy, Didier
    PROGRAMMING LANGUAGES AND SYSTEMS, 2015, 9032 : 685 - 709
  • [39] Beta Reduction is Invariant, Indeed
    Accattoli, Beniamino
    Dal Lago, Ugo
    PROCEEDINGS OF THE JOINT MEETING OF THE TWENTY-THIRD EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC (CSL) AND THE TWENTY-NINTH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2014,
  • [40] Infinitary Combinatory Reduction Systems
    Ketema, Jeroen
    Simonsen, Jakob Grue
    INFORMATION AND COMPUTATION, 2011, 209 (06) : 893 - 926
12345