×

Asymptotically almost all \(\lambda \)-terms are strongly normalizing. (English) Zbl 1278.03034

This interesting paper looks at a completely new aspect of lambda calculus and combinatory logic, and so of functional programming languages, namely the likelihood of random lambda terms or combinators being in a particular form or being subterms of other random terms or combinators.
The main results are: Asymptotically, almost all lambda terms are strongly normalising and an arbitrary fixed closed lambda term almost never appears in a random lambda term. There are, of course, mappings from lambda terms to combinatory terms and vice versa, so it is surprising that the authors were able to show that almost all combinatory terms are not strongly normalising and that any fixed combinatory term almost always appears in a random combinatory term! As part of this, several results on the structural form of a random lambda term are derived, including upper and lower bounds on the number of lambda terms of length \(n\).

MSC:

03B40 Combinatory logic and lambda calculus
68N18 Functional programming and lambda calculus

Software:

QuickCheck
PDFBibTeX XMLCite
Full Text: DOI