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

lmcs:840 - Logical Methods in Computer Science, December 20, 2009, Volume 5, Issue 4 - https://doi.org/10.2168/LMCS-5(4:3)2009
Infinitary Combinatory Reduction Systems: ConfluenceArticle

Authors: Jeroen Ketema ; Jakob Grue Simonsen

    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.


    Volume: Volume 5, Issue 4
    Published on: December 20, 2009
    Imported on: October 28, 2008
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,D.3.1,F.3.2,F.4.1,F.4.2
    Funding:
      Source : OpenAIRE Graph
    • Infinite Objects, computation, modeling and reasoning; Funder: Netherlands Organisation for Scientific Research (NWO); Code: 642.000.502

    5 Documents citing this article

    Consultation statistics

    This page has been seen 1335 times.
    This article's PDF has been downloaded 233 times.