For decades my colleague, Guy Blelloch, and I have promoted a grand synthesis of the two “theories” of computer science, combinatorial theory and logical theory. It is only a small exaggeration to say that these two schools of thought work in isolation. The combinatorial theorists concern themselves with *efficiency*, based on hypothetical translations of high-level algorithms to low-level machines, and have no useful theory of *composition*, the most important tool for developing large software systems. Logical theorists concern themselves with *composition*, emphasizing the analysis of the properties of components of systems and how those components are combined; the heart of logic is a theory of composition (entailment). But relatively scant attention is paid to efficiency, and, to a distressingly large extent, the situation is worsening, and not improving.

Guy and I have argued, through our separate and joint work, for the applicability of PL ideas to algorithms design, leading. for example, to the concept of adaptive programming that Umut Acar has pursued aggressively over the last dozen years. And we have argued for the importance of cost analysis, for various measures of cost, at the level of the code that one actually writes, and not how it is compiled. Last spring, prompted by discussions with Anindya Banerjee at NSF in the winter of 2014, I decided to write a position paper on the topic, outlining the scientific opportunities and challenges that would arise in an attempt to unify the two, disparate theories of computing. I circulated the first draft privately in May, and revised it in July to prepare for a conference call among algorithms and PL researchers (sponsored by NSF) to find common ground and isolate key technical challenges to achieving its goals.

There are serious obstacles to be overcome if a grand synthesis of the “two theories” is to be achieved. The first step is to get the right people together to discuss the issues and to formulate a unified vision of what are the core problems, and what are promising directions for short- and long-term research. The position paper is not a proposal for funding, but is rather a proposal for a meeting designed to bring together two largely (but not entirely) disparate communities. In summer of 2014 NSF hosted a three-hour long conference call among a number of researchers in both areas with a view towards hosting a workshop proposal in the near future. Please keep an eye out for future developments.

I am grateful to Anindya Banerjee at NSF for initiating the discussion last winter that led to the paper and discussion, and I am grateful to Swarat Chaudhuri for his helpful comments on the proposal.

[*Update:* word smithing, corrections, updating, removed discussion of cost models for fuller treatment later, fixed incoherence after revision.]

All links to your position paper are broken:

https://www.cs.cmu.edu/~rwh/papers.htm#secp

The final “l” seems to be missing:

https://www.cs.cmu.edu/~rwh/papers.html#secp

oops. fixed.

Given that the “subject of logic” could be taken to mean Mathematical logic which technically speaking actually includes complexity theory by way of computability theory (a complexity measure is a function on codes for turing machines that satisfies …. ) the claim that the entire subject pays scant attention to efficiency is a bit strange.

For clarification were you referring to mathematical logic here and implicitly the pure study of computability (is blah computable … degree theory etc.. ) or of the pure study of programming language semantics?

i needed terminology to make my points. i used “logic and semantics” to mean euro- theory, and “combinatorics” to refer to ametican- theory, if that’s any help.

At first I was worried that the intermediate step of compilation When considering programming languages and abstracta we don’t want to, the way algorithm researchers must do, handcuff ourselves to some particular compilation strategy. We don’t want to know if, compiled poorly, programs written in a logical programming paradigm had worse complexity than those written in a declarative one (i.e. natural examples of a solution to some problem in the different languages). It’s easy to compile programs poorly.

What we want to know is whether, compiled intelligently, a programming language makes it easy to write (or hard not to) code with good time/space complexity. To be most useful we ‘d really love no results, e.g., this programming language doesn’t allow for efficient (or just “natural” programs in that language don’t) solutions. Of course given a fixed piece of code there is always a compiler that produces the same behavior with optimal (technically as optimal as you want… speedup theorem) results. Alright, we’ve got to consider infinitary collections of programs and the strongest result there would be an impossibility result (for any fixed compilation strategy there are programs in language 1 whose big O time complexity is worse than that of the optimal solution).

But if P == NP my sense is (and I could be wrong as I haven’t actually worked this out) that there is a compiler that will find something very close to optimal as a result. In particular, a purely sequential declarative approach would produce code that took equally good advantage of concurrency as that written using nice semantics for parallelism (yes they aren’t the same but we care about parallel semantics because we want algorithms that perform well concurrently). Since we think P != NP our best compilers may be unable to auto-parallelize efficiently but the sword of damocles will always threaten.

—–

However, on second thought this is demanding to much. Even without strong lower bound results on effective compilation it would be quite interesting. Even just upper bound results would be far from shabby.

Moreover, by pushing the PL community in the direction of a certain more mathematical (or maybe just more of the math I like) style and bringing the compilation step itself into the academic literature in a more formal fashion such a theory would help inform compilation. Such a theory could help us understand when a desirable programming practice resisted as inefficient is a real concern or a problem that can be swept under the rug with a smart compiler.

Oops, and doing computability theory not CS I probably switched parallel and concurrent. It should be clear enough what I meant by each.

a cost semantics is the interface between the programmer and the compiler writer. the programmer expects those costs to be met; the compiler writer is obliged to meet them. part of language design is choosing a usable and realistic cost semantics. this is never done today. no one ever has a clue about the time or space complexity of a haskell program. this situation is absurd.

Ahh I think I understand your program a bit better now.

Coming from a very theoretical background I missed the simple practical value of “What kind of complexity will the resulting code have GIVEN the current compiler”. It’s very useful (and interesting) to ask about the complexity of code compiled by existing compilers whether or not you can answer the question of whether some future compiler can avoid the slowdown.

There are interesting questions also about what a compiler could do given various assumptions about how hard various problems are. I suspect, however, these would be less useful for languages used in practice but who knows.

