A λ-to-CL translation for strong normalization
Yohji Akama · Lecture notes in computer science · 1997
We introduce a simple translation from λ-calculus to combinatory logic (cl) such that: A is an SN λ-term iff the translation result of A is an SN term of cl (the reductions are β-reduction in λ-calculus and weak reduction in cl). None of the conventional translations from λ-calculus to CL satisfy the above property. Our translation provides a simpler SN proof of Gödel's λ-calculus by the ordinal number assignment method. By using our translation, we construct a homomorphism from a conditionally partial combinatory algebra which arises over SN λ-terms to a partial combinatory algebra which arises over SN CL-terms. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.