Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega

Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega, by Matt Brown and Jens Palsberg:

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.

I haven't gone through the whole paper, but their claims are compelling. They have created self-interpreters in System F, System Fω and System Fω+, which are all strongly normalizing typed languages. Previously, the only instance of this for a typed language was Girard's System U, which is not strongly normalizing. The key lynchpin appears in this paragraph on page 2:

Our result breaks through the normalization barrier. The conventional wisdom underlying the normalization barrier makes an implicit assumption that all representations will behave like their counterpart in the computability theorem, and therefore the theorem must apply to them as well. This assumption excludes other notions of representation, about which the theorem says nothing. Thus, our result does not contradict the theorem, but shows that the theorem is less far-reaching than previously thought.

Pretty cool if this isn't too complicated in any given language. Could let one move some previously non-typesafe runtime features, into type safe libraries.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

This is why I heart LtU

It is all very much over my head (surprise) but moving "some previously non-typesafe runtime features, into type safe libraries" is music to my ears. :-)

I don't trust it

The reason is that the theorem assumes that terms are represented as numbers using Gödel numbering. We show that a typed representation can ensure that the diagonalization gadget central to the proof fails to type check. (Emphasis mine.)

I don't fully understand this but I don't buy into a solution which claims to have blocked a proof by making part of it inexpressible.

That seems odd considering

That seems odd considering making undesirable outcomes inexpressible is a primary motivation for types.

Yeah well.

It's the old meta- and object-logic debate we also had with Hewitt. The fact that you blocked an argument doesn't imply you blocked all arguments, and even the fact that something cannot be proven anymore in an object logic is problematic when you consider it can still be proven in a more expressive meta-logic. Even if you consider that object-logic should conflate with meta-logic.

I don't know exactly what they did. I don't feel like reading the argument that close, that would take months for me, but I can't say I trust this result that much. More, since it seems to 'disprove' something which is generally accepted; where disprove is between quotes since I don't know what they did exactly.

Classic "theorems" like

Classic "theorems" like Gödel's often aren't really theorems in the limited prosaic sense of something you could run through, say, Coq; they're deep insights. In Gödel's case, the really deep insight was that types can't protect a formal system against the incompleteness/inconsistency problem because types, unless they actually cripple the power of the system, can only prevent the system from acknowledging that it has a problem, they don't prevent the problem from being there. This paper might be getting around its problem by a legitimately clever technique, but the abstract fails to get that accross — it makes it sound as if they're claiming to block a proof with a gag order, which is in essence what Gödel realized doesn't work.

Their correctness theorem is restricted

Gödel proved that a logic can't prove its own consistency, so you just need a self-interpreter that doesn't prove consistency. As shown in other work (and not discussed here), usually an interpreter lets you prove consistency — that is, it lets you prove that the object language cannot express object-level proofs of absurdity. If you have a term `e : Expr EmptyType` (an object-level proof of absurdity), with a typed interpreter you can produce a term `interp e : EmptyType`, which is absurd.

However, the correctness theorem of their interpreter is more restricted — it guarantees that `interp (quote e)` reduces to `e`. So the above proof needs the extra hypothesis `e: EmptyType` to produce a proof of `EmptyType` — so we end up proving `EmptyType -> EmptyType`, which is quite true.

They don't claim to disprove

They don't claim to disprove Gödel (and barely mention it) — in fact, the "normalization barrier" has never been stated formally anywhere to my knowledge. (I've tried formalizing it with my colleagues for some time, and had run into some of the loopholes they're using).

Also, there's a huge difference with Hewitt: not only this was accepted by peer review at a reputable venue, but their code and proofs can be downloaded.

