3

I am working problems in Hindley and Seldin. The -reduction for this formula eludes me at a certain step, because I am having trouble understanding the ordering of function application. Yes, the applications associate to the left - but what order should the applications be performed in? Should, for instance, the most deeply nested applications be performed first?

(λxyz.xz(yz))((λxy.yx)u)((λxy.yx)v)w

The latter two terms trivially reduce, yielding:

(λxyz.xz(yz))(λy.yu)(λy.yv)w

At this point, Hindely and Seldin note 3 contractions get you to:

(λy.yu)w((λy.yv)w)

Now, I can't tell what sequence of contractions moves the w into the center. And Hindley and Seldin don't say. If someone could please assist here, and let me know whether for instance w should be substituted into (λy.yv) first, or whether (λy.yu) should be substituted into (λxyz.xz(yz)), and what the principle is behind the sequencing of substitutions, as I don't think it's been elucidated yet in Hindley + Seldin (though perhaps I missed something in their exposition)?

infinitesimal_microscope
  • 33
  • The easiest way to view this somewhat complicated formula is through combinatory logic (CL) if you recognize $λxyz.xz(yz)≡\mathsf{S}$ combinator, then your first formula quickly becomes a typical weak redex $\mathsf{S}(λy.yu)(λy.yv)w$ which can be immediately weakly reduces to $(λy.yu)w((λy.yv)w)$ which then immediately β-reduces to $wu(wv)$. But you have to use CL which perhaps you cannot invoke here... – cinch Oct 01 '21 at 05:19

2 Answers2

2

It's in the remark 1.29 right after that exercise. There are as many beta-contraction possibilities as there are redexes in a term, so as soon as a term contains more than one redex, several reductions (= series of contractions) are possible, and all of them are legitimate.

In principle it doesn't matter which one you pick, in the sense that if a term can be reduced to two different terms, then these two terms can always be further reduced to one same term. This property is called confluence, for the lambda calculus also known as the Church-Rosser theorem, and essentially means that the end result of a function application does not depend on the calculation path:
enter image description here

However, while different reductions will never yield different end results in the sense of different normal forms (= terms which can be reduced no further), it may happen that some reductions get stuck in an infinite loop and never lead to a normal form at all, while other reductions with the same starting term succeed. The quasi-leftmost reduction theorem states that if it is at all possible to reach a normal form, then a reduction in which at least every couple steps it is the leftmost redex (which is the one with the lambda furthest on the left) which is contracted will lead to success. This entails that a strictly-leftmost reduction, in which in every step the leftmost redex is contracted, will also work.

So if you want to be on the safe side, simply always choose the leftmost redex for the next contraction step.

In the present example, a strictly-leftmost reduction proceeds as follows (in each line, the redex to undergo contraction in the next step is underlined, and the term obtained from contraction in the previous step is overlined):

$\newcommand{\bred}{\triangleright_\beta} \phantom{\bred\ } \underline{(\lambda xyz.xz(yz))(\lambda y.yu)}(\lambda y.yv)w\\ \bred \underline{\overline{(\lambda yz.(\lambda y.yu)z(yz))}(\lambda y.yv)}w\\ \bred \underline{\overline{(\lambda z.(\lambda y.yu)z((\lambda y.yv)z))}w}\\ \bred \overline{\underline{(\lambda y.yu)w}((\lambda y.yv)w)}\\ \bred \overline{wu}\underline{((\lambda y.yv)w)}\\ \bred wu\overline{(wv)} $

But any other reduction strategy will get you there as well.

