^^Lambda explorer.

Nice! What happened here is your identity function took b as the input and spit it right back out. The process of evaluating a function like this is called beta reduction.

The result you're seeing here is in what's called normal form, which we'll also go through a little later.

Just like we can evaluate functions with variables, we can also evaluate them with other functions! Try typing (λa.a)λb.b

So we can perform beta reductions with other functions as the argument!

With that, we've just introduced the main elements of the syntax of the lambda calculus:

Variables	a₁
Applying one expression to another	a₁b₁
A lambda abstraction	λx.y
Parentheses	(λx.y)

We've also introduced a few ways in which these can be combined.

Applying one lambda expression to a variable	(λx.x)b₁
Applying one lambda expression to another	(λa.a)λb.b

It's time to solidify our understanding of how these combine syntactically. Write any expression to continue.

Repeated applications in the lambda calculus are what is called left-associative. This means that repeated applications are evaluated from left to right.

To make this clearer, if we were to explicity write out the parentheses for the expression abcd, we'd end up with ((ab)c)d. That is, in the expression abcd, a will first be applied to b, then the result of ab will be applied to c, so on and so forth.

Write out the parentheses explicitly for ijkmn

Lambda abstractions have higher prescedence than applications.

This means that if we write the expression λx.yz, it would be parenthesized as λx.(yz) and NOT (λx.y)z.

As a rule of thumb, the body of a lambda abstraction (i.e. the part of the lambda expression after the dot) extends all the way to the end of the expression unless parentheses tell it not to.

Explicitly write the parentheses around λw.xyz, combining this new knowledge with what you learned in the last question around how applications are parenthesized.

Solution: λw.((xy)z)

So what if we DID want to apply a lambda abstraction to a variable? We'd have to write it out a little more explicity, like we did back in problem 6.

For example, if we wanted to apply the lambda abstraction λx.y to variable z, we'd write it out as (λx.y)z

Write an expression that applies the lambda abstraction λa.bc to the variable d.

Fortunately, the other direction requires fewer parentheses. If we wanted to apply a variable to a lambda abstraction instead of the other way around, we'd just write them right next to each other, like any other application.

Concretely, applying a to lambda abstraction λb.c is written as aλb.c

Try applying w to λx.yz!

As you may have noticed before, functions can only take one argument, which is kind of annoying.

Let's say we quite reasonably want to write a function which takes more than one argument. Fortunately, we can sort of get around the single argument restriction by making it so that a function returns another function, which when evaluated subsequently gives you the result. Make sense?

In practice, this looks like λa.λb. [some expression]. Go ahead and write any 'multi-argument' function!