# Rigorous reason against the seemingly wrong way of substitution

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 ?

• $1+2*3$ could stand for $(1+2)*3$ or $1+(2*3)$. What is the "rigorous reason" to choose the latter and not the former? None: it is only a syntactic convention -- deriving from convenience rather than rigor. – chi Mar 6 '18 at 21:59

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.

• :Thanks a lot . I understand a little about trees if what you meant by them is somehow similar to "syntax trees" obtained after parsing . Still then could you provide some source where a more detailed view of lambda calculus through tress has been provided ? – Agnivesh Singh Mar 7 '18 at 18:01
• @AgniveshSingh I don't know of any resources, maybe the PLAI book? It's exactly the "syntax tree" from after parsing, but the key is, I like to think of the syntax tree as the language itself, and the code you parse as just a representation of the tree. But operations like Beta-reduction operate on trees, they're phrased to treat lambda expressions as trees. – jmite Mar 7 '18 at 18:06
• Was there anything wrong with the second way of beta reduction in my post ?If not then , does that mean that the argument can be taken even for the second bound variable as well ? – Agnivesh Singh Mar 7 '18 at 18:17
• And hence wouldn't the church rosser theorem suggest them to be equivalent ? – Agnivesh Singh Mar 7 '18 at 18:17
• About trees , isn't the whole construction of the tree dependent on what we write in the code of the parser ? As such again , as you have suggested earlier , it boils down to whims of human understanding , isn't it ? – Agnivesh Singh Mar 7 '18 at 18:28