Three In The Room
A puzzle and a conference
Zohar Manna is an expert on the mathematical concepts behind all types of programming. For example, his 1974 book the Mathematical Theory of Computation was one of the first on the foundations of computer programming. He wrote textbooks with the late Amir Pnueli on temporal logic for software systems. As remarked by Heiko Krumm in some brief notes on temporal logic, there is a contrast between analyzing the internal logic of pre- and post-conditions as each statement in a program is executed, and analyzing sequences of events as a system interacts with its environment.
Today I want to talk about an encounter with Zohar years ago, and how it relates to a puzzle that I love.
Zohar did one of the coolest PhD theses ever. It was on schema theory, which we have talked about before here. He was advised by both Robert Floyd and Alan Perlis in 1968—two Turing Award winners. The thesis Termination of Algorithms was short, brilliant, a gem. I recall when I started as a graduate student reading it and thinking this was beautiful. His own abstract is:
The thesis contains two parts which are self-contained units. In Part 1 we present several results on the relation between the problem of termination and equivalence of programs and abstract programs, and the first order predicate calculus. Part 2 is concerned with the relation between the termination of interpreted graphs, and properties of well-ordered sets and graph theory.
I will explain the puzzle in a moment, but first let me describe the encounter I had with Zohar. At a STOC, long ago, I saw him and started to explain my result: the solution to the puzzle. After hearing it he said that he liked the solution and then added that he once had worked on this problem. I said that I thought I knew all his work and was surprised to hear that. He smiled and seemed a bit reluctant to explain. Eventually he explained all.
It turned out that he and Steven Ness had a paper On the termination of Markov algorithms at the 1970 Hawaiian International Conference on System Science, held in Honolulu. Zohar explained the conference was not the “best,” but was held every year in the Hawaiian Islands. In January. Where it is warm. And sunny. It sounded like a great conference to me.
I soon went to a couple of these conferences. I stopped going after they accepted one of my papers, then rejected it—this is a long story that I will recount another time. The “accepted-rejected” paper finally did appear in an IEEE journal.
Zohar explained that he went to the conference for the same obvious reasons. He also explained to me the “three-person rule.” The Hawaiian conference was highly parallel and covered many areas of research. Zohar said that you were always guaranteed to have at least three people in the room for your talk: There was the speaker, the session chair, and the next speaker. Hence the three-person rule.
The issue is the distributive law:
Consider any expression that has only variables and the two operations plus () and times (. Suppose one applies the distributive law to the expression, in any order. One stops when there are no further possible applications. The question, the puzzle, was: Does the distributive law always stop? Of course it does. Or does it? The puzzle is to prove that it actually does stop.
I raised this recently as my favorite result, with a smile, during my Knuth Prize lecture at FOCS. I said I had a nice solution and would be glad either to give it or let the audience think about it. They seem to want to think about it, so I gave no solution.
My lecture had been right before dinner, and the next day I spoke to some people about whether they’d thought about it. A few said they had some idea of how to proceed, but no one seemed to have a proof. The reason the problem is a bit challenging is that the rule increases the size of the expression: two copies of now appear instead of one. This means that any local measure of structure may fail.
Indeed Zohar’s proof uses a well ordering argument that is not too hard, but is perhaps a bit hard to find. Check out his paper with Ness.
The first thing I noticed immediately when I heard the problem—see here for the context—was this: The distributive law preserves the value of the expression. We apply it because it expands the expression but it does not change the value of the expression. A rule like
does not preserve value. So who cares whether it halts or not?
But the distributive law preserves the value. So here is a proof based on that observation. Notice the following two things:
- The value is the same as the rule is applied.
- The size of the expression grows as the rule is applied.
The trick is to replace all the variables by . The value stays the same, but it is easy to argue that if the rule never stops then eventually the value of the expression would increase without bound. This is a contradiction.
Are there other termination problems that can be attacked in this way?