### Abstract

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.

Original language | English |
---|---|

Title of host publication | Typed Lambda Calculi and Applications - 3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997, Proceedings |

Editors | Philippe de Groote, J. Roger Hindley |

Publisher | Springer-Verlag |

Pages | 1-10 |

Number of pages | 10 |

ISBN (Print) | 3540626883, 9783540626886 |

DOIs | |

Publication status | Published - 1997 Jan 1 |

Externally published | Yes |

Event | 3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997 - Nancy, France Duration: 1997 Apr 2 → 1997 Apr 4 |

### Publication series

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

Volume | 1210 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

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

Country | France |

City | Nancy |

Period | 97/4/2 → 97/4/4 |

### ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

## Fingerprint Dive into the research topics of 'A λ-to-CL translation for strong normalization'. Together they form a unique fingerprint.

## Cite this

Akama, Y. (1997). A λ-to-CL translation for strong normalization. In P. de Groote, & J. R. Hindley (Eds.),

*Typed Lambda Calculi and Applications - 3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997, Proceedings*(pp. 1-10). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1210). Springer-Verlag. https://doi.org/10.1007/3-540-62688-3_25