I have following lambda calculus:
(λx. + (- x 1)) 9 3
The right beta reduce is:
+ (- 9 1) 3
I made a mistake and took instead of 9 the number 3:
+ (- 3 1) 9
and I've got the same result.
I wasn't realize that was wrong, until compare it with the solution.
Do I have to take the closest substitution, in this case is 9?
The fact you got the same answer in this arithmetic example is a coincidence caused by the arithmetic rather than the lambda calculus.
If you wrote more spaces to make the term structure clearer, it would be easier to see what's going on
(\x. + (- x 1)) 9 3
means, with gratuitous extra parentheses showing the parse tree,
((\x. (+ (- x 1))) 9) 3
because application associates to the left ("rather as we all did in the sixties" - Roger Hindley).
So, the 3 is in the wrong place to be substituted for the x. We have only
( (\x. (+ (- x 1))) 9 ) 3
=
(+ (- 9 1)) 3
=
(+ 8) 3
=
11
Yes, you always need to apply a lambda to its "first" (leftmost) argument.
In theory, there is not such a thing as multiple arguments, there is only application of a single argument. Still, it is common to write
f M N O for the repeated application (((f M) N) O). Note how f takes M as its argument.
In the general case, you will not get the same result if you do application in a different order. Your example was only an incident.
