| |
VOLUME 5, ISSUE 4, PAPER 3
|
Infinitary Combinatory Reduction Systems: Confluence
|
©Jeroen Ketema, Tohoku University
©Jakob Grue Simonsen, University of Copenhagen
|
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.
|
Publication date: December 20, 2009
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-5(4:3)2009
Hit Counts: 890 |
 Creative Commons | |
