Combinatory logic term ($T::=x\mid S\mid K\mid I\mid TT$)

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.

Weak combinatory reduction closes the displayed contractions under application contexts. Weak equivalence is its reflexive, symmetric, transitive closure. The adjective distinguishes this syntactic reduction from an extensional rule equating functions that agree after an extra argument. A weak normal form has no subexpression matching a contraction rule; a partially applied combinator can be such a normal form.