# 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.
• So apply (variable Nat) term is valid (not just syntactically, but in general), and furthermore in normal form? – Alex Nelson Nov 19 '15 at 21:58
• @AlexNelson It's in head normal form. If term is in normal form then apply (variable n) term is in normal form. You can recognize normal forms in that if you start from every application and go left until you hit something that isn't an application, what you hit is always a variable, never a lambda. – Gilles 'SO- stop being evil' Nov 20 '15 at 0:24