(At best, there's the remote possibility of a bug in their FOmega typechecker that their code happens to exploit and that nobody who understood the paper caught, but that seems very unlikely, also because it is well understood how to implement one).

I still don't like it

If you block an argument that doesn't imply you blocked all arguments.

I simply don't like that part of their argument as it was stated in the article. Possibly, it is phrased in a manner which doesn't do justice to their technical argument. I wouldn't know, I am not going to read this paper.

(Let's not discuss Hewitt.)

Yeah, but...

You might have a point on the phrasing, or not. But it's not so productive to get to the bottom of that hole, so let's set that aside and get on the content.

In this case, arguably, there's only one actual argument suggesting what they did is impossible: a total self-interpreter for a total language is impossible. But if one looks at the actual statement, it doesn't actually forbid their scenario. And if you try to apply *the* known proof, it fails for typing reasons: the proof depends crucially on creating some specific term in the object language, and that term is ill-typed. Gödel didn't prove that you can circumvent all typing restrictions.

You can imagine other attempts to prove the same theorem, but they exhibit their self-interpreter I. So assuming mathematics is consistent, attempts to prove that I doesn't exist will fail. To be sure that I exists, you can just look at I, you don't need to look at each proof in detail; you can still do it, but for other reasons (like I do in another comment).

re they don't claim to disprove

Also, there's a huge difference with Hewitt: not only this was accepted by peer review at a reputable venue, but their code and proofs can be downloaded.

Hewitt is making a pretty simple claim that shouldn't be all that controversial but this forum reacted very disappointingly.

Misleading title.

As I read the paper what is claimed appears to be a compiler from of notation to another.

Given that compilers for turing complete languages have already been written in coq (aka CompCert) this result does not appear partivularly novel.

Further the conclusion specifically mentions that a function performing beta reduction was not implemented. Beta reduction is how functions are converted into normal forms in the lambda calculus. Aka the paper does not implement function evaluation and as such do not implement the naive understanding of an interpreter, written in the language executing any code written in the language.

I just skimmed the

I just skimmed the introduction and conclusion, but I think they do claim to implement beta-reduction. Section 9-Terminology distinguishes between two types of self-interpreters. An "unquoter" takes an AST and returns the value it represents (unquote "2+2" --> 4), while a "self-reducer" takes and AST and returns an AST of the value it represents (self-reduce "2+2" --> "4"). They claim to implement the former.

I read it a bit differently

I thought they realized an unquoter, so in the strict sense, unquote "2+2" -> 2+2, which finally reduces to 4 within the system.

I guess an unquoter is more than sufficient, even more ideal, than an interpreter.

Still not sure what they aim to do. At worst, if they can prove to do something which should really be forbidden, they broke some important logics, chaos reigns, and people are back to sticks and stones; i.e., you can only prove what you can calculate.

Eh, I don't think it's that bad

Eh, I don't think it's that bad. :) They work in the standard System Fω, which is a very well understood language, and definitely sound. So I don't think this "loophole" will lead to any logical inconsistency. I think the main conclusion is that the definition of "self interpreter" gives a little more wiggle room than you would think.

I think the main limitation is that, as they write, their quotation function can not be written in System Fω. That is, you can't write an interpreter that takes an Fω program written as a string and evaluates it to a value. Instead, first you have to take the string and "quote" it as a value in their clever representation, and then you can evaluate that value, but the quotation step happens outside the system.

This is particularly clear if you think about their "cheating" encoding in Section 3.3, where a program is encoded as just that program itself with a few extra identity functions scattered through it. If you tried to to write a program which converted from strings into that representation, basically you would have to take strings like "(λn. n+2)" and convert them to functions like (λn. n+2). That is, you would have to write an "ordinary" self-interpreter, which we know is impossible! :)

Reflection

Does this mean the have banned reflection, as you can't turn code into an interpretable string?

Edit: That doesn't seem right now, its more like you cannot interpret flat strings, but you can interpret some other structured syntax. Could you write something that converted from the language AST to the quoted format? Then reflection would still be possible. In that case you could introduce a display transformation that inserts the quoting, and then the code the user inputs would look the same as when it is displayed. Does it really matter that the code is not representable as a flat string within the language itself?

Typed reflection

I'm not sure how you define reflection; the goal here is to support reflection on typed code (at least, that was the goal when my colleague Tillmann introduced typed self representation with my boss).

I think you can do reflection as long as you start from "typed" syntax, but (I believe) you can't go from untyped syntax to typed syntax (the "quoted" format) *in general*.

There shouldn't be any interesting difference between different untyped syntaxes, ranging from Gödel codes to strings to ASTs, so let's pick Gödel codes.

A typed interpreter takes Expr t to t (or, technically Expr (\overline{t}) to t); Expr t is the typed syntax, and t is a type variable. If you could go from a Gödel code to Expr t (for the right t), then you could evaluate the result with the typed interpreter, and you'd have a total language with an untyped self-interpreter — which we know from computability is impossible (as they describe in Sec. 3.1). So you can't get from Gödel codes to typed syntax in general — I like to say, you can't write a self-typechecker.

While (IIRC) the paper doesn't show how to combine typed syntax together, you can write some combinators, and use them if you have enough input. For instance, if `a` is an `Expr (T1 -> T2)`, and `b` is an `Expr T1`, you should be able to apply `a` to `b`.

On the other hand, if you don't know well the types of `a` and `b`, you can't match on the types (as far as I can tell) and check if they're compatible. That's I think a likely problem in practice if you try writing a self-typechecker. If you add a value-level representation of types, you get different problems.

desiderata?

