Applications of infinitary lambda calculus

H. Barendregt, J.W. Klop

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

We present an introduction to infinitary lambda calculus, highlighting its main properties. Subsequently we give three applications of infinitary lambda calculus. The first addresses the non-definability of Surjective Pairing, which was shown by the first author not to be definable in lambda calculus. We show how this result follows easily as an application of Berry's Sequentiality Theorem, which itself can be proved in the setting of infinitary lambda calculus. The second pertains to the notion of relative recursiveness of number-theoretic functions. The third application concerns an explanation of counterexamples to confluence of lambda calculus extended with non-left-linear reduction rules: Adding non-left-linear reduction rules such as δ xx → x or the reduction rules for Surjective Pairing to the lambda calculus yields non-confluence, as proved by the second author. We discuss how an extension to the infinitary lambda calculus, where Böhm trees can be directly manipulated as infinite terms, yields a more simple and intuitive explanation of the correctness of these Church-Rosser counterexamples. © 2009 Elsevier Inc. All rights reserved.
Original languageEnglish
Pages (from-to)559-582
JournalInformation and Computation
Volume207
Issue number5
DOIs
Publication statusPublished - 2009

Fingerprint

Lambda Calculus
Religious buildings
Pairing
Counterexample
Confluence
Intuitive
Correctness
Term
Theorem

Cite this

Barendregt, H. ; Klop, J.W. / Applications of infinitary lambda calculus. In: Information and Computation. 2009 ; Vol. 207, No. 5. pp. 559-582.
@article{781071adb2db48658a64467090ebd970,
title = "Applications of infinitary lambda calculus",
abstract = "We present an introduction to infinitary lambda calculus, highlighting its main properties. Subsequently we give three applications of infinitary lambda calculus. The first addresses the non-definability of Surjective Pairing, which was shown by the first author not to be definable in lambda calculus. We show how this result follows easily as an application of Berry's Sequentiality Theorem, which itself can be proved in the setting of infinitary lambda calculus. The second pertains to the notion of relative recursiveness of number-theoretic functions. The third application concerns an explanation of counterexamples to confluence of lambda calculus extended with non-left-linear reduction rules: Adding non-left-linear reduction rules such as δ xx → x or the reduction rules for Surjective Pairing to the lambda calculus yields non-confluence, as proved by the second author. We discuss how an extension to the infinitary lambda calculus, where B{\"o}hm trees can be directly manipulated as infinite terms, yields a more simple and intuitive explanation of the correctness of these Church-Rosser counterexamples. {\circledC} 2009 Elsevier Inc. All rights reserved.",
author = "H. Barendregt and J.W. Klop",
year = "2009",
doi = "10.1016/j.ic.2008.09.003",
language = "English",
volume = "207",
pages = "559--582",
journal = "Information and Computation",
issn = "0890-5401",
publisher = "Elsevier Inc.",
number = "5",

}

Applications of infinitary lambda calculus. / Barendregt, H.; Klop, J.W.

In: Information and Computation, Vol. 207, No. 5, 2009, p. 559-582.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - Applications of infinitary lambda calculus

AU - Barendregt, H.

AU - Klop, J.W.

PY - 2009

Y1 - 2009

N2 - We present an introduction to infinitary lambda calculus, highlighting its main properties. Subsequently we give three applications of infinitary lambda calculus. The first addresses the non-definability of Surjective Pairing, which was shown by the first author not to be definable in lambda calculus. We show how this result follows easily as an application of Berry's Sequentiality Theorem, which itself can be proved in the setting of infinitary lambda calculus. The second pertains to the notion of relative recursiveness of number-theoretic functions. The third application concerns an explanation of counterexamples to confluence of lambda calculus extended with non-left-linear reduction rules: Adding non-left-linear reduction rules such as δ xx → x or the reduction rules for Surjective Pairing to the lambda calculus yields non-confluence, as proved by the second author. We discuss how an extension to the infinitary lambda calculus, where Böhm trees can be directly manipulated as infinite terms, yields a more simple and intuitive explanation of the correctness of these Church-Rosser counterexamples. © 2009 Elsevier Inc. All rights reserved.

AB - We present an introduction to infinitary lambda calculus, highlighting its main properties. Subsequently we give three applications of infinitary lambda calculus. The first addresses the non-definability of Surjective Pairing, which was shown by the first author not to be definable in lambda calculus. We show how this result follows easily as an application of Berry's Sequentiality Theorem, which itself can be proved in the setting of infinitary lambda calculus. The second pertains to the notion of relative recursiveness of number-theoretic functions. The third application concerns an explanation of counterexamples to confluence of lambda calculus extended with non-left-linear reduction rules: Adding non-left-linear reduction rules such as δ xx → x or the reduction rules for Surjective Pairing to the lambda calculus yields non-confluence, as proved by the second author. We discuss how an extension to the infinitary lambda calculus, where Böhm trees can be directly manipulated as infinite terms, yields a more simple and intuitive explanation of the correctness of these Church-Rosser counterexamples. © 2009 Elsevier Inc. All rights reserved.

U2 - 10.1016/j.ic.2008.09.003

DO - 10.1016/j.ic.2008.09.003

M3 - Article

VL - 207

SP - 559

EP - 582

JO - Information and Computation

JF - Information and Computation

SN - 0890-5401

IS - 5

ER -