0

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.

147pm
  • 920
  • $xy(zx)$ means ($x$ applied to $y$) applied to ($z$ applied to $x$). It doesn't make sense to pass $1\ 2\ 3$ as arguments because $x$ and $z$ must be functions. – Couchy Dec 09 '21 at 06:08
  • I don't follow you. $xy(zx)$ is the body of a lambda expression. I'm not aware of any "applied to" relationship between body members. I've edited the OP to elaborate better what I'm after. – 147pm Dec 09 '21 at 16:43
  • 1
    Then it seems you don't understand lambda calculus. A term is either a variable, an application of two terms, or a lambda abstraction whose body is itself a term. – Couchy Dec 09 '21 at 16:47
  • Application associates to the left, which is why the parentheses are needed. – Couchy Dec 09 '21 at 16:49

2 Answers2

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.

Marc van Leeuwen
  • 115,048
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.

Couchy
  • 2,722
  • 1
    Yes, I can begin to follow now. From SML-family experience (Haskell), we have to assume that the $x$, $y$, and $z$ are different types, therefore $\alpha\to\beta\to\gamma\to\delta$ and $xy(zx):\delta$. I was hung up on the "applied to" within the body. The numbering system and successor lambda expression bring out this fine distinction. This "applied to" within the body is not part of beta reduction's "applying" data to the lambda expression. – 147pm Dec 09 '21 at 18:20