Abstraction problems in combinatory logic: A compositive approach (Q1262300)

This paper analyses the problem of translating \(\lambda\)-calculus terms into combinatory logic terms. Abtraction algorithms constitute the central issue of such translation since they allow removing bound variables from \(\lambda\)-terms by means of introducing some constants (combinators) belonging to a given basis. Three versions of a new abstraction algorithm are presented, using different abstraction techniques (one-sweep, multi-sweep, supercombinators). They derive from the definition of abstraction given by Curry in 1930 and have some interesting features: (a) they employ a potentially infinite basis of combinators, each of which depends on at most two parameters; (b) they introduce a number of basic combinators which is proportional to the size of the expression to be abstracted and invariant for the considered abstraction techniques; (c) they give the result in the form \(RIM_ 1...M_ n\), where R is a regular combinator expressed as a composition of basic combinators, I is the identity combinator and \(M_ 1,...,M_ n\) are constant terms appearing in the expression subject to the abstraction process. The algorithms are compared with existing ones and it is shown that no other algorithm present in the literature shares the cited features. The compactness of the resulting code and its compositive form, and the direct implementability of the basic combinators make the presented algorithms suitable for application in the implementation of functional programming languages.