A Lambda-to-CL Translation for Strong Normalization
Yohji Akama · 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 fi-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 Godel'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. 1 Introduction We often find some translations from -calculus to combinatory logic (cl) provide a pleasing viewpoint in the study of -calculus. The most typical example can be found in the study of the equational theories and the model theories of -calculus. The translations from -calculus to cl have been investigated comprehensively by Curry school [8], and we come to know ...