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.
“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.
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.
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
Proptype, and thoseProp-typed programs always terminate.”So, no.
But also:
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
Propsort. 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.