The quine-bernays combinatory calculus

Raja, N. ; Shyamasundar, R. K. (1995) The quine-bernays combinatory calculus International Journal of Foundations of Computer Science, 6 (4). pp. 417-430. ISSN 0129-0541

Full text not available from this repository.

Official URL:

Related URL:


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.

Item Type:Article
Source:Copyright of this article belongs to World Scientific Publishing Company.
Keywords:Combinatory Logic; Lambda-calculus; Functional Completeness; Variable-elimination Technique
ID Code:56598
Deposited On:24 Aug 2011 10:58
Last Modified:24 Aug 2011 10:58

Repository Staff Only: item control page