Implement SKI combinator calculus This challenge is to golf an implementation of SKI formal combinator calculus.

Definition

Terms

S, K, and I are terms.

If x and y are terms then (xy) is a term.

Evaluation

The following three steps will be repeated until none of them apply.
In these, x, y, and z must be terms.

(Ix) will be replaced by x

((Kx)y) will be replaced by x

(((Sx)y)z) will be replaced by ((xz)(yz))

Input

A string or array, you do not have to parse the strings in the program.

The input is assumed to be a term.

If the simplification does not terminate, the program should not terminate.

Examples

(((SI)I)K) should evaluate to (KK) ((((SI)I)K) > ((IK)(IK)) > (K(IK)) > (KK))

The evaluation order is up to you.

This is code-golf. Shortest program in bytes wins.
Wolfram Language, 63 bytes

#//.{{I,x_}-&gt;x,{{K,x_},y_}-&gt;x,{{{S,x_},y_},z_}-&gt;{{x,z},{y,z}}}&amp;


Try it online!

God, I love pattern matching in Wolfram Language. Represents (xy) as {x,y} (a list of two elements).

Alternatively, if we represent (xy) with x&gt;y, we can do it in 55 bytes.

#//.{I&gt;x_-&gt;x,(K&gt;x_)&gt;y_-&gt;x,((S&gt;x_)&gt;y_)&gt;z_-&gt;(x&gt;z)&gt;(y&gt;z)}&amp;


Try it online!