TY - GEN

T1 - A λ-to-CL translation for strong normalization

AU - Akama, Yohji

N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1997.

PY - 1997

Y1 - 1997

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84892753229&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84892753229&partnerID=8YFLogxK

U2 - 10.1007/3-540-62688-3_25

DO - 10.1007/3-540-62688-3_25

M3 - Conference contribution

AN - SCOPUS:84892753229

SN - 3540626883

SN - 9783540626886

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 1

EP - 10

BT - Typed Lambda Calculi and Applications - 3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997, Proceedings

A2 - de Groote, Philippe

A2 - Hindley, J. Roger

PB - Springer Verlag

T2 - 3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997

Y2 - 2 April 1997 through 4 April 1997

ER -