Functional completeness of the mixed λ-calculus and combinatory logic

Hanne Riis Nielson, Flemming Nielson

    Research output: Contribution to journalJournal articleResearchpeer-review


    Functional completeness of the combinatory logic means that every lambda-expression may be translated into an equivalent combinator expression and this is the theoretical basis for the implementation of functional languages on combinator-based abstract machines. To obtain efficient implementations it is important to distinguish between early and late binding times, i.e. to distinguish between compile-time and run-time computations. The authors therefore introduce a two-level version of the lambda-calculus where this distinction is made in an explicit way. Turning to the combinatory logic they generate combinator-code for the run-time computations. The two-level version of the combinatory logic therefore is a mixed lambda-calculus and combinatory logic. They extend the mixed lambda-calculus and combinatory logic with a new combinator, Psi, and show that this suffices for the mixed lambda-calculus and combinatory logic to be functionally complete. However, the new combinator may not always be implementable and they therefore discuss conditions under which it can be dispensed with
    Original languageEnglish
    JournalTheoretical Computer Science
    Issue number1
    Pages (from-to)99-126
    Publication statusPublished - 1990


    Dive into the research topics of 'Functional completeness of the mixed λ-calculus and combinatory logic'. Together they form a unique fingerprint.

    Cite this