Infinitary Combinatory Reduction Systems: Confluence

TL;DR

This paper investigates confluence properties of higher-order infinitary rewriting systems, specifically for infinitary Combinatory Reduction Systems, establishing conditions under which confluence and normal form properties hold.

Contribution

It proves confluence modulo hypercollapsing subterms for fully-extended, orthogonal iCRSs and highlights differences from first-order infinitary rewriting.

Findings

Fully-extended, orthogonal iCRSs are confluent modulo hypercollapsing subterms.

Such systems have the normal form and unique normal form properties.

Almost non-collapsing iCRSs are not necessarily confluent.

Abstract

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.