 Weak combinatory reduction

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.