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?


1 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.

  • $\begingroup$ So apply (variable Nat) term is valid (not just syntactically, but in general), and furthermore in normal form? $\endgroup$ Nov 19, 2015 at 21:58
  • $\begingroup$ @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. $\endgroup$ Nov 20, 2015 at 0:24
  • $\begingroup$ 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. $\endgroup$ Nov 20, 2015 at 7:08
  • $\begingroup$ Thank you so much for your help, Gilles and @AntonTrunov, I greatly appreciate your insight into this matter :) $\endgroup$ Nov 20, 2015 at 15:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.