Two beta-equal lambda-I-terms with no types in common
RIS ID
87051
Abstract
It is known that in the Curry-style type-assignment system for simple type-theory there exist two closed lambda-K-terms that are beta-equal but have no types in common. This note extends that result to lambda-I-terms.
Publication Details
Bunder, M. W. & Hindley, J. R. (1996). Two beta-equal lambda-I-terms with no types in common. Theoretical Computer Science, 155 (1), 265-266.