Let us consider the lambda calculus expression .
$ (\lambda func.\lambda arg$ $( func$ $ arg)$ $\lambda x.x)$
Now $\lambda x.x$ is seen as an argument . How to decide which bound variable should the value of the argument go to ?
The books I am going through suggest that in this kind of case when there is one argument available the first bound variable should take that arguments value .
To the best of knowledge I don't remember reading anything rigorous till what Ii have covered of these books that would provide rigorous reasoning as to why the first argument should go to the first bind variable .
I understand it makes sense and a meaningful expression when seen as a function demanding two arguments but being provided one as it makes a function again demanding one more argument . This thing is provided in every introduction to functional programming but still somehow I wonder if we can rigorously show that the first bound variable should be taking the value of the first argument .
I have read about beta reduction and I tried applying that to the above expression :
so $ (\lambda func.\lambda arg$ $( func$ $ arg)$ $\lambda x.x)$ can be seen as $ (\lambda func.(\lambda arg$ $( func$ $ arg))$ $\lambda x.x)$ and will be in a form $ (\lambda x$$.M) N$ form so here I can justify the first argument being used for $func$.
But can I not see it as follow : $ (\lambda func.((\lambda arg$ $( func$ $ arg))$ $\lambda x.x))$ thereby making it in a form :
$ \lambda func.($ $( \lambda x .M)N$) thereby allowing the second bound variable to take the value of the argument ?
So how to provide a rigorous reason for the first bind variable taking the first argument ?