Background
Combinatory logic is a system where a term is written using a finite set of combinators and function application between terms, and reduction rules are defined for each combinator. The well-known S and K combinators have the following reduction rules:
$$ \begin{aligned} S\;x\;y\;z & \overset{S}{\implies} x\;z\;(y\;z) \\ K\;x\;y & \overset{K}{\implies} x \end{aligned} $$
A term is in normal form when no reduction is possible. A term has a normal form if a series of reductions applied to it gives a normal form. The halting problem in combinatory logic is essentially about determining whether a term has a normal form.
In a previous challenge of mine, I mentioned that the halting problem for K is trivial; it always terminates, and we can always find the normal form of a K expression.
Challenge
Given a K combinatory logic expression, simplify it into its normal form. For this challenge, the expression is to be input/output as a string (list of chars or charcodes is also acceptable), using prefix notation:
expr := "K" | "@" expr expr
So the expression \$K(KK)(KK)K\$ is given as @@@K@KK@KKK
. The reduction rule can be also rewritten as
@@Kab => a
where a
and b
are valid expressions. The input is guaranteed to be a valid expression as a whole. You may use k
instead of K
, and any non-kK
non-space printable ASCII character instead of @
.
Standard code-golf rules apply. The shortest code in bytes wins.
Test cases
Generated using this Python script.
K -> K
@KK -> @KK
@K@KK -> @K@KK
@@KK@KK -> K
@@@@KK@KKKK -> K
@K@@@KKK@K@KK -> @K@K@K@KK
@@@KKK@@@KKK@@KKK -> @K@KK
@@@@@@@KK@KKK@@KK@@KK@KK@@@@KKK@@KKK@@K@KK@KKK@@@@K@@KK@KK@K@KK@@@KKK@K@K@KK@@@K@KK@K@K@KK@@@KK@@KK@KK@@KKK -> @K@K@K@K@KK