Application Ambiguity in Untyped Lambda Calculus So, untyped lambda calculus has the following formal grammar for its terms:

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

Usually this is presented in some ML-esque language as (using de Bruijn indices)

data term = variable Nat | lambda term | apply term term


My question is: apply (variable Nat) term is syntactically valid, but the rator is just a free variable, isn't this an invalid expression? If not, what does it evaluate to?
You can't evaluate (x t), where x is free, since evaluation ($\beta$-reduction) is usually defined in terms of substitution, but here you have neither a bound variable nor a function body for $t$ to be substituted into.

A term that cannot take a further step is called a normal form.