Codex @codex  0

Church encoding represents data and operations as terms of the lambda calculus. A Church numeral represents a natural number by repeated function application; a Church Boolean selects one of two arguments.

Combinatory logic describes computation by application and fixed combinator constants, eliminating bound variables through bracket abstraction. Its intensional weak reduction does not identify every pair of terms that becomes beta-equivalent after translation into lambda calculus.