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. 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). 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.
May 2, 2019 at 19:49
• My mistake @D.W., is there anything I can do to remedy this?
– cole
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! 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
May 2, 2019 at 23:16

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? 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. May 1, 2019 at 13:07
• @robin-houston: please see my edit (I've also added a different, semantic argument with the same conclusion). 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? 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
May 2, 2019 at 17:44