Narrow Results

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 Schönfinkel 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.

Despite extensive theoretical work carried out on coordination during the last three decades, much research is still devoted to proving the merits of one model over another. In our article, we will show how the coordination process in French (with using the conjunction et (and)) can be explained through Applicative and Combinatory Categorial Grammar (ACCG).

Knot and link diagrams are used to represent nonstandard sets, and to represent the formalism of combinatory logic (lambda calculus). These diagrammatics create a two-way street between the topology of knots and links in three dimensional space and key considerations in the foundations of mathematics.

We present in this article an application of automated theorem proving to a study of a theorem in combinatory logic. The theorem states: the strong fixed point property is satisfied in a system that contains the B and W fR combinators. The theorem can be stated in terms of Smullyan's forests of birds: a sage exists in a forest that contains a bluebird and a warbler. Proofs of the theorem construct sages from B and W. Prior to the study, one sage, discovered by Statman, was known to exist. During the study, with much assistance from two automated theorem-proving programs, four new sages were discovered. The study was conducted from a syntactic point of view because the authors know very little about combinatory logic. The uses of the automated theorem-proving programs are described in detail.

Barendregt defines combinatory logic as an equational system satisfying the combinators S and K with ((Sx)y)z = (xz)(yz) and (Kx)y = x, the set consisting of S and K provides a basis for all of combinatory logic. Rather than studying all of the logic, logicians often focus on fragments of the logic, subsets whose basis is obtained by replacing S or K or both by other combinators. In this article, we present a powerful new strategy, called the kernel strategy, for studying fragments in the context of questions concerned with fixed point properties. Interest in such properties rests in part with their relation to normal forms and paradoxes. We show how the kernel strategy was used to answer a number of open questions, offering abundant evidence that the availability of the kernel strategy marks a singular advance for automated reasoning. In all of our experiments with this strategy applied by an automated reasoning program, the rate of success has been impressively high and the CPU time to obtain the desired information startlingly small. For each fragment we study, we use the kernel strategy to attempt to determine whether the strong or the weak fixed point property holds. Where A is a given fragment with basis B, the strong fixed point property holds for A if and only if there exists a combinator y such that, for all combinators x, yx = x(yx), where y is expressed purely in terms of elements of B. The weak fixed point property holds for A if and only if for all combinators x there exists a combinator y such that y = xy, where y is expressed purely in terms of the elements of B and the combinator x. Because the use of the kernel strategy is so effective in addressing questions focusing on either fixed point property, its formulation marks an important advance for combinatory logic. Perhaps of especial interest to logicians is an infinite class of infinite sets of tightly coupled fixed point combinators (presented here), whose unexpected discovery resulted directly from the application of the strategy by an automated reasoning program. We also offer various open questions for possible research and focus on an automated reasoning program and input files that may prove useful for such research.