Submitted by Robin Adams
Statement. Does Expansion Postponement hold for every PTS?
Problem Origin. This property was ﬁrst conjectured by Pollack [Pollack, 1992] .
We can replace the usual conversion rule in a Pure Type System (PTS):
with the following two rules:
Expansion Postponement (EP) is the conjecture that every derivable judgement in a PTS has a derivation in which the expansion rule is used at most once, as the ﬁnal step in the derivation.
This was proposed by Pollack in 1992 [Pollack, 1992], where he showed that it is a necessary condition for the type-checking algorithm given there to be complete. Gutiérrez and Ruiz [Gutiérrez and Ruiz, 2003] proved that it is a necessary condition for cut elimination in a sequent calculus formulation of PTSs.
It was shown by Erik Poll [Poll, 1998] to hold for every weakly normalising PTS, and by Barthe [Barthe, 1998] to hold for injective PTSs.