The Normalization Barrier Revisited

In a POPL 2016 paper, Brown and Palsberg presented a breakthrough result on "the normalization barrier." The normalization barrier, according to conventional wisdom, originates from a theorem in computability theory, which says that a total universal function for all total computable functions is impossible. Therefore, it was widely believed that strongly normalizing lambda calculi do not have self-interpreters either. However, Brown and Palsberg constructed a self-interpreter for F-omega, which is a strongly normalizing lambda calculus. One of the key insights behind the Brown-Palsberg breakthrough is due to the fact that "static type checking in F-omega can exclude the (computability) proof’s diagonalization gadget, leaving open the possibility for a self-interpreter," according to Brown and Palsberg [2016]. In this paper, we revisit this phenomenon. In particular, in the Brown-Palsberg result, terms in F-omega were encoded as typed representations, and an external type checker was assumed to do type checking. In our work, we consider a type checker assumed to be built into the interpreter, which reports type errors on ill-typed inputs. We believe this is closer to real interpreters. Consequently, our representation is untyped, and ill-typed inputs are specifically handled. Under this setting, we show that the original computability theory result still holds. Our result does not contradict the Brown-Palsberg result. Rather, it shows that computability theory results are still applicable to F-omega from a different angle, thus "rebuilding" the normalization barrier.