I’d like to ask a not-too-closely related question, if you don’t mind.
A Curry-Howard analogue of Gödel’s Second Incompleteness Theorem is the statement “no total language can embed its own interpreter”; see the classic post by Conor McBride. But Conor also says (and it’s quite obviously true), that total languages can still embed their coinductive interpreters, for example one that returns in the partiality monad.
So, my question is: what is the logical interpretation of a coinductive self-interpreter? I feel I’m not well-versed enough in mathematical logic for this. I imagine it would have a type like “forall (A : ’Type) → ‘Term A → Partiality (Interp A)”, where ‘Type and ’Term denote types and terms in the object language and “Interp” returns a type in the meta-language. But what does “Partiality” mean logically, and is it anyhow related to the Löbstacle?
So, my question is: what is the logical interpretation of a coinductive self-interpreter?
The logical interpretation of a coinductive self-interpreter is something that says, roughly, “If you keep feeding me computing power, someday I might self-interpret!”. And indeed, if you eventually feed it enough compute-power, it will self-interpret. You just wouldn’t be able to prove ahead of time that it does so.
But what does “Partiality” mean logically, and is it anyhow related to the Löbstacle?
“Partiality” in PL terms means “the type contains \Bot, the Bottom element”. The Bottom element is the type-theoretic element for representing nontermination.
If you can construct \Bot-the-element, you can prove \Bot-the-type, which is also called False, and implies all other propositions and types by the Principle of Explosion. The Second Incompleteness Theorem roughly says:
“In order to self-verify, you must prove that your proof procedure implements the logic you believe in an infinite number of cases. Normally you could try to do that by induction, but since you only have a finite-sized axiom scheme to go on, while your language is Turing-complete, you will never have enough information to verify every possible proof of every possible theorem via inductive application of your axioms, so you’ll have to check some ‘by hand.’ That will take infinite time, so you’ll never finish. Or, if you presume that you did finish, it meant you proved \Bot and thus obtained all other propositions by Explosion.”
As we’ve seen, such a sublanguage (perhaps called `Ask’, a part of Haskell
which definitely excludes Hell) cannot contain all the angels, but it
certainly admits plenty of useful ones who can always answer mundane
things you might Ask. It’s ironic, but not disastrous that lucifer, the
evaluation function by which Ask’s angels bring their light, is himself an
angel, but one who must be cast into Hell.
I’d like to ask a not-too-closely related question, if you don’t mind.
A Curry-Howard analogue of Gödel’s Second Incompleteness Theorem is the statement “no total language can embed its own interpreter”; see the classic post by Conor McBride. But Conor also says (and it’s quite obviously true), that total languages can still embed their coinductive interpreters, for example one that returns in the partiality monad.
So, my question is: what is the logical interpretation of a coinductive self-interpreter? I feel I’m not well-versed enough in mathematical logic for this. I imagine it would have a type like “forall (A : ’Type) → ‘Term A → Partiality (Interp A)”, where ‘Type and ’Term denote types and terms in the object language and “Interp” returns a type in the meta-language. But what does “Partiality” mean logically, and is it anyhow related to the Löbstacle?
The logical interpretation of a coinductive self-interpreter is something that says, roughly, “If you keep feeding me computing power, someday I might self-interpret!”. And indeed, if you eventually feed it enough compute-power, it will self-interpret. You just wouldn’t be able to prove ahead of time that it does so.
“Partiality” in PL terms means “the type contains \Bot, the Bottom element”. The Bottom element is the type-theoretic element for representing nontermination.
If you can construct \Bot-the-element, you can prove \Bot-the-type, which is also called False, and implies all other propositions and types by the Principle of Explosion. The Second Incompleteness Theorem roughly says:
“In order to self-verify, you must prove that your proof procedure implements the logic you believe in an infinite number of cases. Normally you could try to do that by induction, but since you only have a finite-sized axiom scheme to go on, while your language is Turing-complete, you will never have enough information to verify every possible proof of every possible theorem via inductive application of your axioms, so you’ll have to check some ‘by hand.’ That will take infinite time, so you’ll never finish. Or, if you presume that you did finish, it meant you proved \Bot and thus obtained all other propositions by Explosion.”
LoL!