Submitted by Paweł Urzyczyn
Statement. Which equations on intersection types preserve normalization?
Problem Origin. Included in the list of open problems from the “Gentzen” meeting in 1993. Author unknown.
Let be a ﬁnite set of equations between intersection types, and let be the congruence generated by . Extend intersection type assignment by the rule:
Under what condition such a type assignment system has the (strong) normalization property? As an example consider . This system is not “positive” or “monotone” (cf. Problem 1) yet it is believed to be strongly normalizing. Note: As shown in [Mendler, 1991], positivity is a necessary and sufficient condition for strong normalization of a system deﬁned by equations between simple types (without intersections).