[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.


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

Γ  ⊢ M  : τ
---------- (τ =E  σ)
Γ ⊢ M   : σ
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 E =  {a1 = (a2 →  a1) ∧ (a1 → a1), a2 = a1 → a2} . 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 defined 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]  
© 2006 Dip. Informatica - Universita di Torino
Last modified: July 21, 2014