The relationship between large cardinals and program termination

Solution 1:

This isn't really an answer, but it's way way too long for a comment. I just want to offer some commentary on the linked answer. Re: your actual questions, you might find this paper interesting.

I think that Neel's$^*$ comment is somewhat misleading.

Let's start from the basic side of things: how do large cardinals imply facts about arithmetic? (Via Godelization, facts about program behavior are "really" facts about arithmetic.) The simplest answer is via consistency claims. The statement "ZFC is consistent" is a $\Pi^0_1$ sentence (look up the arithmetic hierarchy if you're not already familiar with it). It is also implied (over ZFC) by the existence of a weakly inaccessible cardinal; this is because ZFC proves the statement "If $\alpha$ is weakly inaccessible, then $L_\alpha\models$ ZFC." So this is an example of a fact about arithmetic which is implied by a large cardinal statement.

This can be directly turned into a statement about program termination, as follows. For a given computably axiomatizable theory $T$ (such as ZFC), we can write a program $\pi_T$ which halts iff $T$ is inconsistent - basically, $\pi_T$ just searches for a proof of a contradiction from $T$, and halts iff it finds one.

As an aside: the task of finding reasonably small programs which "represent" certain properties of a given theory, or at least have meaningful properties which can't be proved in a given theory, is an interesting one. See e.g. this work by Aaronson and Yedidia on a short program which runs forever, but which ZFC can't prove runs forever.

Essentially, the following is a basic fact about computability and provability:

The consistency of a given computably axiomatizable theory $T$ is equivalent to the non-termination of a program associated to $T$, and consistency statements often follow from large cardinals.

So that's a sense in which large cardinals can lead to statements about the behavior of programs. It's even better than that: the program $\pi_T$ associated to $T$ is optimal, in the sense that a reasonable theory (much much less than ZFC - even less than PA!) proves that $\pi_T$ terminates iff $T$ is inconsistent. In particular, to each large cardinal axiom A we can associate a program $\sigma_A$ such that $\sigma_A$ terminates iff ZFC+A is inconsistent. So:

The consistency with ZFC of a given large cardinal axiom is equivalent to the non-termination of a certain program.

So this connects the consistency of large cardinals with the non-termination of programs.

But that's not what Neel said! He said that large cardinals were equivalent to statements about program termination.

Now on the face of it, this is outright false: statements about program termination are arithmetic statements, and these can't depend on the actual truth of large cardinal axioms. Precisely, if A is (what would generally be recognized as) a large cardinal axiom, then ZFC does not prove "$\varphi$ is equivalent to A" - or even "$\varphi$ implies A" for any arithmetic sentence $\varphi$ unless ZFC actually disproves A.

This may sound mysterious, but there's actually much less to it than meets the eye. Fix a large cardinal axiom A = "there is a cardinal $\kappa$ such that [stuff]." The [stuff] will always imply that such a $\kappa$ gives a model of ZFC, that is, that $L_\kappa\models$ ZFC (this is a sociological claim about what constitutes a "large cardinal" - the term "large cardinal" is not a precise one).

