Strong normalization and confluence for reflexive combinatory logic. (English) Zbl 1328.03010

Beklemishev, Lev D. (ed.) et al., Logic, language, information and computation. 18th international workshop, WoLLIC 2011, Philadelphia, PA, USA, May 18–20, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-20919-2/pbk). Lecture Notes in Computer Science 6642. Lecture Notes in Artificial Intelligence, 228-238 (2011).
Summary: Reflexive combinatory logic RCL was introduced by S. N. Artëmov [Russ. Math. Surv. 59, No. 2, 203–229 (2004); translation from Usp. Mat. Nauk 59, No. 2, 9–36 (2004; Zbl 1074.03029)] as an extension of typed combinatory logic CL\(_{\rightarrow }\) capable to internalize its own derivations of typing judgments. It was designed as a basic theoretical prototype of functional programming languages extended by this kind of self-referential capacity. However, its operational aspects remained to be clarified.
We study reductions for reflexive combinatory logic and prove strong normalization and confluence properties.
For the entire collection see [Zbl 1214.03002].


03B40 Combinatory logic and lambda calculus
68N18 Functional programming and lambda calculus


Zbl 1074.03029
Full Text: DOI