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?
It's down to the placement of the parenthesis.
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}}$$