We all know how to SKI, but can you BCKW?

Question

Background

Lambda calculus is a model of computation using lambda terms.

• A variable \$x\$ is a lambda term.
• If \$E\$ is a lambda term, the lambda abstraction \$\lambda x. E\$ is a lambda term.
• If \$E_1, E_2\$ are lambda terms, the lambda application \$E_1 E_2\$ is a lambda term.

The rule of computation is called \$\beta\$-reduction: \$(\lambda x. E_1) E_2\$ is reduced to \$E_1\$ in which every occurrence of \$x\$ is replaced with \$E_2\$. For example, \$(\lambda x. x x)(\lambda y. y)\$ is reduced to \$(\lambda y. y)(\lambda y. y)\$, then to \$\lambda y. y\$.

Combinatory logic operates on a similar premise, but instead of variables and lambda abstraction, it uses a fixed set of combinators. Each combinator has a fixed arity, and it is \$\beta\$-reduced only when it gets enough number of arguments applied to it.

For example, \$S\$ and \$K\$ have following reduction rules:

$$ \begin{align} S x y z &\mapsto x z (y z) \\ K x y &\mapsto x \end{align} $$

\$S\$ has an arity of 3, so \$SKK\$ is not reducible. But if you apply one more argument to it, it reduces to \$SKKx \mapsto Kx(Kx) \mapsto x\$, which shows that \$SKK\$ is extensionally equal to the identity function \$\lambda x. x\$ in lambda calculus.

SKI combinator calculus is a well-known complete combinatory logic system, i.e. a system where any arbitrary lambda calculus term can be represented. This section on Wikipedia shows how to transform any given lambda term into a SKI expression.

BCKW system is a lesser known complete system, discovered by Haskell Curry in 1930. It uses four combinators defined as follows:

$$ \begin{align} B x y z &\mapsto x (y z) \\ C x y z &\mapsto x z y \\ K x y &\mapsto x \\ W x y &\mapsto x y y \end{align} $$

In Haskell terms, \$B\$ equals (.), \$C\$ equals flip, and \$K\$ equals const. Haskell doesn't have a built-in for \$W\$, but it is equal to (<*>id).

Challenge

Given a lambda term, convert it to an equivalent term in BCKW system.

The I/O format is flexible. The lambda term and BCKW term can be represented as a string notation (fully parenthesized or using prefix notation) or a (pre-parsed) nested structure. It is also allowed to use four distinct values (numbers, chars, strings) in place of BCKW combinators. The lambda term can also use de Bruijn indexes or other directly equivalent representations.

Standard code-golf rules apply. The shortest code in bytes wins.

Examples

There are infinitely many different correct outputs for every input, so these are merely examples of possible conversions.

\x. x
=>  W K  or  B C C
\x. x x
=>  W (W K)
\x y z. x (y z)
=>  B
\x y z. z x y
=>  B C (C (W K))
\f g x y. f (g x) (g y)
=>  B W (B (B C) (B (B (B B)) B))
\x y z. y (y y) y
=>  K (W (W (W (B (B (B (B K))) B))))
\f x. f (f (f x))
=>  W (W (C (B B (B B B)) B))

Answer 1

Haskell, 133 bytes

data T=T:@T|L T|V Int|B|C|K|W
l(x:@y)=W:@(B:@(C:@l x):@l y)
l(V 0)=W:@K
l(V n)=K:@V(n-1)
l x=K:@x
f(L x)=l$f x
f(x:@y)=f x:@f y
f x=x

Try it online!

Accepts De Bruijn–indexed lambda terms with \$λ\$ written as L, application written as :@, and variables written V 0, V 1, … from innermost to outermost.

This uses the standard unoptimized \$SKI\$ abstraction elimination algorithm, with \$Sxy\$ and \$I\$ replaced by \$W(B(Cx)y)\$ and \$WK\$. As such, it’s very inefficient in terms of output size.

Answer 2

Python 3, 451 bytes

I='W','K'
F=lambda v,e:v==e[0]or F(v,e[1])if[]==e*0else e!=v if''==e*0else F(v,e[0])and F(v,e[1])
f=lambda x,u:0*x==()and u==x[1]
T=lambda e,v='$':e if''==e*0else(T(e[1][0],v)if f(*e[::-1])and F(e[0],e[1][0])else(('K',T(e[1],v))if F(*e)else(I if e[0]==e[1]else T([e[0],T(*e[::-1])],v))))if[]==e*0else((('W',e[0][0])if f(e,v)else(('C',e[0][0]),e[1]),v)if f(e[0],v)else(((('B',e[0]),e[1][0]),v)if f(e[1],v)else((I,v)if v==e[0]else T(e[0],v),T(e[1],v))))

Try it online!

Previous byte counts: 628, 617, 559, 552, 536, 506, 495, 480, 472, 461, 456

I was working on a term-rewriting procedure for this in my free time anyways, why not golf it? Input/Output format is strings for variables, tuples lists of length two for lambda abstractions, and lists tuples of length two for applications.

(Reduced char count by switching input/output method)

(Reduced to 559 bytes thanks to @ovs)