Application Ambiguity in Untyped Lambda Calculus

Question

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?

Answer 1

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.

• Alex Nelson: So apply (variable Nat) term is valid (not just syntactically, but in general), and furthermore in normal form?
• Gilles 'SO- stop being evil': @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.
• Anton Trunov: I agree with @Gilles. And it also depends on the reduction strategy. For example, under normal order strategy it is in normal form, not just in head normal form. Under normal order strategy the leftmost, outermost term is always reduced first. That means the argument term is substituted into the function body before the argument term is reduced.
• Alex Nelson: Thank you so much for your help, Gilles and @AntonTrunov, I greatly appreciate your insight into this matter :)