1
$\begingroup$

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?

$\endgroup$
1
$\begingroup$

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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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