Basics of 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 that we will explore in some detail, is the "pure" Lambda Calculus. And actually, there are many variations even in the pure Lambda Calculus. But all of the variations share a strong family resemblance, so what we learn now will apply to all of them. The lambda calculus we'll be focusing on for the first part of the course has no types. Some prefer to say it does have types, 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. Here is its syntax:
Variables: `x`, `y`, `z`...
Each variable is an expression. For any expressions M and N and variable a, 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)`