Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It only takes a minute to sign up.
Sign up to join this community
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.
