The typed [lambda]-calculus is not elementary recursive

Home
→
Research Collections
→
Interdisciplinary and Peer-Reviewed
→
View Item

Statman, Richard

1979-07

Citation: Statman, Richard (1979/07)."The typed [lambda]-calculus is not elementary recursive." Theoretical Computer Science 9(1): 73-81. <http://hdl.handle.net/2027.42/23535>

Abstract: We prove that the problem of deciding for closed terms t1, t2 of the typed [lambda]-calculus whether t1 [beta]-converts to t2 is not elementary recursive.

DOIs: http://dx.doi.org/10.1016/0304-3975(79)90007-0

URI: http://www.sciencedirect.com/science/article/B6V1G-45FC46N-47/2/fa4feaa605aa92e559fbc6b53f37adfc

Handle: http://hdl.handle.net/2027.42/23535

Show full item record