The quine-bernays combinatory calculus

Abstract

We develop a theory for constructing Combinatory Versions of λ-calculi. Our theory is based on a method, used by Quine and Bernays, for the general elimination of variables in formulations of first-order logic. Our Combinatory Calculus presents a significant departure from those propounded by Schonfinkel and Curry. A non-trivial extension of Quine's technique is developed, to go beyond the realm of first-order quantification theory, and cover the entire λ-calculus. The system consists of five Combinators, powerful enough to represent λ-abstractions over arbitrary terms. The Combinatory Calculus is shown to have the property of functional completeness. Algorithmic translations from the λ-calculus to the Combinatory Version, and vice-versa, are provided. The approach has the distinct advantage of being able to encode combinatory formulations of process algebras.