| |
VOLUME 4, ISSUE 1, PAPER 3
|
Call-by-value Termination in the Untyped λ-calculus
|
©Neil D. Jones, University of Copenhagen
©Nina Bohr, IT University of Copenhagen
|
Abstract
A fully-automated algorithm is developed able to show that evaluation
of a given untyped λ-expression will terminate under CBV
(call-by-value). The ``size-change principle'' from first-order
programs is extended to arbitrary untyped λ-expressions in two
steps. The first step suffices to show CBV termination of a single,
stand-alone λ-expression. The second suffices to show CBV
termination of any member of a regular set of λ-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
λ-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.
|
Publication date: March 17, 2008
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-4(1:3)2008
Hit Counts: 2467 |
 Creative Commons | |
