You're looking at Less Wrong's discussion board. This includes all posts, including those that haven't been promoted to the front page yet. For more information, see About Less Wrong.

Gunnar_Zarncke comments on [Link] Self-Representation in Girard’s System U - Less Wrong Discussion

2 Post author: Gunnar_Zarncke 18 June 2015 11:22PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Article Navigation

Comments (13)
Tags: programming-language self-representation ai lambda-calculus

Comments (13)

You are viewing a single comment's thread. Show more comments above.

Comment author: Gunnar_Zarncke 29 June 2015 09:33:55AM 0 points [-]

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.

Comment author: [deleted] 29 June 2015 11:10:03PM 0 points [-]

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.

Powered by Reddit Powered by Reddit