Natalie Clarius
  • 10,530
  • So if under the guidance of quasi-leftmost reduction theorem, should the underline of the first step in your answer stretch to the λ-term $(λy.yv)$? So the final answer should arrive as $wv(wu)$. – cinch Sep 29 '21 at 04:54
  • No. $(\lambda xyz.xz(yz))(\lambda y.yu)(\lambda y.yv)$ is not a redex. The redex to undergo contraction in the first step is $\lambda xyz.xz(yz)$ applied to $(\lambda y.yu)$. This is the leftmost redex, and the only one available for this step. But e.g. in the next step, one could alternatively choose to contract $(\lambda y.yu)z$ first instead of the leftmost redex underlined. But a different reduction can not possibly lead to a different end result. That's what confluence means. – Natalie Clarius Sep 29 '21 at 11:01
  • The quasi-leftmost reduction theorem means that as long as you at least occasionally choose the leftmost redex for contraction, you will arrive at a normal form, if there is one at all., which is the case for this exercise. Here for simplicity I chose to not only quasi-leftmost reduce, but strictly-leftmost reduce, i.e., pick the leftmost redex in every step. – Natalie Clarius Sep 29 '21 at 11:03
  • Here's a another interesting example $λyz.(λuv.u)zy$, if apply the right β-redex first we should add parentheses as $λyz.((λu.(λv.u))(z)(y))$ ▹β: $λyz.((λv.z)y)$ ▹β: $λyz.z$. But if first we apply left-most β-redex we should add parentheses as $(λy.(λz.(λuv.u)))(z)(y)$ ▹β: $(λz.(λuv.u))y$ ▹β: $λuv.u$▹α: $λyz.y$. And it's well known $λyz.y$ cannot be equivalent to $λyz.z$, otherwise all λ-terms would be equal. But in this case only the first right β-redex approach is correct since by default without explicit parentheses, the scope of $λyz.$ stretches to the very end, so $λyz.$ applies no term.. – cinch Sep 30 '21 at 05:41
  • Obviously changing the lambda term to a different one leads to a different end result; if you add parentheses to $1 \cdot 5 + 3$ to make it $1 \cdot (5+3)$, it becomes equal to $8$ instead of $9$, but that doesn't mean that the original term has multiple values, it just means parentheses matter. – Natalie Clarius Sep 30 '21 at 12:29
  • The point is that contracting the available redexes in the same existing lambda term in a different order will always eventually yield the same normal form, just like $(5+4)-(2/1)$ will always be equal to $7$, no matter if you choose to calculate in the order $(5+4)-(2/1) = 9-(2/1) = 9-2=7$ or $(5+4)-(2/1)=(5+4)-2=9-2=7$. – Natalie Clarius Sep 30 '21 at 12:29
  • I think my last two comments didn't quite address what you wrote. When performing beta reduction you can't just add parentheses, because that changes it to a whole different term. You must work with the existing term with the existing parentheses and redexes. In the present example, $λyz.(λuv.u)zy$, there is only one redex, namely $(λuv.u)z$, which is thereby simulatenously the leftmost and the rightmost redex, and that's the only contraction you can perform in this step. – Natalie Clarius Oct 01 '21 at 19:48
  • ... But there are other steps where the existing term with the existing bracketing gives rise to several redexes, e.g. in the second step, $(\lambda yz.(\lambda y.yu)z(yz))(\lambda y.yv)w$, the first (leftmost) redex is $(\lambda yz.(\lambda y.yu)z(yz))(\lambda y.yv)$ and the second (and rightmost) redex is $(\lambda y.yu)z$, and the order of choice between these can not possibly lead to different end results. That's confluence. – Natalie Clarius Oct 01 '21 at 19:56
  • I totally agree. Another confusion about left-associative in λ-calculus is perhaps for if/then/else... – cinch Oct 01 '21 at 19:58
  • What do you mean? – Natalie Clarius Oct 01 '21 at 20:08
  • I just saw a new post here discussing parentheses priority facing if/then/else... – cinch Oct 01 '21 at 20:13
1

Per its left association rule you should first apply left-most $λx$ out of $λxyz$ and shouldn't worry about $w$'s applicative substitution yet since it's at the end of your term and far away from the left-associated redex. From your second term actually it becomes:

$≡[(λy.yu)/x](λyz.xz(yz))(λy.yv)w \\ : (λyz.(λy.yu)z(yz))(λy.yv)w \\ : (λyz.zu(yz))(λy.yv)w \\ ≡[(λy.yv)/y](λz.zu(yz))w\\ : λz.zu(((λy.yv)z))w \\ : (λz.zu(zv))w \\ : wu(wv) $

Note it takes 3 contractions as your book mentioned to arrive at your last term in your book which is my third step counted from the last and your book's suggestion may not be unique or simplest here...

cinch
  • 1,648
  • 1
  • 4
  • 12