OK, so suppose ZFC doesn't disprove A. Then by Godel's completeness theorem, ZFC + A has a model $M$. Now let $\kappa$ be the least ordinal in $M$ such that either $M\models$[stuff]$(\kappa)$ or for some $\alpha\in Ord^M$, $\kappa\in L_\alpha^M$ and $L_\alpha^M\models$[stuff]$(\kappa)$. (This isn't necessarily the actual least witness to A - it could be smaller.) By the note above, we have $L_\kappa^M\models$ ZFC, but by definition of $\kappa$ we also have $L_\kappa^M\not\models$ A. However, the set of natural numbers didn't change between $M$ and $L_\kappa^M$ (since all we did was "cut (the $L$ of) $M$ off" at some infinite level), so $L_\kappa^M$ satisfies all the same arithmetic facts as $M$ itself - in particular, the truth value of $\varphi$ didn't change. So we've shown:

If A is a large cardinal axiom and $\varphi$ is an arithmetic sentence consistent (over ZFC) with A, then $\varphi$ doesn't prove A.

And the case when $\varphi$ isn't consistent (over ZFC) with A is of course trivial, since then $\varphi$ can't be equivalent (over ZFC) with A unless A is inconsistent.

So in what sense was Neel's claim correct?

I think he was making a point about the semantics of programming languages. This is not a subject I know much about, so I may be wrong here, but my understanding is as follows:

The idea here is to create an actual mathematical structure associated to a given programming language. My understanding is that often, if not usually, this structure is a category with various nice properties and possibly additional structure. Incidentally, the precise details of the structure can be subtle - see e.g. this discussion of whether the "categorical" semantics for Haskell actually is a category. (I am totally unqualified to comment on this specific issue, by the way. If you're interested you might ask a question here about it.)

The point now is that the following can, and apparently does, occur:

There is a semantics $\mathcal{S}$ for a programming language FOO, such that the non-termination of certain programs in FOO are equivalent to the existence of certain corresponding large cardinal axioms, appropriately re-interpreted into the relevant framework, in the structure $\mathcal{S}$.

That is, the construction of $\mathcal{S}$ from FOO is somehow canonical, and we're not speaking of the non-termination claim as implying the genuine existence of a large cardinal, but rather as implying a fact about the internal structure of the object $\mathcal{S}$.

Note the phrase "appropriately re-interpreted." A large cardinal axiom stated in the language of set theory doesn't immediately make sense in the context of, say, category theory. Instead, we need to look for an appropriate equivalent. A neat example of this is the equivalence, due to Blass, of the existence of a measurable cardinal and the existence of an exact functor $F$ from Sets to Sets which isn't naturally equivalent to the identity. Now, if we're given some "appropriate" category $\mathcal{C}$, it perhaps makes sense to say "$\mathcal{C}$ thinks there is a measurable cardinal" iff the statement "there is an exact functor $\mathcal{C}\rightarrow\mathcal{C}$ not equivalent to the identity" is true.

So I suspect that this is what Neel means when he says that claims about termination are equivalent to set-theoretic claims: that when we look at the canonical semantics for a given programming language, termination facts are reflected by internal set-theoretic properties of that structure.

$^*$I'm not sure what the etiquette is regarding names; I've used first name, but I'm happy to use full name or professional title or etc. if that's the better standard.

Solution 2:

I think the comment you quote means less than you think it does.

First of all, it's not about whether individual programs terminate, but whether all programs in a given programming language terminate. This is often a trivial question: In every actually used general-purpose programming language it is pretty clear that of course there's a way to write an infinite loop.

There are also non-general programming languages that are deliberately designed such that they only allow terminating programs to be written. As we all know, this comes at a cost: there will inevitably be total recursive functions that the language cannot express.

Neel is/was apparently engaged in pushing the boundaries of that: finding a way to define a programming language such that all valid programs terminate, and yet a usefully large class of functions can be written in a reasonably straightforward way. When he says "modern programming languages are type theories", he's expressing hope/belief that good solutions to that problem will come as an integrated result of the language's type system -- the rules that prevent a program from doing nonsensical/dangerous things like treating a number from its input like a memory address -- rather than a bolt-on static analysis that exists only to verify that programs are total. These type systems are closely related to type theories in logic and category theory.

(Note that for practical purposes a language that guarantees just that everything is total is of questionable utility: if you're running code you got from an untrusted source and want to be sure they didn't trick you into running something that never terminates, you also want to be sure that they won't trick you into trying to calculate Graham's number in base 23, even though that is theoretically a terminating task).

What Neel seems to be saying is that some of the proposed solutions have the property that ZFC cannot prove that they work (as in, that all valid programs in such-and-such system terminates), but that ZFC plus such and such often-accepted large cardinal assumption can.

He's probably not, in light of Noah's arguments, asserting that "this type system works" implies that such and such large cardinal must exist. But it is conceivable that he can prove "this type system works" equivalent to "such and such large cardinal axiom is relatively consistent with ZFC". These are both statements of the same general flavor (there are solid connections between consistency of logics and totality of programming languages, e.g. via the Curry-Howard correspondence), so it wouldn't be outrageous for them to imply each other.