Andrej Bauer: On self-interpreters for lambda calculi

Abstract: Matt Brown and Jens Palsberg constructed a self-interpreter for System F omega. They require a self-interpreter to have an injective quoting function and that the source codes be beta-normal. I show that under the same constraints there is a self-interpreter for Gödel's System T, and in fact for any strongly normalizing typed lambda-calculus expressive enough to encode natural numbers and pairs. The proof is a swindle which makes one think that the constraints by Brown and Palsberg are not good enough, but I show that they are essentially the best we could hope for in terms of type complexity. What we need is a better definition of a self-interpreter that takes into account structural properties of self-interpreters.