Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Acta Informaticaarrow_drop_down
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao
Acta Informatica
Article . 1996 . Peer-reviewed
License: Springer TDM
Data sources: Crossref
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao
Acta Informatica
Article . 1996 . Peer-reviewed
License: Springer TDM
Data sources: Crossref
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao
zbMATH Open
Article
Data sources: zbMATH Open
DBLP
Article . 2020
Data sources: DBLP
MPG.PuRe
Article . 1996
Data sources: MPG.PuRe
versions View all 5 versions
addClaim

Relating confluence, innermost-confluence and outermost-confluence properties of term rewriting systems

Relating confluence, innermost-confluence and outermost-confluence properties of term rewriting system
Authors: Krishna Rao, M.;

Relating confluence, innermost-confluence and outermost-confluence properties of term rewriting systems

Abstract

In the last few decades, term rewriting systems have played a fundamental role in the analysis and implementation of abstract data type specifications, decidability of word problems, theorem proving, computability theory, design of functional programming languages (e.g. Miranda), integration of functional programming and logic programming paradigms, termination of logic programs, etc. Termination and confluence are two fundamental properties of term rewriting systems. In this paper, we study confluence properties. To be precise, we obtain a number of results relating different notions of confluence. A rewrite step \(C[l \sigma] \Rightarrow C[r \sigma]\) with rewrite rule \(l \to r\) is an innermost reduction step if no proper subterm of \(l \sigma\) is reducible. A term rewriting system is innermost-confluent if its innermost rewrite relation is confluent. The study of innermost confluence is interesting since denotational semantics is often defined by a kind of innermost evaluation procedure, which is similar to innermost rewriting. A reduction step \(C[l \sigma] \Rightarrow C[r \sigma]\) with rewrite rule \(l \to r\) is an outermost reduction step if no position above \(l \sigma\) is a redex position, i.e., there is no subterm \(s\) of \(C[l\sigma]\) and no rule \(l' \to r'\) such that (i) \(l \sigma\) is a proper subterm of \(s\) and (ii) \(s\) is an instance of \(l'\). A term rewriting system \({\mathcal R}({\mathcal F}, R)\) is outermost-confluent if its outermost rewrite relation is confluent. Outermost-confluence is interesting because outermost reduction corresponds to lazy evaluation. If a system is outermost-confluent, that means that the lazy semantics is well-defined, regardless of the order in which outermost reductions are done and regardless of which rules are applied. Also, nonterminating outermost-confluent systems are those for which a semantics based on infinite terms seems most natural, since lazy evaluation for nonterminating programs can lead to infinite structures. It is easy to observe that confluence of terminating systems implies innermost-confluence and outermost-confluence as every innermost/outermost derivation terminates. However, a terminating system can be innermost or outermost-confluent without being confluent. A nonterminating system can be confluent but not innermost (outermost) confluent and vice versa. The following results are established in the paper. 1. A weakly innermost normalizing overlay system is innermost-confluent if and only if it is confluent. 2. A weakly innermost normalizing system is innermost-confluent if it is confluent. But the converse is not true. 3. strongly innermost normalizing system is innermost-confluent if \(s\theta\) and \(t \theta\) are joinable by innermost rewriting for every overlay critical pair \(\langle s, t \rangle\) and a substitution \(\theta\) which replaces variables by irreducible terms. 4. Let \(R\) be a weakly outermost normalizing left-linear overlay system with the property: if the right-hand side \(r_1\) of a rule unifies with a non-variable proper subterm of the left-hand side \(l_2\) of a rule then \(l_2\) does not unify with the left-hand side of any other rule in \(R\). Then \(R\) is confluent if and only if it is outermost-confluent. 5. A weakly outermost normalizing system is outermost-confluent if it is confluent. But the converse is not true. 6. Every weakly normalizing almost orthogonal system is outermost-confluent. A strongly outermost normalizing left-linear overlay system is confluent if and only if it is outermost-confluent.

Keywords

confluence, Grammars and rewriting systems, Semantics in the theory of computing, lazy evaluation, term rewriting systems, denotational semantics

  • BIP!
    Impact byBIP!
    selected citations
    These citations are derived from selected sources.
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    1
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
Powered by OpenAIRE graph
Found an issue? Give us feedback
selected citations
These citations are derived from selected sources.
This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Citations provided by BIP!
popularity
This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
1
Average
Average
Average
Upload OA version
Are you the author of this publication? Upload your Open Access version to Zenodo!
It’s fast and easy, just two clicks!