Use of Parentheses in Lambda Calculus when λ is Involved

881 Views Asked by At

The question about use of parentheses in lambda calculus here covers the basic idea of how parentheses are formatted in lambda calculus; however, it does not cover scenarios where $\ \lambda $ is involved.

What are the rules for use of parentheses in lambda expressions, when $\ \lambda $ is involved? For example, what would the parenthesization of $\ (\lambda y.y) \space (\lambda x.\lambda z.z \space \space y) \space w \space $ look like?

1

There are 1 best solutions below

0
On BEST ANSWER

The $\lambda$-term $(\lambda y.y)(\lambda x. \lambda z. z y) w$ is a term of the form $NML$, where

\begin{align} N &= \lambda y.y & M &= \lambda x. \lambda z. zy & L &= w \end{align}

As summarized here for notations:

  • application is left associative, which means that $NML$ must be read as $(NM)L$, that is, the term is constructed by first applying $N$ to $M$, and then by appling the whole term $NM$ to $L$;

  • abstraction extends as far right as possible, which means that $\lambda x. \lambda z.zy$ must be read as $\lambda x. (\lambda z.(zy))$, that is, the term is constructed by first applying $z $ to $y$, then by abstracting $z$ from $zy$--yielding $\lambda z.zy$--and finally by abstracting $x$ from $\lambda z.zy$--yielding $\lambda x.\lambda z.zy$.

Therefore, a fully parenthesized presentation of the $\lambda$-term $(\lambda y.y)(\lambda x. \lambda z. z y) w$ is the following:

$$\bigg((\lambda y.y) \color{red}{\Big(}\lambda x. \color{blue}{\big(}\lambda z. (z y)\color{blue}{\big)} \color{red}{\Big)}\bigg) w$$

Notice that in the $\lambda$-term $(\lambda y.y)(\lambda x. \lambda z. z y) w$ there is only one $\beta$-redex, the subterm $(\lambda y.y)(\lambda x. \lambda z. z y)$.