Head position in lambda calculus

261 Views Asked by At

I'm confused about what actually constitutes the head position in a lambda term. Wikipedia defines it as the $(\lambda x. A) M_1$ in:

$\lambda x_1 . \ldots \lambda x_n . (\lambda x . A) M_1 M_2 \ldots M_m$ , with $n \ge 0, m \ge 1$

However, if this is true, why can't I go ahead and say $(\lambda x_n. (\lambda x. A) M_1 ) M_2)$ is in head position? I could continue widen the my "head" until I run out of abstractions or applications.

Because normally, I would evaluate the term like this: $\lambda x_1 . \ldots \lambda x_n . (\lambda x . A) M M_1 \ldots M_m$ =

$\lambda x_2. \ldots \lambda x_n. (\lambda x.A)[x_1 = M] M_1 \ldots M_m$, and so on

Are any of the above statements true?