Ketema, Jeroen and Simonsen, Jakob Grue - Infinitary Combinatory Reduction Systems: Confluence

lmcs:840 - Logical Methods in Computer Science, December 20, 2009, Volume 5, Issue 4
Infinitary Combinatory Reduction Systems: Confluence

Authors: Ketema, Jeroen and Simonsen, Jakob Grue

We study confluence in the setting of higher-order infinitary rewriting, in particular for infinitary Combinatory Reduction Systems (iCRSs). We prove that fully-extended, orthogonal iCRSs are confluent modulo identification of hypercollapsing subterms. As a corollary, we obtain that fully-extended, orthogonal iCRSs have the normal form property and the unique normal form property (with respect to reduction). We also show that, unlike the case in first-order infinitary rewriting, almost non-collapsing iCRSs are not necessarily confluent.


Source : oai:arXiv.org:0910.4081
DOI : 10.2168/LMCS-5(4:3)2009
Volume: Volume 5, Issue 4
Published on: December 20, 2009
Submitted on: June 25, 2015
Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,D.3.1,F.3.2,F.4.1,F.4.2


Share

Browsing statistics

This page has been seen 10 times.
This article's PDF has been downloaded 2 times.