Here's what we did in seminar on Monday 9/13, Sometimes these notes will expand on things mentioned only briefly in class, or discuss useful tangents that didn't even make it into class. This present page expands on *a lot*, and some of this material will be reviewed next week. [Linguistic and Philosophical Applications of the Tools We'll be Studying](/applications) ========================================================================== [Explanation of the "Damn" example shown in class](/damn) Basics of Lambda Calculus ========================= The lambda calculus we'll be focusing on for the first part of the course has no types. (Some prefer to say it instead has a single type---but 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 type." 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)