# Why is a head redex always the leftmost redex?

I am studying lambda-calculus from Sorensen's book (Lectures on the Curry-Howard Isomorphism, 2006 edition), and on page 15 there is a definition of 'head redex'

in a lambda term $$\lambda\vec{z}.(\lambda x P)Q\vec{R}$$ the subterm $$(\lambda x P)Q$$ is called head redex.

It is then claimed that

a head redex is always the leftmost redex.

Why is that?

It seems to me that it isn't necessarily the leftmost redex.

From the definition of $$\lambda$$-term it follows that every $$\lambda$$-term $$t$$ can be uniquely written in the form

$$\tag{1} \lambda x_1 \dots \lambda x_n. s_0 s_1 \dots s_m$$ for some $$n,m \geq 0$$ and some $$\lambda$$-terms $$s_0, s_1, \dots, s_m$$, where $$s_0$$ is either a variable (and then $$t$$ is a head normal form) or a $$\beta$$-redex $$(\lambda y. t_1)t_2$$ (which is called the head redex of $$t$$) for some $$\lambda$$-terms $$t_1, t_2$$. t If $$s_0$$ is the head redex of $$t$$ (that is, $$s_0 = (\lambda y.t_1)t_2$$ for some $$\lambda$$-terms $$t_1, t_2$$), then $$s_0$$ is the leftmost $$\beta$$-redex occurring in $$t$$, in the sense that in $$t$$ there is no subterm of the form $$(\lambda z.r)s$$ such that $$\lambda z$$ is to the left of the $$\lambda y$$ in $$s_0$$. Said differently, $$s_0 = (\lambda y.t_1)t_2$$ is the $$\beta$$-redex in $$t$$ whose $$\lambda$$ is the leftmost one among the $$\lambda$$'s of all the $$\beta$$-redexes occurring in $$t$$. To convince yourself, look at the way $$t$$ is written in $$(1)$$.

Note that the $$\lambda$$ of the head redex may not be the leftmost $$\lambda$$ in a term (there may be several $$\lambda$$'s to the left of it that are not in a $$\beta$$-redex), and that the head redex $$s_0 = (\lambda y.t_1)t_2$$ (if any) is also one of the outermost $$\beta$$-redexes (otherwise it would be inside another $$\beta$$-redex whose $$\lambda$$ is to the left of the $$\lambda$$ of $$s_0$$, which is impossible by definition of leftmost $$\beta$$-redex). For instance, in $$\lambda x \lambda x'.(\lambda y.(\lambda y'.y')y)y'' (xx) ((\lambda z.z)z')$$

the head redex is $$(\lambda y. (\lambda y'. y')y)y''$$, which is the leftmost $$\beta$$-redex and one of the outermost $$\beta$$-redexes (the other outermost $$\beta$$-redex is $$(\lambda z. z)z'$$ on the right). The $$\lambda$$ of the head redex (that is, $$\lambda y$$) is not the leftmost $$\lambda$$ of the term (which is $$\lambda x$$). In the head redex there is an inner $$\beta$$-redex, $$(\lambda y'. y')y$$, which is not a head redex for the whole term.

• So we were not talking about the leftmost written $\lambda$ (so that the leftmost would be the first one) but the smallest leftmost subterm that is an abstraction (if I am explaining it clear enough). Am I right? May 1 at 17:31
• Though if I am right, in the first case we would have a head redex, which isn't true. We have an internal redex. May 1 at 17:49
• @ΝικολέταΣεβαστού - We are talking about the about the $\beta$-redex in a term $t$ whose $\lambda$ is the leftmost one among the $\lambda$'s of all the $\beta$-redexes occurring in $t$. May 1 at 20:36
• @ΝικολέταΣεβαστού - I edited my answer to take into account your comments. You're wrong when you talk about the "smallest leftmost subterm". May 1 at 21:48
• I found this answer too that would help anyone not familiar with the term "outermost" Lambda calculus normal order - what is "outermost"?. Thanks a lot! Now it is all crystal clear! May 2 at 8:14