I am trying to understand which are the right steps to perform the following reduction following the normal order reduction. I cannot understand which is the correct order in which I should perform the reduction, and why, in this expression:
(λn.λs.λz.n s (sz)) (λs.λz.s z)
could you please help me out?
Note: this reduction can also be seen as the function successor
(λn.λs.λz.n s (sz))
applied to the Church numeral 1
(λs.λz.s z)
knowing that the number zero is represented as:
(λs.λz.z)
The normal, AKA leftmost-outermost, reduction order attempts to reduce the leftmost outermost subterms first.
Since you are looking for the outermost terms, you need to determine the main building blocks of your term, remembering that every term is a variable, an abstraction over a term or an application of terms:
(λn.λs.λz.n s (s z)) (λs.λz.s z)
---------LHS-------- ----RHS----
----------APPLICATION-----------
The left-hand side (LHS) of the main term is the leftmost outermost one, so it is the starting point of the reduction. Its outermost abstraction is λn and there is a bound variable n in that term, so it will be substituted with the right-hand term:
λn.λs.λz.n s (s z)
-- -
However, since both LHS and RHS contain s and z variables, you need to rename them in one of them first; I chose to rename the ones in RHS:
λs.λz.s z -> λa.λb.a b
Now you can drop the λn abstraction and substitute the n variable with λa.λb.a b:
λn.λs.λz.n s (s z) -> λs.λz.(λa.λb.a b) s (s z)
-- - -----n-----
It's time to look for the next reduction spot:
λs.λz.(λa.λb.a b) s (s z)
Since lambda calculus is left-associative, this is the same as:
λs.λz.(((λa.λb.a b) s) (s z))
The next leftmost outermost reducible term is (λa.λb.a b) s which reduces to (λb.s b):
λs.λz.(((λa.λb.a b) s) (s z)) -> λs.λz.((λb.s b) (s z))
-- - - -
And the last reducible term is (λb.s b) (s z), where b is substituted with (s z):
λs.λz.((λb.s b) (s z)) -> λs.λz.(s (s z))
-- - ----- -----
Which leads to the final state in normal form:
λs.λz.s (s z)