Two beta-equal lambda-I-terms with no types in common

Authors

M W. Bunder, University of WollongongFollow
J R. Hindley, University of Wales

RIS ID

87051

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.

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.