# Introduction to the Lambda Calculus # We often talk about "*the* Lambda Calculus", as if there were just one; but in fact, there are many, many variations. The one we will start with, and will explore in some detail, is often called "the pure" or "the untyped" Lambda Calculus. Actually, there are many variations even under that heading. But all of the variations share a strong family resemblance, so what we learn now will apply to all of them. > Fussy note: calling this the "pure" Lambda Calculus is entrenched terminology, but it coheres imperfectly with other uses of "pure" we'll encounter. There are three respects in which the lambda calculus we'll be presenting might claim to deserve the name "pure": (1) it has no pre-defined constants and a very spare syntax; (2) it has no types; (3) it has no side-effects, and is insensitive to the order of evaluation. > Sense (3) corresponds most closely to the other uses of "pure" you'll see in the surrounding literature. With respect to this point, it may be true that the Lambda Calculus has no side effects. (Let's revisit that assumption at the end of term.) But as we'll see next week, it is *not* true that it's insensitive to the order of evaluation. So if that's what we mean by "pure", this lambda calculus isn't as pure as you might hope to get. Some *typed* lambda calculi will turn out to be more pure in that respect. > But this lambda calculus is at least "pure" in sense (2). At least, it doesn't *explicitly talk about* any types. Some prefer to say that the Lambda Calculus *does* have types implicitly, it's just that there's only one type, so that every expression is a member of that one type. If you say that, you have to say that functions from this type to this type also belong to this type. Which is weird... In fact, though, such types are studied, under the name "recursive types." More about these later in the seminar. > Well, at least this lambda calculus is "pure" in sense (1). As we'll see next week, though, there are some computational formal systems whose syntax is *even more* spare, in that they don't even have variables. So if that's what mean by "pure", again this lambda calculus isn't as pure as you might hope to get. > Still, if you say you're talking about "the pure" Lambda Calculus, or "the untyped" Lambda Calculus, or even just "the" Lambda Calculus, this is the system that people will understand you to be referring to. ## Syntax ## Here is its syntax:
Variables: x, y, z ...
Each variable is an expression. For any variable `a` and (possibly complex) expressions `M` and `N`, the following are also expressions:
Abstract: (λa M)
We'll tend to write (λa M) as just `(\a M)`, so we don't have to write out the markup code for the λ. You can yourself write (λa M) or `(\a M)` or `(lambda a M)`.
Application: (M N)