A closed λ-term E is called an enumerator if M ε /gL/dg /gTn ε N E/drn/dl = β M. Here Λ° is the set of closed λ-terms, N is the set of natural numbers and the /drn/dl are the Church numerals λfx./tfnx. Such an E is called reducing if moreover M ε /gL/dg /gTn ε N E/drn/dl /a/gb M. In 1983 I conjectured that every enumerator is reducing. An ingenious recursion theoretic proof of this conjecture by Statman is presented in Barendregt . The proof is not intuitionistically valid, however. Dirk van Dalen has encouraged me to find intuitionistic proofs whenever possible. In the lambda calculus this is usually not difficult. In this paper an intuitionistic version of Statmans proof will be given. It took me somewhat longer to find it than in other cases
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/0168-0072(94)00022-u
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 71,489
Through your library

References found in this work BETA

The Lambda Calculus. Its Syntax and Semantics.E. Engeler - 1984 - Journal of Symbolic Logic 49 (1):301-303.

Add more references

Citations of this work BETA

Add more citations

Similar books and articles

The Proofs of $Alpha Rightarrow Alpha$ in $P - W$.Sachio Hirokawa - 1996 - Journal of Symbolic Logic 61 (1):195-211.
A Gitik Iteration with Nearly Easton Factoring.William J. Mitchell - 2003 - Journal of Symbolic Logic 68 (2):481-502.
Strong Normalization and Typability with Intersection Types.Silvia Ghilezan - 1996 - Notre Dame Journal of Formal Logic 37 (1):44-52.
Topological Representation of the Lambda-Calculus.Steve Awodey - 2000 - Mathematical Structures in Computer Science 10 (1):81-96.
Decomposable Ultrafilters and Possible Cofinalities.Paolo Lipparini - 2008 - Notre Dame Journal of Formal Logic 49 (3):307-312.
More on Regular Reduced Products.Juliette Cara Kennedy & Saharon Shelah - 2004 - Journal of Symbolic Logic 69 (4):1261 - 1266.
Stationary Sets and Infinitary Logic.Saharon Shelah & Jouko Väänänen - 2000 - Journal of Symbolic Logic 65 (3):1311-1320.
Weakly Normal Closures of Filters on $P_kappa Lambda$.Masahiro Shioya - 1993 - Journal of Symbolic Logic 58 (1):55-63.
New Directions in Type-Theoretic Grammars.Reinhard Muskens - 2010 - Journal of Logic, Language and Information 19 (2):129-136.


Added to PP index

Total views
19 ( #585,317 of 2,520,788 )

Recent downloads (6 months)
1 ( #405,623 of 2,520,788 )

How can I increase my downloads?


My notes