Home

Call-by-value Termination in the Untyped Lambda-calculus

From Arxiv:

A fully-automated algorithm is developed able to show that evaluation of a given untyped lambda-expression will terminate under CBV (call-by-value). The ``size-change principle'' from first-order programs is extended to arbitrary untyped lambda-expressions in two steps. The first step suffices to show CBV termination of a single, stand-alone lambda-expression. The second suffices to show CBV termination of any member of a regular set of lambda-expressions, defined by a tree grammar. (A simple example is a minimum function, when applied to arbitrary Church numerals.) The algorithm is sound and proven so in this paper. The Halting Problem's undecidability implies that any sound algorithm is necessarily incomplete: some lambda-expressions may in fact terminate under CBV evaluation, but not be recognised as terminating.
The intensional power of the termination algorithm is reasonably high. It certifies as terminating many interesting and useful general recursive algorithms including programs with mutual recursion and parameter exchanges, and Colson's ``minimum'' algorithm. Further, our type-free approach allows use of the Y combinator, and so can identify as terminating a substantial subset of PCF.

To renew the discussion on Total Functional Programming, this paper is an alternative to Termination Checking with Types.

By Daniel Yokomizo at 2008-01-08 05:29 | Lambda Calculus | Semantics | other blogs | 8731 reads

Comment viewing options

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

Authors

The authors are Neil Jones and Nina Bohr. The latter name is not known to me, but the former will not need any introduction to the LtU hardcore.

By Charles Stewart at Tue, 2008-01-08 14:28 | login or register to post comments

Nina Bohr

Nina Bohr is one of Lars Birkedal's students -- I think she recently finished her PhD. The two also wrote a very interesting paper on proving contextual equivalences for a language with references and higher-order store.

By neelk at Tue, 2008-01-08 23:22 | login or register to post comments

Typo ?

At some point, I got quite puzzled by the definitions in the Example 4.1(end of page 11): these functions didn't appeared to terminate in most cases to me (and ghci seemed to confirm my intuition), whereas it is stated at the end of the next paragraph (Termination reasoning) that a call of any program function with any data will terminate, a claim that seemed inexact to me (f 1 2, for example, being non-terminating as far as I can tell).

The only solution I was able to come up with was to replace the if w = 0, in the beginning of the definition of g, by if v = 0. With this modification, the two functions now terminate in every case (I think), and it seems moreover coherent with what is stated at the end of the section (page 12):

G satisfies the size-change condition, since every infinite multipath has either a thread
that decreases u infinitely, or a thread that decreases v infinitely.

So, is this a typo or am I missing something ?

Anyway, the paper is pretty nice. The algorithm appears to be able to check primitive recursive functions, so I'm asking myself if it would also be able to check Walther recursive ones, since the combination of Walter recursion + mutual recursion + higher-order functions make a pretty expressive subset of lambda-calculus, one I would be happy to learn that it is statically checkable for termination. Gotta look at that :)

By renaud at Tue, 2008-01-08 20:33 | login or register to post comments