Old Neglected Theorems Are Still Theorems

March 20, 2014

I have very recently been thinking about the question of partiality vs totality in programming languages, a perennial topic in PL’s that every generation thinks it discovers for itself.  And this got me to remembering an old theorem that, it seems, hardly anyone knows ever existed in the first place.  What I like about the theorem is that it says something specific and technically accurate about the sizes of programs in total languages compared to those in partial languages.  The theorem provides some context for discussion that does not just amount to opinion or attitude (and attitude alway seems to abound when this topic arises).

The advantage of a total programming language such as Goedel’s T is that it ensures, by type checking, that every program terminates, and that every function is total. There is simply no way to have a well-typed program that goes into an infinite loop. This may seem appealing, until one considers that the upper bound on the time to termination can be quite large, so large that some terminating programs might just as well diverge as far as we humans are concerned. But never mind that, let us grant that it is a virtue of  T that it precludes divergence.

Why, then, bother with a language such as PCF that does not rule out divergence? After all, infinite loops are invariably bugs, so why not rule them out by type checking? (Don’t be fooled by glib arguments about useful programs, such as operating systems, that “run forever”. After all, infinite streams are programmable in the language M of inductive and coinductive types in which all functions terminate. Computing infinitely does not mean running forever, it just means “for as long as one wishes, without bound.”)  The notion does seem appealing until one actually tries to write a program in a language such as T.

Consider computing the greatest common divisor (GCD) of two natural numbers. This can be easily programmed in PCF by solving the following equations using general recursion:

\begin{array}{rcl}    \textit{gcd}(m,0) & = & m \\    \textit{gcd}(0,m) & = & m \\    \textit{gcd}(m,n) & = & \textit{gcd}(m-n,n) \quad \text{if}\ m>n \\    \textit{gcd}(m,n) & = & \textit{gcd}(m,n-m) \quad \text{if}\ m<n    \end{array}

The type of \textit{gcd} defined in this manner has partial function type (\mathbb{N}\times \mathbb{N})\rightharpoonup \mathbb{N}, which suggests that it may not terminate for some inputs. But we may prove by induction on the sum of the pair of arguments that it is, in fact, a total function.

Now consider programming this function in T. It is, in fact, programmable using only primitive recursion, but the code to do it is rather painful (try it!). One way to see the problem is that in T the only form of looping is one that reduces a natural number by one on each recursive call; it is not (directly) possible to make a recursive call on a smaller number other than the immediate predecessor. In fact one may code up more general patterns of terminating recursion using only primitive recursion as a primitive, but if you examine the details, you will see that doing so comes at a significant price in performance and program complexity. Program complexity can be mitigated by building libraries that codify standard patterns of reasoning whose cost of development should be amortized over all programs, not just one in particular. But there is still the problem of performance. Indeed, the encoding of more general forms of recursion into primitive recursion means that, deep within the encoding, there must be “timer” that “goes down by ones” to ensure that the program terminates. The result will be that programs written with such libraries will not be nearly as fast as they ought to be.  (It is actually quite fun to derive “course of values” recursion from primitive recursion, and then to observe with horror what is actually going on, computationally, when using this derived notion.)

But, one may argue, T is simply not a serious language. A more serious total programming language would admit sophisticated patterns of control without performance penalty. Indeed, one could easily envision representing the natural numbers in binary, rather than unary, and allowing recursive calls to be made by halving to achieve logarithmic complexity. This is surely possible, as are numerous other such techniques. Could we not then have a practical language that rules out divergence?

We can, but at a cost.  One limitation of total programming languages is that they are not universal: you cannot write an interpreter for T within T (see Chapter 9 of PFPL for a proof).  More importantly, this limitation extends to any total language whatever.  If this limitation does not seem important, then consider the Blum Size Theorem (BST) (from 1967), which places a very different limitation on total languages.  Fix any total language, L, that permits writing functions on the natural numbers. Pick any blowup factor, say 2^{2^n}, or however expansive you wish to be.  The BST states that there is a total function on the natural numbers that is programmable in L, but whose shortest program in L is larger by the given blowup factor than its shortest program in PCF!

The underlying idea of the proof is that in a total language the proof of termination of a program must be baked into the code itself, whereas in a partial language the termination proof is an external verification condition left to the programmer. Roughly speaking, there are, and always will be, programs whose termination proof is rather complicated to express, if you fix in advance the means by which it may be proved total. (In T it was primitive recursion, but one can be more ambitious, yet still get caught by the BST.)  But if you leave room for ingenuity, then programs can be short, precisely because they do not have to embed the proof of their termination in their own running code.

