Lambda calculus

Lambda calculus uses a small syntax: variables name expressions, abstraction forms functions, and application supplies an argument. Functions and arguments belong to the same expression system, allowing functions to become inputs and results. This simplicity focuses analysis on computation rules rather than on the instruction set of a particular physical computer.

References: [1]

Beta reduction applies an abstraction by substituting an argument into its body. Substitution must avoid capturing free variables and accidentally changing their bindings. Renaming bound variables can preserve meaning, so the formal treatment distinguishes surface spelling from the underlying structure and relationships that determine what an expression represents.

References: [2]

An expression can contain several reducible parts. Evaluating an argument first and reducing a surrounding application first can produce different computation paths; one strategy may reach a result where another does not terminate. Untyped lambda calculus includes expressions without normal forms, so simple rules do not guarantee successful evaluation of every expression.

References: [1]

Lambda calculus contributed to the formalization of effective computation and has rigorous connections to other classical models. Practical languages using lambda syntax add types, effects, and input-output facilities. Their semantics are not simply the untyped calculus unchanged; the calculus instead supplies a precise setting for studying functions, binding, and evaluation.

References: [2]