I think the operations you want are easy to implement if the representation of lambda term X is a pair (Godel number of X, normal form of X). To compose two of those, just compose the normal forms and concatenate the Godel numbers. Other operations like eval or pretty printing are also trivial. Or am I missing something and their "typed syntax" has more interesting desiderata?

Typing is hard

The typing is really really hard. A typed interpreter for a language with addition, say, and pairs (and nothing else) usually requires GADTs or Church-encoding. I recommend you try or look up answers.
Now you want to represent polymorphic functions in this typed syntax, in such a way that you can apply them and get the right type.

And once you have the self-interpreter, you need to make sure that you can also write and type other operations — and in many attempts, that's often only possible for some operations but not others. Their set of benchmarks is the most successful ever.

All you have explained is the easy part (and I'm not sure "concatenate Gödel numbers" is quite correct, but some actual operation exists).

thanks!

Thanks, I think I understand the paper a bit better now. Here's a quick recap, just to make sure I got everything right:

Since we provably can't have an eval function that accepts a program's source code (Godel number), we will instead make it accept a "typed representation" - a value of some type Expr<T> where T is the program's return type. The main requirement is that all constructible values of type Expr<T> must be in one-to-one correspondence with valid programs that return T. (That means you can't just represent a program by its return value, or its return value paired with its source code, etc.)

With such a typed representation, the problem becomes much simpler. The usual counterexample with diagonalization no longer typechecks, and writing a self-interpreter in the most direct and obvious way will just work (section 3.3 of the paper). The main unsolvable problem was actually going from the source code to the typed representation, which is less like source code and more like verified executable code with a bunch of annotations.

From that point, the game is about how many "annotations" you can stick in. I suppose it's pretty exciting but I haven't parsed that part yet. Overall, good paper, though it's way too easy to misunderstand.

Sec. 3.3: An easy counterexample to the normalization barrier

What's described in Sec. 3.3 is not what I'd call the most obvious self-interpreter — (though maybe you did understand what happens and just have different expectations). Regardless, I'll give my summary of 3.3: it's a trivial self-interpreter, but it gives a counterexample to the supposed "normalization barrier" and you can explain it quickly to anybody understanding System F (at least on a whiteboard, I'll try here).

As they say there,

The quoter [described in this Section] will support only the self-interpreter and nothing else.

In particular, on that representation you can't do anything else you'd expect to do on an AST — say, pattern matching or transformations. The representation is a function `\id -> body`, and as they say, you can prove that the `id` argument must be the polymorphic identity function (Haskell's id) by parametricity.

In very imprecise terms, the quoted program uses id as a strange sort of callback.
The goal is that quoting always produces a normal form.
For instance, take program `(\x -> (+) x 1) 41`. Evaluating it would reduce to 42, but if you quote it you get `\id : ... . (id (\x -> (id ((id (+)) x) 1))) 41`, where each application is stuck until you get the `id` argument. The self-interpreter simply provides that argument.

I find it hard to call this "obvious way" — if you want, it's the most extreme form of metacircular interpretation, but somehow people seldom discuss this.
As they say, this result (unlike the other ones) holds also for System F and for bigger systems, while the main self-interpreter they provide is just for Fomega, not for smaller or bigger systems.

For a preview of the rest, I suggest you to skip a bit to Sec. 7 and see which operations they implement. They'll probably look somewhat obvious (except maybe the CPS transformation); yet, they're the first to support all of them at the same time.

Also, people have used a typed representation for much longer, so that's not enough to solve all problems. The other big problem is described in Sec. 4 (though I already forgot Sec. 4.2 again).

thanks again

Yeah, I understood the interpreter from section 3.3 in the same way as you describe. It comes together easily once you see that it should only support eval, and it's very natural that it would work in many different systems. Actually it seemed more fundamental to me than the main result, because the problem solved by the main result is not as concisely specified, unless I'm missing something.

Can their representation be converted to string?

Just something which I wondered about.

Thanks to you too

Thanks for the summary. I want to read the details sometime to see how it relates to what I've written about. Sounds like this moves 'encode' out of the language, whereas I move a tiny part of eval out of the language.

Correction on previous work

Previously, the only instance of this for a typed language was Girard's System U, which is not strongly normalizing.

Ahem, that's not the only instance. The first self-interpreter in a typed language was from Tillmann Rendel, Klaus Ostermann and Christian Hofer in 2009 (whose research group I later joined). However, unlike System U, their language (System Fomega*) did not have decidable typechecking (though in my experience this was a purely theoretical concern), and IIUC nobody yet knows whether it is strongly normalizing:

http://www.cs.au.dk/~chmh/tsr/