Lambda calculus: S-problem: not quite seeing the pattern
So, I'm wading through the practice problems in Davie's chapter on Lambda Calculus, and he throws this one at me:
So, I tried to do this just by substituting and following the rules (fortunately I had already calculated S (S S) and (S S)). But by about the third piece of paper I lost track of the parenthesis and gave up. I threw it into a lambda calculator which used 1079 steps to produce a result that was over 15 lines long.
reduce the following λ-expression to normal form:
S (S S) (S S) (S S) S S
where S = λ x y z . x z (y z)
Now, likely Davie didn't intend to give me 5 hours of busy work, so presumably there is some pattern or short cut I am supposed to be seeing here. Does anyone have any insight they could share that would be beneficial to me here?
Re: Lambda calculus: S-problem: not quite seeing the pattern
I tried a couple of calculators and I got results similar to yours. It may be that different reduction strategies (call-by-name, call-by-value, etc.) would give very different number of steps, but the final expression seems indeed long and impractical to write by hand.