Functional completeness of the mixed λ-calculus and combinatory logic

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