# Is the SK2 calculus a complete basis, where K2 is the flipped K combinator?

Specifically, if I defined a new $$K_2$$ as $$K_2 = \lambda x. (\lambda y. y)$$ instead of $$K = \lambda x. (\lambda y. x)$$ would the $$\{S, K_2,I\}$$-calculus be a compete basis?

My guess is "no," just because I can't seem to be able to construct the regular K combinator from the $$S$$, $$I$$, and $$K_2$$ combinators, but I don't have an algorithm to follow, nor do I have good intuition about making things out of these combinators.

It seems like you can define $$K_2 = K I$$ with the regular $$\{S, K, (I)\}$$-calculus, but I couldn't really work backwards from that to get a derivation of $$K$$ in terms of $$K_2$$ and the rest.

My attempt at a proof that it was not functionally complete essentially attempted to exhaustively construct every function attainable from these combinators in order to show that you reach a dead end (a function you've seen before) no matter what combinators you use. I realize that this isn't necessarily going to be true of functionally incomplete sets of combinators (e.g. the $$K$$ combinator on its own will never dead end when applied to itself), but this was my best thought. I was always able to use the $$S$$ combinator to sneak out of what I thought was finally a dead end, so I'm no longer so sure of the feasibility of this approach.

I asked this question on StackOverflow but was encouraged to post it here. I received a few comments on that post, but I'm not sure I understood them right.

Bonus: if it isn't a complete basis, is the resulting language nonetheless Turing-complete?

• this is a nice puzzle. It seems that S and K' only allow you to generate terms whose head normal forms have up to three leading λs (i.e., terms that normalize to the form λx₁.λx₂.λx₃. xᵢ t₁ ... tₙ), so that might be another route to proving incompleteness, although it seems a bit tricky to formalize. You definitely never reach a "dead end", though: begin by defining I = λx.x = K2 K2, then by repeating the transformation t ↦ S t K2 you can express λx.x I ... I for any string of Is. Commented May 2, 2019 at 16:23
• ...And sorry, by "incompleteness", I mean incompleteness of SK' as a combinatory basis for the untyped lambda calculus. I also do not have a good intuition for whether or not it is Turing-complete (which would be implied by combinatory completeness, but not the other way). Commented May 2, 2019 at 16:40
• Cross-posted: stackoverflow.com/q/55148283/781723, cs.stackexchange.com/q/108741/755. Please do not post the same question on multiple sites. Each community should have an honest shot at answering without anybody's time being wasted.
– D.W.
Commented May 2, 2019 at 19:49
• My mistake @D.W., is there anything I can do to remedy this?
– cole
Commented May 2, 2019 at 19:53

Consider the terms of the $$S,K_2,I$$ calculus as trees (with binary nodes representing applications, and $$S, K_2$$ leaves representing the combinators.

For example, the term $$S(SS)K_2$$ would be represented by the tree

        @
/ \
/   \
@    K2
/ \
/   \
S     @
/ \
/   \
S     S


To each tree $$T$$ associate its rightmost leaf, the one you get by taking the right branch at each @. For example, the rightmost leaf of the tree above is $$K_2$$.

As can be seen from the ASCII art below, all reduction rules in the $$S, K_2, I$$ calculus preserve the rightmost leaf.

         @                           @
/ \                         / \
/   \                       /   \
@     g    [reduces to]     @     @
/ \                         / \   / \
/   \                       e   g f   g
@     f
/ \
/   \
S     e

      @
/ \
/   \
@     f    [reduces to]   f
/ \
/   \
K2    e


From there on, it's easy to see that if some term $$T$$ reduces to $$T'$$, then $$T$$ and $$T'$$ have the same rightmost leaf. Hence, there is no term $$T$$ in the $$S, K_2, I$$ calculus such that $$TK_2S$$ reduces to $$K_2$$. However, $$KK_2S$$ reduces to $$K_2$$, hence $$K$$ cannot be expressed in the $$S,K_2, I$$ calculus.

• Very nice argument! Commented May 2, 2019 at 23:00
• Very slick and clear argument. Thank you. Perhaps I will open a separate question to ask about Turing completeness.
– cole
Commented May 2, 2019 at 23:16
• I'm not sure I understood this answer. What would happen if we considered the combinators $S$, $K_2$, $I$ and $B$, where $Bxyz=x(yz)$? From what I understand, we would look at the rightmost leaf of $Bxyz$ and $x(yz)$ and conclude that this reduction rule preserves the rightmost leaf $z$. Therefore $K$ still cannot be expressed in the $S$, $K_2$, $I$, $B$ calculus. But then what about $S(BBB)(BK_2)$? Isn't that $K$? Commented May 8 at 3:12
• @2014MELO03: No, if you set $Bxyz=x(yz)$ then $S(BBB)(BK_2)$ does not give the $K$ combinator. As you noticed, $K$ is not expressible in the $S,K_2,B$ calculus by the same argument as above. I think you understood the answer, but perhaps made a mistake while reducing $S(BBB)(BK_2)xy$? Look for a step in that reduction where $y$ first disappears from the rightmost leaf position, that's where the error will be. Commented May 8 at 8:04
• @Z.A.K.: Because of $\eta$-reduction, $Kxy=x$ is equivalent to $Kxyz=xz$, this way $y$ is never the rightmost leaf. The reduction would be: $S(BBB)(BK_2)xyz=BBBx(BK_2x)yz=B(Bx)(BK_2x)yz=Bx(BK_2xy)z=x(BK_2xyz)=x(K_2(xy)z)=xz$. Both reduce to $xz$, so $S(BBB)(BK_2)xyz=Kxyz$ and therefore $S(BBB)(BK_2)=K$. Commented May 8 at 18:08

EDIT: As the comments point out, this is only a partial answer, since it applies only to the simply-typed $$S,K_2,I$$ calculus (or rather, it shows that there is no possible definition of K that does not contain an ill-typed subterm). If there's no objection, I won't delete it, since it presents a very productive proof technique for the typed setting.

Recall that our combinators have the following types (Curry-style, so $$A,B,C$$ are variable):

• $$K: A \rightarrow B \rightarrow A$$
• $$K_2: A \rightarrow B \rightarrow B$$
• $$S: (A \rightarrow B \rightarrow C) \rightarrow (A \rightarrow B) \rightarrow (A \rightarrow C)$$
• $$I: A \rightarrow A$$

By the Curry-Howard correspondence, if we can express $$K$$ in terms of $$I,S,K_2$$ then the Hilbert-style proof calculus with three logical axioms $$A \rightarrow B \rightarrow B, (A \rightarrow B \rightarrow C) \rightarrow (A \rightarrow B) \rightarrow (A \rightarrow C), A \rightarrow A$$ and one inference rule (from $$A$$ and $$A \rightarrow B$$ infer $$B$$) proves the formula $$A \rightarrow B \rightarrow A$$.

But we can give a three-valued (values t,f,u) semantics to the connective $$\rightarrow$$ such that the formulas $$A \rightarrow B \rightarrow B$$, $$(A \rightarrow B \rightarrow C) \rightarrow (A \rightarrow B) \rightarrow (A \rightarrow C)$$ and $$A \rightarrow A$$ get the value t for any interpretation.

A B | A -> B
t t | t
t f | f
f t | t
f f | t
t u | f
f u | t
u t | t
u f | f
u u | t


This semantics is clearly sound in the sense that every consequence of the axioms $$K_2, S, I$$ gets the value t under every interpretation (it is not complete, there are things that always get the value t but that we cannot actually prove). However, $$A \rightarrow B \rightarrow A$$ gets the value f under the interpretation that assigns u to $$A$$ and t to $$B$$, and is therefore not provable from the axioms corresponding to $$S, K_2, I$$.

• I like the approach, but could you clarify what rules you are taking as your sequent calculus? Commented May 1, 2019 at 12:00
• Can you sketch how to prove S in this restricted sequent calculus? It doesn’t seem to be possible with the rules I guessed you might mean. Commented May 1, 2019 at 13:07
• @robin-houston: please see my edit (I've also added a different, semantic argument with the same conclusion). Commented May 1, 2019 at 16:31
• I agree with Charles Stewart (over here: twitter.com/txtpf/status/1123962607306706944) that it's not clear how to pass from uninhabitation in simply-typed lambda calculus to inexpressibility using combinators. There might be an argument specific for K, but the initial step "...then one could also do the same thing in the simply-typed λ-calculus" doesn't hold in general (Charles mentioned the counterexample of the Y combinator). Do you see of making this argument rigorous? Commented May 2, 2019 at 16:08
• @NoamZeilberger I also agree. This argument unfortunately seems insufficient: in the untyped calculus you might be able to obtain $K$ using a construction which involves (sub)terms which have no type. One should prove that if you can achieve that, you can also do the same using only typed terms, but that looks hard to prove to me.
– chi
Commented May 2, 2019 at 17:44