Combinatory logic is a formal system, equivalent to λ calculus, that can express functions without the use of formal variables. Every term is a function and there is just one binary operation, application.
Construct — Wolfram Language application
Function — abstraction in λ calculus
FindEquationalProof — generate representations of proofs in combinatory logic