Combinatory Logic

Barendregt [Barendregt81] defines combinatory logic as an equational system satisfying the combinators S and K with (( Sx)y)z = (xz)(yz) and (Kx)y = x. Rather than studying this logic in its entirety, one finds challenging test problems by replacing one or both of S and K by one or more combinators and focusing on questions concerning the possible presence of the strong fixed point property. The set consisting of the combinators under study is called a basis, and the set of combinators generated by a basis is called a fragment. 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 problems we offer focus on various subsets of the following combinators.

EQ(a(a(a(B,x),y),z),a(x,a(y,z))).	EQ(a(M,x),a(x,x)).
EQ(a(a(a(C,x),y),z),a(a(x,z),y)).	EQ(a(a(a(N,x),y),z),a(a(a(x,z),y),z)).
EQ(a(a(a(H,x),y),z),a(a(a(x,y),z),y)).	EQ(a(a(a(S,x),y),z),a(a(x,z),a(y,z))).
EQ(a(I,x),x).	EQ(a(a(W,x),y),a(a(x,y),y)).

For each of the following problems, the object is to use the combinators specified in the problem and no others and prove that the strong fixed point property holds by finding an appropriate object.

Problem CL1, simple. The set consists of B, M, and W.

Problem CL2, hard. The set consists of B and W.

Problem CL3, hard. The set consists of B and N.

Problem CL4, hard. The set consists of B and H.

Problem CL5, hard. The set consists of B, C, I, and S.

To complement the preceding test problems and for those who enjoy the study of open questions, we offer two open questions. Does the set consisting of B and M alone permit the construction of an object that proves that the strong fixed point property holds? Does the set consisting of B and S alone permit the construction of an object that proves that the strong fixed point property holds?