Combinatory logic term (source code)

= Combinatory logic term
{title2=$T::=x\mid S\mid K\mid I\mid TT$}

= CL-term
{c}
{synonym}

A finite applicative expression over free variables and the combinator constants $S,K,I$, with application associating to the left. One may instead take $I$ as the abbreviation $SKK$. There is no variable binder in this syntax.