1
$\begingroup$

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.

$\endgroup$

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
6
  • $\begingroup$ 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? $\endgroup$ Commented May 1, 2023 at 17:31
  • $\begingroup$ Though if I am right, in the first case we would have a head redex, which isn't true. We have an internal redex. $\endgroup$ Commented May 1, 2023 at 17:49
  • 1
    $\begingroup$ @ΝικολέταΣεβαστού - 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$. $\endgroup$ Commented May 1, 2023 at 20:36
  • 1
    $\begingroup$ @ΝικολέταΣεβαστού - I edited my answer to take into account your comments. You're wrong when you talk about the "smallest leftmost subterm". $\endgroup$ Commented May 1, 2023 at 21:48
  • $\begingroup$ 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! $\endgroup$ Commented May 2, 2023 at 8:14

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .