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))
(<*>id)
\$\endgroup\$join
specialized for the Reader monad. \$\endgroup\$