Argument Order

First Argument Fills the Outermost Lambda

In a curried function like λx.λy.M, the first argument fills x (the outermost parameter). The second argument fills y (the inner parameter).

(λx.λy.M) a →β λy.M[x := a]

The outer lambda peels away first, binding its parameter to the argument. The inner lambda survives, waiting for the next argument.

Which Variable Fills First?

When a curried function receives two arguments, reduction proceeds left to right:

(λx.λy.x) a b

First step: (λx.λy.x) a →β λy.a Second step: (λy.a) b →β a

The first argument a fills the outermost parameter x. Only after that reduction does b reach the inner parameter y.

Order Changes the Result

Consider two functions that both take arguments x and y but return different parameters:

• λx.λy.x -- returns the first argument
• λx.λy.y -- returns the second argument

Applied to the same arguments a b:

• (λx.λy.x) a b →β (λy.a) b →β a
• (λx.λy.y) a b →β (λy.y) b →β b

The body determines which argument survives, but argument order determines which argument is which. If we swapped the order of a and b, the results would also swap.

Select the First Argument

The function λx.λy.x takes two arguments and returns the first one. Reducing step by step:

1. (λx.λy.x) a b -- a fills x
2. →β (λy.a) b -- b fills y
3. →β a -- but y does not appear in the body, so b is discarded

The first argument survives. The second is ignored.

Select the Second Argument

The function λx.λy.y takes two arguments and returns the second one. Reducing step by step:

1. (λx.λy.y) a b -- a fills x
2. →β (λy.y) b -- but x does not appear in body λy.y, so a is discarded
3. →β b -- the identity function returns b

The first argument is ignored. The second argument survives.

Selectors Preview

We have seen that λx.λy.x always returns its first argument, and λx.λy.y always returns its second.

These are selectors: given two options, each one consistently picks the same position. No matter what arguments you supply, λx.λy.x selects the first and λx.λy.y selects the second.

This is not a coincidence or a toy example. Selectors turn out to be one of the most powerful patterns in lambda calculus -- they will reappear as the foundation for decisions and data structures.

Three-Argument Order

Currying extends to any number of arguments. A three-parameter function nests three abstractions:

λx.λy.λz.M

Applied to three arguments a b c, reduction proceeds from the outside in:

1. (λx.λy.λz.M) a →β λy.λz.M[x := a] -- a fills x
2. →β λz.M[x := a][y := b] -- b fills y
3. →β M[x := a][y := b][z := c] -- c fills z

The outermost parameter always receives the first argument.