patternModerate
Is the SK2 calculus a complete basis, where K2 is the flipped K combinator?
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?
$$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
To each tree $T$ associate its rightmost leaf, the one you get by taking the right branch at each
As can be seen from the ASCII art below, all reduction rules in the $S, K_2, I$ calculus preserve the rightmost leaf.
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.
For example, the term $S(SS)K_2$ would be represented by the tree
@
/ \
/ \
@ K2
/ \
/ \
S @
/ \
/ \
S STo 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 eFrom 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 eContext
StackExchange Computer Science Q#108741, answer score: 18
Revisions (0)
No revisions yet.