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.
Application () — left-associative functional application
CombinatorK, CombinatorS — fundamental combinators
CombinatorB ▪ CombinatorC ▪ CombinatorI ▪ CombinatorW ▪ CombinatorY
Construct — Wolfram Language application
Function — abstraction in λ calculus
Automated Theorem Proving »
FindEquationalProof — generate representations of proofs in combinatory logic