Significance of the inner parentheses in this lambda expression? $(\lambda xyz.xy(zx)) \;1\; 2\; 3$

Question

I have this lambda expression

$$(\lambda xyz.xy(zx)) \;1\; 2\; 3$$

or

$$(\lambda x. (\lambda y. (\lambda z.xy(zx))))\;1\;2\;3$$ $$(\lambda y. (\lambda z.1y(z1))))\;2\;3$$ $$(\lambda z.12(z1))))\;3$$ $$1\;2\;(3\;1)$$

What exactly is the point of the inner parentheses in the original expression -- which I dutifully carried along to the end? What's the difference between $1\;2\;(3\;1)$ and $1\;2\;3\;1$? The outer is to distinguish between the expression and the input, I'm assuming, but the inner $\ldots(zx)\ldots$ isn't clear to me. Parentheses in math indicate "belonging together," but I don't understand this "belonging together." Even if I wanted to have two $x$ variables in the body, I'd just have them without needing parentheses. I checked out this, but I don't think it's the same parentheses issue.

Answer 1

First of all, I should point out that there are two ways to understand the lambda calculus, it can be typed or untyped. Not all lambda terms can be typed.

---

First observe that the term $λxyz.xy(zx)$ can be typed. Since it takes three arguments, let us say the type is $$\alpha\to\beta\to\gamma\to\delta$$ so that given $x:\alpha, y:\beta,z :\gamma$ we obtain $xy(zx):\delta$.

Now in the body, $z$ is applied to $x$, so this means $\gamma = \alpha\to\eta$, and $zx : \eta$. Similarly, $x$ is applied to $y$ and $zx$, so it must be that $\alpha = \beta\to\eta\to\delta$. Putting this together we get that

$$λxyz.xy(zx) : (\beta\to\eta\to\delta)\to\beta\to((\beta\to\eta\to\delta)\to\eta)\to\delta.$$ We can now check that if $$x : \beta\to\eta\to\delta\\y:\beta\\z : (\beta\to\eta\to\delta)\to\eta$$ then $$zx: \eta\\xy:\eta\to\delta\\xy(zx):\delta.$$

What this means is that for the application $(λxyz.xy(zx))\ u\ v\ w$ to make sense in the typed setting, it must be that for some given types $\beta,\eta,\delta$ we have $u:\beta\to\eta\to\delta$, $v :\beta$, and $z:(\beta\to\eta\to\delta)\to\eta$. Since $\mathbb N$ is not a function type, the first and third arguments cannot be of type $\mathbb N$.

---

Now if you still wish to give some sense in an untyped setting to the term $(λxyz.xy(zx))\ 1\ 2\ 3$, you can only do this if you interpret $1, 2,3$ as lambda terms. You can do this using a Church encoding, that is if you define $$0 := \lambda s.\lambda z. z\\ 1:=\lambda s.\lambda z. sz\\ 2:=\lambda s.\lambda z. s(sz)\\ 3:=\lambda s.\lambda z. s(s(sz)).$$

Then, your expression $1\ 2\ (3\ 1)$ corresponds to the term $$(\lambda s.\lambda z.sz)(\lambda s.\lambda z.s(sz))((\lambda s.\lambda z.s(s(sz)))(\lambda s.\lambda z. sz))$$ which you can reduce further.

---

You could also check out this question for an explanation of the structure of a lambda term.

Answer 2

Syntactically, function application is a two-operand non-associative operation, where the latter means that $f(g\,x)$ has to be distinguished from $(f\,g) x$ (the function application operation conventionally has an empty operator symbol, in other words the two operands are just juxtaposed; for the current discussion it would however make no difference if a visible operator symbol were used). The basic solution to avoid ambiguity for formulas that contain more than one such operation is to require parentheses around every non atomic sub-expression that is itself operand of another application, as in the two examples I cited. One can reduce the number of required parentheses somewhat by stipulating that in one of the two operand positions the parentheses can be omitted, and indeed in $\lambda$-calculus such omission is allowed for the left operand, so $(f\,g)x$ can be written simply as $f\,g\,x$ (the operation is then said to associate to the left). But of course the parentheses must by retained in the case of a right operand, to be able to distinguish $f(g\,x)$ from $f\,g\,x$.

Since $\lambda$-calculus also has $\lambda$-expressions, it may be useful to state how these enter into the syntactic game. By convention $\lambda$-abstraction binds weaker than function application, which means that a $\lambda$-expression that is an operand of a function application, either left or right, always needs to be parenthesised; on the other hand no additional parentheses are needed to hold a function application that is the "body" of the $\lambda$-expression together. A new $\lambda$-expression that occurs directly as body of another one also requires no additional parentheses, since in this case there is actually no ambiguity on how to parse something like $\lambda x.\lambda y.x$ in the first place.