Functional completeness of the mixed \(\lambda\)-calculus and combinatory logic (Q750415)

The authors present a two-level version of combinatory logic and lambda calculus for distinguishing between early and late binding times, i.e. compile-time and run-time computations. In this paper, which is an extension of a previous one by the same authors, the two-level lambda calculus is enriched by a new combinator, \(\Psi\), which makes the calculus complete, in the sense that every \(\lambda\)-expression can be translated into an equivalent combinator expression.