Rigorous reason against the seemingly wrong way of substitution

Question

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 ?

Answer 1

You're not going to find a rigorous reason, because there is no semantic reason. The reason is purely syntactic.

The key is to remember that lambda calculus expression are, in fact, trees. A node is either a variable, with no children, an application with two children, or a lambda, with two children, one of which is the variable it binds.

Trees are hard to write, so we have a syntax for writing expression trees in a linear way. If we wrap every expression in parentheses, there's an unambiguous mapping between linear expressions and trees. But any time that parentheses are missing, we need precedence rules to disambiguate.

The choice of precedence rules is arbitrary, and is purely catered towards human understanding.

Once you're working with trees, or at least fully parenthesized expressions, then it should be more clear why the argument is given as the outermost bound variable: application is a binary operation between siblings in the trees. Other than the substitution operation, we don't want to have to look up or down the tree when applying a reduction.

If you want a syntax where you don't always apply arguments this way, you may be interested in the spine calculus, which is a syntax that nicely captures the idea of applying multiple arguments to a single core, called the head.