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?

  • 1
    $\begingroup$ $(\lambda x_n.(\lambda x.A)M_1)M_2$ is not a subterm of $\lambda x_1.\dots\lambda x_n.(\lambda x.A)M_1M_2\dots M_m$. The latter means $\lambda x_1.\dots\lambda x_n.(\dots(((\lambda x.A)M_1)M_2)\dots M_m)$. I strongly recommend fully parenthesizing lambda terms as misparsing them is a constant source of errors for people starting out with them. $\endgroup$ – Derek Elkins May 7 '18 at 13:44

Your Answer

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

Browse other questions tagged or ask your own question.