HiveBrain v1.2.0
Get Started
← Back to all entries
patternModerate

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

Submitted by: @import:stackexchange-cs··
0
Viewed 0 times
thebasiscalculuscombinatorwheresk2flippedcomplete

Problem

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?

Solution

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.

Code Snippets

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

Context

StackExchange Computer Science Q#108741, answer score: 18

Revisions (0)

No revisions yet.