Functional completeness of the mixed λ-calculus and combinatory logic

Publication: Research - peer-reviewJournal article – Annual report year: 1990

View graph of relations

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
StatePublished - 1990
Download as:
Download as PDF
Select render style:
Download as HTML
Select render style:
Download as Word
Select render style:

ID: 3972936