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 permitted. 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.
Tue 22 OctDisplayed time zone: Pacific Time (US & Canada) change
14:00 - 15:30 | |||
14:00 20mKeynote | Jens, the Ultimate PL Renaissance man! JENSFEST Vivek Sarkar Rice University, USA | ||
14:20 25mTalk | The Essence of the Flyweight Design Pattern JENSFEST Fernando Magno Quintão Pereira Federal University of Minas Gerais, Caio Raposo Universidade Federal de Minas Gerais | ||
14:45 25mTalk | The Normalization Barrier Revisited JENSFEST | ||
15:10 20mTalk | Input Reduction with Reduction Trees JENSFEST Christian Gram Kalhauge Technical University of Denmark |