Endrullis, Joerg and Grabmayer, Clemens and Hendriks, Dimitri and Klop, Jan Willem and van Oostrom, Vincent - Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples

lmcs:752 - Logical Methods in Computer Science, June 8, 2014, Volume 10, Issue 2
Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples

Authors: Endrullis, Joerg and Grabmayer, Clemens and Hendriks, Dimitri and Klop, Jan Willem and van Oostrom, Vincent

We present some contributions to the theory of infinitary rewriting for weakly orthogonal term rewrite systems, in which critical pairs may occur provided they are trivial. We show that the infinitary unique normal form property fails by an example of a weakly orthogonal TRS with two collapsing rules. By translating this example, we show that this property also fails for the infinitary lambda-beta-eta-calculus. As positive results we obtain the following: Infinitary confluence, and hence the infinitary unique normal forms property, holds for weakly orthogonal TRSs that do not contain collapsing rules. To this end we refine the compression lemma. Furthermore, we establish the triangle and diamond properties for infinitary multi-steps (complete developments) in weakly orthogonal TRSs, by refining an earlier cluster-analysis for the finite case.


Source : oai:arXiv.org:1403.6172
DOI : 10.2168/LMCS-10(2:7)2014
Volume: Volume 10, Issue 2
Published on: June 8, 2014
Submitted on: November 2, 2010
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 82 times.
This article's PDF has been downloaded 76 times.