1
$\begingroup$

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?

$\endgroup$
1
  • $\begingroup$ $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. $\endgroup$ Commented Dec 4, 2015 at 2:10

1 Answer 1

Reset to default
3
$\begingroup$

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}}$$

$\endgroup$

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.