I have a question regarding lambda calculus normal order reduction. Essentially every explanation I've found is similar to this answer, which describes the order as ([reduce] the leftmost outermost $\beta$-redex first" (bold is mine), and then proceeds to enact what I would just think of as the "leftmost" (when reading the string from left to right) applications.
"Leftmost outermost" seems to apply two coequal criteria, but I can't even seem to find the second term being enacted. What does the word outermost mean in this context, and how would the ordering be different if it weren't there?
Best Answer
Depending on the definition of leftmost, the adjective outermost may be or not be superfluous.
The most common meaning of leftmost is the one pointed out by Lemontree in his comment, and it refers to the syntactic tree associated with each $\lambda$-term. First, you define the notion of outermost and innermost redexes. In a $\lambda$-term $M$, a redex is
A term may contain several outermost redexes and several innermost redexes. For instance, in the $\lambda$-term $x ((\lambda y.y)y) ((\lambda z.z)z)$, the two redexes are outermost (and innermost too!). Two fix an order so as to define an evaluation strategy, we choose the leftmost or the rightmost redex among the outermost or innermost ones, where leftmost (resp. rightmost) means the one that occurs leftmost (resp. rightmost) in the syntax tree of the $\lambda$-term. In this way, there is at most one leftmost-outermost redex in a $\lambda$-term, and similarly for leftmost-innermost, rightmost-innermost, etc.
Clearly, this definition of leftmost (and of rightmost) makes sense only together with the notion of outermost or innermost.
A second possible meaning of leftmost is less common but it is used for instance in Krivine's textbook. Since a redex has necessarily the form $(\lambda x.M)N$, in every $\lambda$-term, each subsequence of the form "$(\lambda$" corresponds to a unique redex in that term. We can then define the leftmost redex in a $\lambda$-term $M$ as the redex whose "$(\lambda$" part occurs leftmost in $M$, seen as a string of characters.
In this second definition of leftmost, the adjective outermost is clearly superfluous: the leftmost redex (in this second meaning) is necessarily outermost (in the sense defined above). Actually, this second meaning of leftmost coincides with the definition of leftmost-outermost above: both definitions identify the same redex in a $\lambda$-term (if any), although they follow a different procedure to identify it. Indeed, the only difference is in the meaning of the word "leftmost" in the definitions of "leftmost-outermost redex" and of "leftmost redex".
In the literature, the definition of the normal order reduction via the notion leftmost-outermost redex is common (and often preferred to the one via the second meaning of leftmost) because it is flexible: indeed, using the same approach one can define other evaluation strategies based on the leftmost-innermost redex, the rightmost-innermost redex, etc.