Girard's original texts concerning this is magnificent. Everyone needs to know more about Girard.
I had to google ELI5 :-)
First:
OK, now what the result means is that Brown and Palsberg achieve to create a system of types that allows to formally describe the objects (words, numbers) used in interpreters that can interpret themselves.
Why is that astonishing? Interpreters have been around for a long time, or? Including those that interpret themselves (which is called bootstrapping). Yes, but most of these use only very simple types. The power of the types used in a programming languages limits the way one can reason about the programs in the language. For the simple lamguages the interpreted programs are just a bunch of words. It is not possible to state that the bunch of words is a valid program. The System F mentioned above is quite powerful mathematically speaking. Fω even more. But both were not able to describe a program which interprets itself as valid program. This was achieved by System U.
System F is a type theory which is a formal system which is an alternative to set theory, so...
Yes, I quite realize, being something of a type-theory geek myself. What System F is not is a dependent type theory, with a proposition type and strong normalization, or even a propositional fragment in which proofs must normalize, or types dependent on values (which you need, in order to get proper propositional reasoning!).
A self-interpreting variant on Martin-Loef or Homotopy Type Theory would have been astounding! But that's not what this is.
Decidability has a price. So apparently you are dissatisfied by this result or consider it trivial. I think this buys a lot. Waht are you missing?
Decidability is not actually what we want here :-p. I could go into elaborate descriptions of what we want, but those would be theory-laden with my own ideas. Read my backlog on here to get an idea of the general direction I'm thinking in.
This result is not trivial, but it's useful for talking about Turing-complete programming languages, not about logic.
This is no such advancement for AI research. This only provides the possibility of typechecking your AI, which is neither necessary nor sufficient for self-optimizing AI programs.
I like how you made this comment, and then emailed me the link to the article, asking whether it actually represents something for self-modifying systems.
Now, as to whether this actually represents an advance... let's go read the LtU thread. My guess is that the answer is, "this is an advancement for self-modifying reasoning systems iff we can take System U as a logic in which some subset of programs prove things in the Prop type, and those Prop-typed programs always terminate."
However, System U is not strongly normalizing and is inconsistent as a logic.
So, no.
But also:
Anyway, the big deal here is:
"Our techniques could have applications... to growable typed languages..."
Curry-Howard tells us types are logical propositions. Mathematicians from Bayes to Laplace to Keynes to Cox to Jaynes have told us probability is an extension of logic or (as I prefer) logical truth/falsehood are limiting cases of probability. Alternatively, probability/logic are measures of information, in the algorithmic information theory sense. So a "growable typed language" seems it would have obvious benefits to machine learning and probabilistic programming generally. In other words, it's not inherently a big deal not to be strongly normalizing or have decidable type checking by default—that just means the system doesn't yet have enough information. But when the system acquires new information, it can synthesize new types and their relations, "growing" the typed language.
It's hard to overstate how significant this is.
I read the LtU thread as well, and began to wonder if Snively was stealing from me.
But no, you need a normalizing fragment to have a Prop sort. Or at least, you need more than this, particularly a solid notion of a probabilistic type theory (which linguists are at the beginning of forming) and Calude's work in Algorithmic Information Theory, to actually build self-verifying theorem-proving type-theories this way.
This is no major result indeed. Neither necessary nor sufficient. But if you want safe self-optimizing AI you (and the AI) need to reason about the source. If you don't understand how the AI reasons about itself you can't control it. If you force the AI to reason in a way you can do too, e.g. by piggybacking on a sufficiently strong type system, then you at least have a chance to reason about it. There may be other ways to reason about self-modifying programs that don't rely on types but these are presumably either equivalent to such types - and thus the result is helpful in that area too - or more general - in which case proofs become likely more complicated (if feasible at all). So some equivalent to these types is needed for reasoning about safe self-modifying AI.
Self-Representation in Girard’s System U, by Matt Brown and Jens Palsberg:
In 1991, Pfenning and Lee studied whether System F could support a typed self-interpreter. They concluded that typed self-representation for System F “seems to be impossible”, but were able to represent System F in Fω. Further, they found that the representation of Fω requires kind polymorphism, which is outside Fω. In 2009, Rendel, Ostermann and Hofer conjectured that the representation of kind-polymorphic terms would require another, higher form of polymorphism. Is this a case of infinite regress?We show that it is not and present a typed self-representation for Girard’s System U, the first for a λ-calculus with decidable type checking. System U extends System Fω with kind polymorphic terms and types. We show that kind polymorphic types (i.e. types that depend on kinds) are sufficient to “tie the knot” – they enable representations of kind polymorphic terms without introducing another form of polymorphism. Our self-representation supports operations that iterate over a term, each of which can be applied to a representation of itself. We present three typed self-applicable operations: a self-interpreter that recovers a term from its representation, a predicate that tests the intensional structure of a term, and a typed continuation-passing-style (CPS) transformation – the first typed self-applicable CPS transformation. Our techniques could have applications from verifiably type-preserving metaprograms, to growable typed languages, to more efficient self-interpreters.