A λ-to-CL translation for strong normalization

Yohji Akama

doi:10.1007/3-540-62688-3_25

A λ-to-CL translation for strong normalization

Yohji Akama

SCI - Mathematics

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

7 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 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	https://doi.org/10.1007/3-540-62688-3_25
Publication status	Published - 1997
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

Conference

Conference	3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997
Country/Territory	France
City	Nancy
Period	97/4/2 → 97/4/4

Access to Document

10.1007/3-540-62688-3_25

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

Akama, Yohji. / A λ-to-CL translation for strong normalization. Typed Lambda Calculi and Applications - 3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997, Proceedings. editor / Philippe de Groote ; J. Roger Hindley. Springer Verlag, 1997. pp. 1-10 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{62f04a3d158042c69294b264131e46ae,

title = "A λ-to-CL translation for strong normalization",

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{\"o}del{\textquoteright}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.",

author = "Yohji Akama",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1997.; 3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997 ; Conference date: 02-04-1997 Through 04-04-1997",

year = "1997",

doi = "10.1007/3-540-62688-3_25",

language = "English",

isbn = "3540626883",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "1--10",

editor = "{de Groote}, Philippe and Hindley, {J. Roger}",

booktitle = "Typed Lambda Calculi and Applications - 3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997, Proceedings",

address = "Germany",

}

Akama, Y 1997, A λ-to-CL translation for strong normalization. in P de Groote & JR Hindley (eds), Typed Lambda Calculi and Applications - 3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1210, Springer Verlag, pp. 1-10, 3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997, Nancy, France, 97/4/2. https://doi.org/10.1007/3-540-62688-3_25

A λ-to-CL translation for strong normalization. / Akama, Yohji.
Typed Lambda Calculi and Applications - 3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997, Proceedings. ed. / Philippe de Groote; J. Roger Hindley. Springer Verlag, 1997. p. 1-10 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1210).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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 -

Akama Y. A λ-to-CL translation for strong normalization. In de Groote P, Hindley JR, editors, Typed Lambda Calculi and Applications - 3rd International Conference on Typed Lambda Calculi and Applications, TLCA 1997, Proceedings. Springer Verlag. 1997. p. 1-10. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-62688-3_25

A λ-to-CL translation for strong normalization

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this