Home » forums » LtU Forum

Continuation calculus

Continuation calculus ("CC") is an alternative to lambda calculus, where the order of evaluation is determined by programs themselves. CC is a constrained term rewriting system, designed such that continuations are no unusual terms. This makes it natural to model programs with nonlocal control flow, as is the case with exceptions and call-by-name functions. The resulting system has very simple operational semantics.

Because no real pattern matching is possible in CC, we can only examine data through its reduction behavior. This in turn allows us to define values that are compatible to natural numbers or lists, but whose deconstruction requires computation. Such values are similar to call-by-name function applications.

For an introduction, look at the presentation. Details can be found in the paper. You may also experiment with the online evaluator, which has some example programs.

In future work, I will describe a scheme to translate functional programs to continuation calculus. I also plan to describe an applicable type system, but the details have yet to be worked out.

By bgeron at 2013-06-04 13:22 | LtU Forum | previous forum topic | next forum topic | other blogs | 4892 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Neat

I am becoming too old to understand all this stuff, but looks like very promising work. A minor point: I missed the proof that one can translate arbitrary cbn and cbv lambda terms to the cc term rewrite system.

And I wonder about performance of this scheme when used in a simple functional language compiler.

I don't expect you'll find that well-typed terms always termninate since cbv lc doesn't have that property. If I remember well, I might be mistaken. I don't find it an interesting property anyway.

Then again, too long ago for me to really understand what's going on. Looks nice, my old university just went up a notch.

By marco at Wed, 2013-06-05 00:55 | login or register to post comments

Thanks

There was not enough room to include everything in the paper, but I'm working on a translation scheme right now. We have a toy compiler for a call-by-value language to CC; the language includes lambda and function application, so CC is certainly expressive enough.

We can convert lambda calculus terms to CC in three steps:

  1. CPS transformation
  2. Supercombinator transformation
  3. Make a rule for each supercombinator. In the lambda term, replace supercombinators by the names of the corresponding rule, and replace application by dot.

I'm working on a more direct translation from ML/Haskell to CC, because going via lambda calculus is a bit of a detour.

Regarding performance: A simple compiler could generate code for each rule, and use an indirect jump after each rule's code. I think the CPU's branch predictor will be able to correctly predict a lot of those jumps. Furthermore, rules of the form "A.x1...xk -> B.t1...tn" compile to a statically predictable jump. A third-party optimizer might then inline the jump at compile time, as a starting point for more optimizations; I believe that such administrative rules will thus be quite cheap.

By bgeron at Wed, 2013-06-05 13:48 | login or register to post comments

link dead

Is there an alternate link for the paper -- I get a dropbox error trying to access it.

EDIT: never mind, it's up again. :)

By jimdesu at Wed, 2013-06-05 23:00 | login or register to post comments