[Next] [Previous] [Up]

#### Problem # 11

Submitted by Paweł Urzyczyn

Date: 1993

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.

[PRINT this PROBLEM]

Let be a ﬁnite set of equations between intersection types, and let be
the congruence generated by . Extend intersection type assignment by the
rule:

This generalizes the notion of a recursive type introduced via “type constraints”
in the style of [Mendler, 1991].
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).

##### References for # 11

[Mendler, 1991] Mendler, N. (1991). Inductive types and type
constraints in the second-order lambda calculus. Annals of Pure and
Applied Logic, 51(1-2):159–172.

[Next] [Previous] [Up]

Last modified: July 21, 2014