This is very exciting!

As someone who has one foot in the combinatorial world and one foot in the compositional world, and is just starting out academically, I find the current offerings of theory in our field to be inadequate. In some places the “theory A”-ists and the “theory B”-ists, although in the same department, are in different buildings altogether, and are rarely in direct contact. (I’m at Cornell … where fortunately there does seem to be a bit of contact. But it’s limited, as it is everywhere in CS it seems.)

I want to see more “crunchy math” in type theory! Crunchy types, if you will.

As it happens I am at Cornell for the opening of the new, unified, building!

Nice to meet you. :-)

As a (semi) sidenote: how can one capture the notion of “constant space” or “logarithmic space” in the lambda calculus? For TMs it’s relatively straightforward: have a read only tape for the input, a write only tape for the output, and use a “rw” tape to model the intermediate memory requirements. It’s a bit less clear how to do it with rewriting. Do you have a story for this?

The critical point is that the lambda calculus

is not a machine model. It’s an algebra of machines, and the fact that it canalsobe viewed as a machine model (i.e., has a reasonable cost semantics) is an extremely powerfultheorem, because it means that you can freely switch back and forth between algebraic and machine-oriented views. (See, for instance, Beniamino Accattoli and Ugo Dal Lago’s recent paperOn the Invariance of the Unitary Cost Model for Head Reduction.)The untyped lambda calculus gives (basically) the algebra of computable machines. With the appropriate type discipline, you can cut things down to talk about smaller complexity classes.

For logspace in particular, what makes it tricky is that logspace is closed under composition, but in a subtle way — to implement the composition of two logspace algorithms, you have to dovetail the two algorithms, so that the first algorithm produces output in sync with the second algorithm’s demand for inputs. But at a high level, this is what the geometry of interaction does, and you can see Ulrich Schoepp and Ugo dal Lago’s

Functional Programming in Sublinear Spacefor how to give a type system for logspace programs.IMO, this really illustrates the power of being able to view the LC in two ways. One intuition behind GoI is that you have a network with token passing along channels, and this doesn’t look like terms at all! But because the lambda calculus is an algebraic theory of machines, we can compositionally interpret terms into dataflow networks, and lift the cost semantics of the first-order network to the higher-order language.

Hi Bob,

As someone who works a bit in both fields, I am really glad that there is increasing interest in bridging these two fields, or at least improving lines of communication. It’s really a shame that the two most of theoretical and rigorous fields of computer science have diverged to this point.

I feel the same way.

Bob: I am a bit surprised that you interpreted my questions during my visit to CMU as “opposition” to your approach. The more appropriate word is “curiosity”. I was curious about how you assign costs to beta-reductions, and I was persuaded by the answers you gave in person and over email. At any rate, these were technical questions, not a challenge to the idea of synthesizing Theory A and Theory B, about which I have/had nothing but respect.

I think one immediately important question is which models can serve as versatile semantics for the logical crowd while also being equipped with a powerful enough combinatorial theory for the combinatoric crowd, and furthermore also allow a natural translation between the two points of view. The geometry of interaction and games in general come to mind as promising forerunners that have already yielded some fruit.

This is really encouraging, Bob. Something that has really troubled me during my nascent academic career has been the (perceived) lack of any actual coordination/organization of large-scale research agendas. Why is our field so averse to grand narratives and such?

Just to point out that Bounded Linear Logic made significant strides in bridging the gap between semantics and computability via type theory. There is a small but very energetic community of people working on type-theoretic approaches to resource control. We had a lovely workshop last year about it. I am posting the link because it includes an essential reading list.

http://www.cs.bham.ac.uk/~drg/bll.html

thanks! good point.

Provocative post. In trying to envision how this might proceed, one model I think about is the approach that PL has taken to other fields. Work with domain experts, discover the problems they face, and then direct theoretical and practical work to make their lives better. In this case, try to discover the problems that Theory A researchers wrestle with every day, and look at where their tools may be less adequate than they realized (in this case, their tools being more mathematical/abstract logical systems than e.g. python or R), and then try to develop technology that solves those types of problems (again, more formal perhaps than in other domains).

I would add a few other points of overlap to those mentioned in your position paper. First, the lovely “lightweight semiformal” complexity analysis in agda paper: [http://www.cse.chalmers.se/~nad/publications/danielsson-popl2008.html] (Steffen Jost seems to have done some related work as well). Second, the principled program transformation/calculation tradition from Bird onwards. Shing-Cheng Mu’s work in this tradition such as [http://www.iis.sinica.edu.tw/~scm/2012/programming-from-galois-connections-2/] points to how we can get to very formal notions of “most efficient” that synthesize directly from specifications. Certainly we aren’t going to start doing that for “hard” problems anytime soon, but it seems that providing algorithmacists a better framework for producing guaranteed-correct transformations of complex algorithms may itself be very well received. Finally, there is Sands’ very nifty work on improvement theory [http://www.cse.chalmers.se/~dave/papers/hoots97.pdf] — this year at ICFP, Hackett and Hutton had a paper using it to demonstrate a result in the _efficiency correctness_ of the worker/wrapper transform.

Thanks for all the citations! I knew of a couple of these, but not the most recent you mention. And thanks for the suggestions.

“Logical theorists concern themselves with composition, emphasizing the analysis of the properties of components of systems and how those components may be combined; the entire subject of logic is a theory of composition (entailment). But relatively scant attention is paid to efficiency…”

Bob – aren’t you being all too glib here? What about the huge amount of work done on descriptive complexity theory? – let alone the even larger amount of work done on the complexity of logical inference. Perhaps there is more to logic than is dreamt of in your philosophy of programming languages…

That’s a very valid point.