Lambda Calculus: β-Reduction

Church's original model of computation — functions, variables, substitution