Understand free and bound variable associations in Lambda Calculus

I understand that free variables in Lambda calculus are those that are not bound to a specific metavariable inside of an abstraction, while bound variables are the direct opposite. The idea that confuses me is that of parenthetical placement inside of an expression/series of expressions.

expression = λa.λu.(au)(uta)


In an example like this, I look at this and see that au is parenthesized which I think makes a and u both free variables. Which, following that idea, would make u, t and a in the following set of would also be free.

Am I misunderstanding the order of evaluation in this expression?

@Rob Unfortunately I cannot reply to your comment, but the way I understand this would then be.

Original: expression = λa.λu.(au)(uta)

Proper disambiguation rule application:

expression = λa.(λu.((au)((ut)a)))


So technically t is the only free variable because it is not used in the same body that it's metavariable counterpart resides in? a is bound to the scope of the first lambda while u is bound to the scope of the second lambda?

• $a$ and $u$ are not free variables in $\lambda a . \lambda u. (au)(uta)$. The parentheses in the body of the $\lambda$-abstraction tell us what function of the parameters $a$ and $u$ the $\lambda$-abstraction calculates. The parentheses don't affect the scope of the variable bindings. Dec 4 '15 at 2:10

In $\sf\lambda u.\lambda a.(ua)(uta)$ all occurrences of $u$ and $a$ are bound.   The body of the statement extends until the end of line.   $(ua)(uta)$ is the application of $ua$ to $uta$, and it occurs within the nested scope.
$$\sf \lambda u.\underbrace{\lambda a.\overbrace{(ua)(uta)}^{a\textrm{ is bound}}}_{u\textrm{ is bound}}$$
In $\sf \lambda u.(\lambda a.ua)(uta)$ the second occurrence of $a$ is free. The application $uta$ is not within the scope of $\lambda a$; which is contained within the innermost parenthesis. However, $uta$ is within the scope of $\lambda u$, so the $u$ is bound while both $t$ and $a$ are free. The application $ua$ is nested within both scopes, so both $u$ and $a$ are bound there.
$$\sf \lambda u.\underbrace{\mathop{(\lambda a.\overbrace{ua})}^{a\textrm{ is bound}}(uta)}_{u\textrm{ is bound}}$$