Functional completeness of the mixed λ-calculus and combinatory logic
Publication: Research - peer-review › Journal article – Annual report year: 1990
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 language | English |
|---|---|
| Journal | Theoretical Computer Science |
| Publication date | 1990 |
| Volume | 70 |
| Journal number | 1 |
| Pages | 99-126 |
| ISSN | 0304-3975 |
| State | Published |
ID: 3972936