The untyped lambda calculus is a minimal model of computation built from only three forms:

$$e ::= x \mid \lambda x.e \mid e\ e.$$

A variable names a value, an abstraction $\lambda x.e$ defines a function of $x$, and an application $e_1\ e_2$ applies one expression to another.

For example, the identity function is

$$I=\lambda x.x,$$

and applying it to $y$ gives

$$(\lambda x.x)\ y.$$

Despite its tiny syntax, functions can encode data and control structure. For instance,

$$\text{true}=\lambda t.\lambda f.t,$$ $$\text{false}=\lambda t.\lambda f.f$$

behave like Boolean selectors because true a b chooses $a$ and false a b chooses $b$.

Functions are values and can receive or return other functions, so higher-order programming is built into the model rather than added as a special feature.

The lambda calculus matters because it strips programming down to binding, abstraction and application. This makes it small enough for exact semantic proofs while remaining expressive enough to model general computation and the functional core of many real languages.