A lambda-calculus function call is modeled by beta reduction. When an abstraction is applied to an argument,

$$(\lambda x.e)\ v \to_\beta e[v/x],$$

the argument replaces the function's bound parameter using capture-avoiding substitution.

For example,

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

reduces first to

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

and then to $\lambda y.y$.

An expression of the form $(\lambda x.e)\ v$ is a beta redex: a reducible expression. An expression containing no beta redex is in beta-normal form.

Not every term has a normal form. The self-application

$$\Omega=(\lambda x.x\ x)(\lambda x.x\ x)$$

reduces back to itself forever.

A term can also contain several redexes, so reduction may have choices. The lambda calculus is confluent: if a term can reduce along different paths to normal forms, those normal forms agree up to alpha-equivalence. Confluence does not guarantee termination, but it means reduction order does not create two incompatible final answers when a normal form is reached.