Strong Normalization and Confluence for Reflexive Combinatory Logic

摘要

Reflexive combinatory logic RCL was introduced by S. Arte mov as an extension of typed combinatory logic Cl__, capable to inter nalize 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 re mained to be clarified. We study reductions for reflexive combinatory logic and prove strong normalization and confluence properties.