According to conventional wisdom, a self-interpreter for a
strongly normalizing λ-calculus is impossible. We call this
the normalization barrier. The normalization barrier stems
from a theorem in computability theory that says that a total
universal function for the total computable functions is
impossible. In this paper we break through the normalization
barrier and define a self-interpreter for System F_ω, a
strongly normalizing λ-calculus. After a careful analysis of
the classical theorem, we show that static type checking in
F_ω can exclude the proof’s diagonalization gadget, leaving
open the possibility for a self-interpreter. Along with the
self-interpreter, we program four other operations in F_ω, including
a continuation-passing style transformation. Our operations
rely on a new approach to program representation
that may be useful in theorem provers and compilers.
1 comment
[ 2.7 ms ] story [ 15.2 ms ] threadAccording to conventional wisdom, a self-interpreter for a strongly normalizing λ-calculus is impossible. We call this the normalization barrier. The normalization barrier stems from a theorem in computability theory that says that a total universal function for the total computable functions is impossible. In this paper we break through the normalization barrier and define a self-interpreter for System F_ω, a strongly normalizing λ-calculus. After a careful analysis of the classical theorem, we show that static type checking in F_ω can exclude the proof’s diagonalization gadget, leaving open the possibility for a self-interpreter. Along with the self-interpreter, we program four other operations in F_ω, including a continuation-passing style transformation. Our operations rely on a new approach to program representation that may be useful in theorem provers and compilers.