View Related Documents

Abstract

Klop’s Problem is finding a type for characterizing hereditary head normalizing terms, that is, lambda-terms whose Böhm trees do not contain the bottom. This paper proves that this problem does not have any solution by showing that the set of those terms is not recursively enumerable. This paper also gives a best-possible solution by providing an intersection type system with a countably infinite set of types such that typing in all these types characterizes hereditary head normalizing terms. By using the same technique, this paper also shows that the set of lambda-terms normalizing by infinite reduction is not recursively enumerable.

Fulltext Preview

Image of the first page of the fulltext document