← All problems
Unverified
Weak versus Strong Normalization for Pure Type Systems
A Pure Type System (PTS) is weakly normalizing if every typable term has at least one finite reduction sequence to a normal form. It is strongly normalizing if every reduction sequence from every typable term is finite. Is every weakly normalizing PTS strongly normalizing?
