Andrej Bauer: On self-interpreters for lambda calculi

Datum objave: 22. 2. 2016
Seminar za temelje matematike in teoretično računalništvo
Torek, 23. 2. 2016, od 12h do 14h, Plemljev seminar, Jadranska 19
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.