Benjamin C. Pierce's Types and Programming Languages presents on page 54:
The following expression, (1 + 2) * 3
, becomes the following concrete Abstract Syntax Tree:
Pierce goes onto say:
To saving writing too many parentheses, we adopt two conventions when writing lambda-terms in linear form. First, application associates to the left – that is,
s t u
stands for the same tree as(s t) u
:
Second, the bodies of abstraction are taken to extend as far to the right as possible, so that, for example,
$$\lambda x. \lambda y. x y x$$
stands for the same tree as:
$$\lambda x. (\lambda y. ((x y) x)$$
My incomplete understanding is that the second tree can be represented in a Lambda Calculus via the last tree?
Or, put differently, how does the second tree map/relate to the third? I'm not understanding the $\lambda$ usages.
Best Answer
The terms $\lambda x.\lambda y.x y x $ and $\lambda x.(\lambda y.((x y) x))$ both have the same abstract syntax tree, namely
This means that, as far as the meaning is concerned, the two symbol strings "$\lambda x.\lambda y.x y x $" and "$\lambda x.(\lambda y.((x y) x))$" should be thought of as two representations of the same term.