Constructive proofs of the range property in lambda calculus

DOI10.1016/0304-3975(93)90083-6MaRDI QIDQ1314345zbMATH OpenOpenAlexWikidataFDO

Authors Henk Barendregt

Publication date 26 September 1994

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/2066/17244

zbMATH Keywords

coding of lambda-terms by natural numbersconstructive proofsErshov numerationsrange of a combinatorrange property

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Theory of numerations, effectively presented structures (03D45)

Review text

The range property, conjectured in 1968 by Böhm, says that the range of a combinator \(F\), that is the set of all terms \(F A\) modulo \(\beta\)- convertibility, is either a singleton or an infinite set. This paper recalls first the classical (nonconstructive) proofs and then gives two constructive proofs. The first one adds to Böhm's idea of using a fixed point the coding of lambda-terms by natural numbers. The second is based on Ershov numerations. This leads to a generalization of the range theorem due to Statman.

Recommendations

• scientific article; zbMATH DE number 1670575
• Some results on extensionality in lambda calculus
• Towards the range property for the lambda theory \(\mathcal H\)
• A coinductive confluence proof for infinitary lambda-calculus
• Reducibility Proofs in the λ-Calculus
• A new coinductive confluence proof for infinitary lambda calculus
• scientific article; zbMATH DE number 65536
• A note on the proof theory of the -calculus
• Proof systems for retracts in simply typed lambda calculus

Cites work

• scientific article; zbMATH DE number 3735770 (Why is no real title available?)
• scientific article; zbMATH DE number 3611324 (Why is no real title available?)
• scientific article; zbMATH DE number 3291134 (Why is no real title available?)
• Introduction to generalized type systems
• The lambda calculus, its syntax and semantics
• The λ-calculus is ω-incomplete
• Theoretical Pearls:Representing ‘undefined’ in lambda calculus
• Theorie Der Numerierungen III

Cited in

(11)

• Some results on extensionality in lambda calculus
• Enumerators of lambda terms are reducing constructively
• About the range property for H
• Solution to the range problem for combinatory logic
• Lambda theories allowing terms with a finite number of fixed points
• Existential Type Systems with No Types in Terms
• On the number of fixed points of a combinator in lambda calculus
• Relational graph models at work
• The range property fails for H
• Is sized typing for Coq practical?
• Towards the range property for the lambda theory \(\mathcal H\)

This page was built for publication: Constructive proofs of the range property in lambda calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1314345)