Combinatory logic term
= 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.