There are ways around the BST, of course, and I am not saying otherwise.  For example, the BST merely guarantees the existence of a bad case, so one can always argue that such a case will never arise in practice.  Could be, but I did mention the GCD in T problem for a reason: there are natural problems that are difficult to express in a language such as T.  By fixing the possible termination arguments in advance, one is tempting fate, for there are many problems, such as the Collatz Conjecture, for which the termination proof of a very simple piece of code has been an open problem for decades, and has resisted at least some serious attempts on it.  One could argue that such a function is of no practical use.  I agree, but I point out the example not to say that it is useful, but to say that it is likely that its eventual termination proof will be quite nasty, and that this will have to be reflected in the program itself if you are limited to a T-like language (rendering it, once again, useless).  For another example, there is no inherent reason why termination need be assured by means similar to that used in T.  We got around this issue in NuPRL by separating the code from the proof, using a type theory based on a partial programming language, not a total one.  The proof of termination is still required for typing in the core theory (but not in the theory with “bar types” for embracing partiality).  But it’s not baked into the code itself, affecting its run-time; it is “off to the side”, large though it may be).

Updates: word smithing, fixed bad link, corrected gcd, removed erroneous parenthetical reference to Coq, fixed LaTeX problems.


An Unpleasant Interruption, Some Good News, and A Plea

March 8, 2014

It’s been a while since my last blog post (early last December, in fact), and I’ve even neglected to process comments during the same period.  Why the interruption?  Have I finally run out of things to complain about?  Not a chance!  Actually, what’s happened is that on December 18 I underwent a kidney transplant from a kind living donor who I scarcely even knew before the surgery occurred.  (If you are interested in the back story, you might like to read the newspaper article about it that appeared in the Pittsburgh Post-Gazette last Christmas.)  My condition, primary FSGS, is idiopathic, and has been worsening for about 20 years (an unusually long time before transplant is indicated).  Things finally became acute last year when I was reduced to approximately 10% kidney function, close to the lower bound for survival without renal replacement therapy.  I was deeply humbled by the generosity of numerous people who stepped forward to volunteer to donate an organ to me, some of whom are readers of this blog and are in any case well-known to all of you.  To them I am unable to adequately express my gratitude, but I can try to pay it forward over time.  The donor selection process is largely opaque to the donee (so as to ensure that the donor not being is coerced or bribed), but as it turned out Tony Balko, the fiancé of my “niece”, Marina Pfenning, daughter of my colleague Frank Pfenning, became my donor, and thereby saved my life.

I have spent the last couple of months recovering from the surgery itself, which involved a substantial incision, monitoring my progress and the health of the organ, and adjusting the immune suppressants to achieve a balance between avoiding rejection and inviting infection.  As a pay-it-forward gesture I volunteered to be a subject in a study of a new immune suppressant, ASKP1240, that is being developed specifically for kidney transplant patients.  All this means frequent visits to the transplant center and frequent blood draws to measure my kidney function and medication levels.  The recovery and monitoring has kept me operating at a reduced level, including neglecting my blog.

The good news is that Tony and I have fully recovered from surgery, and I am happy to say that I am enjoying an optimal outcome so far.  The transplanted organ began working immediately (this is not always the case), and within two days I had gotten back ten years of kidney function.  By now I am at completely normal blood levels, with no signs of kidney disease, and no signs of rejection or other complications.  Tony gave me a really good organ, and my body seems to be accepting it so far.  I’m told that the first six months are determinative, so I expect to have a pretty solid sense of things by the summer.

I would like to say that among the many things I’ve learned and experienced these last few months, one is an appreciation for the importance of organ donation.  Every year hundreds of people die from kidney disease for lack of a suitable organ.  If someone is limited to the national cadaverous donors list, it can take more than two years to find an acceptable organ, during which time people often die waiting.  Another complication is that someone may have a willing donor, perhaps a family member, with whom they are incompatible.  There are now several living donor exchange networks that arrange chains of organ swaps (as many as 55 simultaneously, I’m told!) so that everyone gets a compatible organ.  But to be part of such an exchange, you must have a living donor.

Living donation is a daunting prospect for many.  It does, after all, involve major surgery, and therefore presents a health risk to the donor.  On the other hand nature has  provided that we can survive perfectly well on one kidney, and a donation is literally the difference between life and death for the recipient.  The trade-off is, in objective terms, clearly in favor of donation, but the scarcity of organs makes clear that not everyone, subjectively, reaches the same conclusion.  As an organ recipient, allow me to plead with you to consider becoming an organ donor, at least upon your death, and perhaps even as a living donor for those cases, such as kidney donation, where it is feasible.  Should you donate, and find yourself in need of an organ later in life, you will receive top priority among all recipients for a donated organ.  The donation process is entirely cost-free to the donor in monetary terms, but pays off big-time in terms of one’s personal satisfaction at having saved someone’s life.