A λ-to-CL translation for strong normalization

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Citations (Scopus)

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 languageEnglish
Title of host publicationTyped Lambda Calculi and Applications - 3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997, Proceedings
EditorsPhilippe de Groote, J. Roger Hindley
PublisherSpringer-Verlag
Pages1-10
Number of pages10
ISBN (Print)3540626883, 9783540626886
DOIs
Publication statusPublished - 1997 Jan 1
Externally publishedYes
Event3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997 - Nancy, France
Duration: 1997 Apr 21997 Apr 4

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1210
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997
CountryFrance
CityNancy
Period97/4/297/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