Lambda Calculus Argument Delimiter

Question

So I've been looking into lambda calculus on and off for months simply trying to understand the numerical system and the successor function. I understand that it's basically just argument evaluation, but the syntax confused me for the longest time. Finally, I found this:

S0 = (λ abc.b(abc)) (λ sz.z) = λ bc.b((λ sz.z) bc) = λ bc.b((λ z.z) c) = λ bc.b(c)

from this URL: http://palmstroem.blogspot.com/2012/05/lambda-calculus-for-absolute-dummies.html

and realized that I didn't understand how this worked because there seems to be no delimiter indicating the start of argument space. My question is: Is there an acceptable delimiter for this in lambda calculus, and, if not, how can I verbalize this when writing or viewing it?

EDIT: Some people seem to have misunderstood this, so let me explain better. How do I indicate that a function is being called on a specific set of arguments? For example, in most programming languages the indicator is just parenthesis

function(arg0,arg1,arg3...)

Is there an equivalent to this in untyped lambda calculus?

ANOTHER EDIT: Okay, it's still misunderstood as to what I mean. Let's talk about the successor function again. The wikipedia pages shows something like the following:

Succ=La.Lb.Lc.b (a b c)
               ^

The marked whitespace is annoying since It's not clear that the part in parenthesis is still part of the function itself, and instead looks like an argument is being passed to the function. Is there a delimiting character that separates the body of the function from the arguments on which it is to be called? Example:

Succ=((La.(Lb.(Lc.(b,((a,b),c))))),),,

The problem that I think I'm having is that since functions can be returned as primary values, the syntax doesn't express that very clearly. However, in the example that I gave, we can see that there are three commas without trailing inputs, indicating that the function takes 3 values (the function to find the successor of and the successor's potential arguments). Is there a good convention to express the point where a function's body ends and the values that it needs to be evaluated begin?

*A VERY IMPORTANT EDIT: * This is not about currying.

Answer 1

So, I think part of the problem is that the resource you're using is not using standard lambda calculus notation.

In most texts, there is a space between arguments. I would write $\lambda x\ y\ z\ldotp z$ in place of $\lambda x y z\ldotp z$. But, if you assume a convention that variables are always single letters, you can omit the space without ambiguity.

But I can't imagine one would ever write whole programs this way. Rather, this is more likely to show up in examples, code snippets, and small proofs, where there aren't many variables and the names don't matter.

Basically it boils down to this:

• A minimal lambda calculus only allows one argument per function, so there's no need for a delimiter. The dot denotes the function body.
• There is common syntactic sugar for multiple arguments, which abbreviates $\lambda x \ldotp (\lambda y \ldotp (\lambda z\ldotp z))$ as $\lambda x\ y\ z\ldotp z$.
• In a situation where variable names are assumed to be single letters, one could use $\lambda x y z\ldotp z$ in place of $\lambda x\ y\ z\ldotp z$.

There is no delimiter, other than the space, that I know of for arguments. Commas would be frowned upon, since they indicate tuples, rather than curried arguments.

EDIT: to respond to the OPs edit:

There is no such thing as multiple arguments in an untyped lambda calculus, at least not in standard ones. There are two ways to simulate multiple-argument functions.

1. Tuples: you can use a Church encoding to pass a single argument, which can be decomposed into multiple values. So you would write $f (<x,y>)$, where $<x,y>$ is some special syntax for making a pair, and then decompose it as $HD\ t$ and $TL\ t$ inside your function to get at each argument.
2. Currying: When, in an imperative language, you would write f(x,y,z), you write $(f\ x\ y\ z)$, which is syntactic sugar for $(((f\ x)\ y)\ z)$. A function accepting multiple arguments is just a function which returns another function.

It turns out that these two are basically isomorphic, so which you do doesn't much matter.

Some languages, like Scheme, have built in syntax for multiple-argument functions, but I haven't seen anything like that in a formal lambda calculus. Usually they're intended to be minimal, and so when you don't need multiple-argument functions, you don't put them in.

Answer 2

People who do $\lambda$-calculus use a number of convenient abbreviations that make it a bit harder for the beginner to figure out what is going on. I will use no such abbreviations.

Since you are asking a very basic question it is difficult to guess where exactly your confusion lies. I will answer more broadly than is probably necessary, just to make sure you get your answer, and also for the benefit of others.

Expressions are trees

It is a historic accident that we write text from left to right in a straight line. We are so used to this that we devised ways of representing data that is not naturally linear in such a linear fashion. For example, an arithmetic expressions is most naturally viewed as a tree, e.g.,

is an arithmetical expression. We have a way of writing it down in a line:

(3 + 8) * 7

Here is another way of writing the same expressions:

(   3+   8)*7

That is, spaces are not important. The font is not important.

The process of converting a string of symbols into the corresponding tree is known as parsing.

In $\lambda$-calculus it is exactly the same. Expressions are really trees and it would be much better to draw them as trees, but that is impractical. So we write them in a straight line.

$\lambda$-calculus syntax

The syntax of $\lambda$-calculus (at least the basic version of it) is very simple. It is simpler than arithmetical expressions, and even simper than any programming language that people use in practice.

Spaces do not matter in $\lambda$-calculus.

There are precisely three ways in which you can create an expressions:

1. It can be a variable, say $x$, $y$, $z$, $x_1$, $y_{42}$ and similar. The letter $\lambda$ is not a variable because it is used for another purpose.

2. If we have two expressions, say $A$ and $B$ then we can juxtapose them and place parentheses around them to get $(A \, B)$. It does not matter how much space there is between $A$ and $B$. This is called application.

3. If we have an expression $A$ and a variable $x$ then we can write $(\lambda x \,.\, A)$ to get an expression. It does not matter how much space there is between $\lambda$ and $x$. The period between $x$ and $A$ is irrelevant, it is just a visual embellishment. This is called $\lambda$-abstraction.

It may help to see an example. The expressions that you wrote as

 (λ abc.b(abc)) (λ sz.z)

is written without any abbreviations (such as omitted parentheses) as

 ((λa.(λb.(λc.(b((ab)c)))))(λs.(λz.z)))

I hope I got that right. As a tree it is

You should understand this picture before proceeding.

How do we apply three arguments to a function?

We do no such thing. We can apply expression $A$ to expression $B$ by forming an application $(A \, B)$. This is the only way to apply anything. We always apply exactly one thing to exactly one argument.

Nevertheless, we can nest applications to get the desired effect of applying several things. For instance

((f x) y)

is the application of (f x) to y. It has the effect of applying f to two arguments. To see how this works, suppose we wanted a function which takes two arguments and it returns the first argument. This would be

(λu.(λv.u))

To apply this function to a and (c b) we do a double application:

(((λu.(λv.u)) a) (c b))

The way to think of this is that (λu.(λv.u)) first gets the argument a. It computes the result (λv.a). Then (λv.a) is applied to the second argument (c b), and it computes the result a.

If we want to apply f to three things a, b and c then we write

(((f a) b) c)

Without parenthesis and using standard conventions for abbreviations this is written as

f a b c

or equivalently as

f         a b      c

Keep in mind that we did not apply f to three things! Instead, we applied f only to a. Then we applied (f a) to b. Then we applied ((f a) b) to c. This gave the desired effect of passing three things to f.

If we wrote

(f (a (b c)))

then that would be f applied to one thing, namely (a (b c)). This is different from (((f a) b) c). If we wrote

((f a) (b c))

then that would be (f a) applied to (b c), so in effect this is like applying f to two arguments a and (b c).

I did not tell the whole story. I left out the concept of bound variables and I did not explain how substitution works. But I hope this clears up some misunderstanding.