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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$
4
  • $\begingroup$ So apply (variable Nat) term is valid (not just syntactically, but in general), and furthermore in normal form? $\endgroup$ Commented 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$ Commented 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$ Commented 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$ Commented 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.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.