+++ /dev/null
-## Syntax 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 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/these 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
-this 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 this
-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.
-
-Here is its syntax:
-
-<blockquote>
-<strong>Variables</strong>: <code>x</code>, <code>y</code>, <code>z</code>...
-</blockquote>
-
-Each variable is an expression. For any expressions M and N and variable a, the following are also expressions:
-
-<blockquote>
-<strong>Abstract</strong>: <code>(λa M)</code>
-</blockquote>
-
-We'll tend to write <code>(λa M)</code> as just `(\a M)`, so we
-don't have to write out the markup code for the
-<code>λ</code>. You can yourself write <code>(λa
-M)</code> or `(\a M)` or `(lambda a M)`.
-
-<blockquote>
-<strong>Application</strong>: <code>(M N)</code>
-</blockquote>
-
-Expressions in the lambda calculus are called "terms". Here is the
-syntax of the lambda calculus given in the form of a context-free
-grammar:
-
- T --> Var
- T --> ( lambda Var T)
- T --> ( T T )
- Var --> x
- Var --> y
- Var --> z
- ...
-
-Very, very simple.
-
-Sometimes the first two production rules are further distinguished, and those
-are called more specifically "value terms". Whereas Applications (terms of the
-form `(M N)`) are terms but not value terms.
-
-Examples of terms:
-
- x
- (y x)
- (x x)
- (\x y)
- (\x x)
- (\x (\y x))
- (x (\x x))
- ((\x (x x)) (\x (x x)))
-
-
-## Beta-Reduction ##
-
-The lambda calculus has an associated proof theory. For now, we can regard the
-proof theory as having just one rule, called the rule of **beta-reduction** or
-"beta-contraction". Suppose you have some expression of the form:
-
- ((\a M) N)
-
-This is an application whose first element is an abstract. This
-compound form is called a **redex**, meaning it's a "beta-reducible
-expression." `(\a M)` is called the **head** of the redex; `N` is
-called the **argument**, and `M` is called the **body**.
-
-The rule of beta-reduction permits a transition from that expression to the following:
-
- M [a <-- N]
-
-What this means is just `M`, with any *free occurrences* inside `M` of
-the variable `a` replaced with the term `N` (--- "without capture", which
-we'll explain in the [[advanced notes|FIXME]]).
-
-What is a free occurrence?
-
-> Any occurrence of a variable `a` is **bound** in T when T has the form `(\a N)`.
-
-> An occurrence of a variable `a` is **bound** in T when T has the form `(\b
-N)` --- that is, with a *different* variable `b` --- just in case that
-occurrence of `a` is bound in the subexpression `N`.
-
-> When T has the form `(M N)`, any occurrences of `a` that are bound in the
-subexpression `M` are also bound in T, and so too any occurrences of `a` that
-are bound in the subexpression `N`.
-
-> An occurrence of a variable is **free** if it's not bound.
-
-For instance consider the following term `T`:
-
- (x (\x (\y (x (y z)))))
-
-The first occurrence of `x` in T is free. The `\x` we won't regard as
-containing an occurrence of `x`. The next occurrence of `x` occurs
-within a form `(\x (\y ...))` that begins with `\x`, so it is bound as well. The
-occurrence of `y` is bound; and the occurrence of `z` is free.
-
-To read further:
-
-* [[!wikipedia Free variables and bound variables]]
-
-Here's an example of beta-reduction:
-
- ((\x (y x)) z)
-
-beta-reduces to:
-
- (y z)
-
-We'll write that like this:
-
- ((\x (y x)) z) ~~> (y z)
-
-Different authors use different terminology and notation. Some authors use the term
-"contraction" for a single reduction step, and reserve the term
-"reduction" for the reflexive transitive closure of that, that is, for
-zero or more reduction steps. Informally, it seems easiest to us to
-say "reduction" for one or more reduction steps. So when we write:
-
- M ~~> N
-
-we'll mean that you can get from M to N by one or more reduction
-steps.
-
-When `M` and `N` are such that there is some common term (perhaps just one
-of those two, or perhaps a third term) that they both reduce to,
-we'll say that `M` and `N` are **beta-convertible**. We'll write that
-like this:
-
- M <~~> N
-
-More details about the notation and metatheory of
-the lambda calculus here:
-
-* [[ week2 lambda calculus fine points]]
-
-
-## Shorthand ##
-
-The grammar we gave for the lambda calculus leads to some
-verbosity. There are several informal conventions in widespread use,
-which enable the language to be written more compactly. (If you like,
-you could instead articulate a formal grammar which incorporates these
-additional conventions. Instead of showing it to you, we'll leave it
-as an exercise for those so inclined.)
-
-
-**Parentheses** Outermost parentheses around applications can be dropped. Moreover, applications will associate to the left, so `M N P` will be understood as `((M N) P)`. Finally, you can drop parentheses around abstracts, but not when they're part of an application. So you can abbreviate:
-
- (\x (x y))
-
-as:
-
- \x (x y)
-
-but you should include the parentheses in:
-
- (\x (x y)) z
-
-and:
-
- z (\x (x y))
-
-
-**Dot notation** Dot means "assume a left paren here, and the matching right
-paren as far the right as possible without creating unbalanced
-parentheses". So:
-
- \x (\y (x y))
-
-can be abbreviated as:
-
- \x (\y. x y)
-
-and that as:
-
- \x. \y. x y
-
-This:
-
- \x. \y. (x y) x
-
-abbreviates:
-
- \x (\y ((x y) x))
-
-This on the other hand:
-
- (\x. \y. (x y)) x
-
-abbreviates:
-
- ((\x (\y (x y))) x)
-
-We didn't have to insert any parentheses around the inner body of `\y. (x y)` because they were already there.
-
-
-**Merging lambdas** An expression of the form `(\x (\y M))`, or equivalently, `(\x. \y. M)`, can be abbreviated as:
-
- (\x y. M)
-
-Similarly, `(\x (\y (\z M)))` can be abbreviated as:
-
- (\x y z. M)
-
-
-## Lambda terms represent functions ##
-
-Let's pause and consider the following fundamental question: what is a
-function? One popular answer is that a function can be represented by
-a set of ordered pairs. This set is called the **graph** of the
-function. If the ordered pair `(a, b)` is a member of the graph of `f`,
-that means that `f` maps the argument `a` to the value `b`. In
-symbols, `f: a` ↦ `b`, or `f (a) == b`.
-
-In order to count as a *function* (rather
-than as merely a more general *relation*), we require that the graph not contain two
-(distinct) ordered pairs with the same first element. That is, in
-order to count as a proper function, each argument must correspond to
-a unique result.
-
-The lambda calculus seems to be wonderfully well-suited for
-representing functions. In fact, the untyped
-lambda calculus is Turing Complete (see [[!wikipedia Turing Completeness]]):
-all (recursively computable) functions can be represented by lambda
-terms. Which, by most people's lights, means that all functions we can "effectively decide" ---
-that is, compute in a mechanical way without requiring any ingenuity or insight ---
-can be represented by lambda terms. As we'll see, though, it will be fun
-(that is, not straightforward) unpacking how these things can be so "represented."
-
-For some lambda terms, it is easy to see what function they represent:
-
-> `(\x x)` represents the identity function: given any argument `M`, this function
-simply returns `M`: `((\x x) M) ~~> M`.
-
-> `(\x (x x))` duplicates its argument (applies it to itself):
-`((\x (x x)) M) ~~> (M M)` <!-- **M** or ω; W is \uv.uvv -->
-
-> `(\x (\y (y x)))` reorders its two arguments:
-`(((\x (\y (y x))) M) N) ~~> (N M)` <!-- **T**; C is \uvx.uxv -->
-
-> `(\x (\y x))` throws away its second argument:
-`(((\x (\y x)) M) N) ~~> M` <!-- **K** -->
-
-and so on. In order to get an intuitive feel for the power of the
-lambda calculus, note that duplicating, reordering, and deleting
-elements is all that it takes to simulate the behavior of a general
-word processing program. That means that if we had a big enough
-lambda term, it could take a representation of *Emma* as input and
-produce *Hamlet* as a result.
-
-Some of these functions are so useful that we'll give them special
-names. In particular, we'll call the identity function `(\x x)`
-**I**, and the function `(\x (\y x))` **K** (for "konstant": <code><b>K</b> x</code> is
-a "constant function" that accepts any second argument `y` and ignores
-it, always returning `x`).
-
-It is easy to see that distinct lambda expressions can represent the same
-function, considered as a mapping from input to outputs. Obviously:
-
- (\x x)
-
-and:
-
- (\z z)
-
-both represent the same function, the identity function. However, we said
-(FIXME in the advanced notes) that we would be regarding these expressions as
-synactically equivalent, so they aren't yet really examples of *distinct*
-lambda expressions representing a single function. However, all three of these
-are distinct lambda expressions:
-
- (\y x. y x) (\z z)
-
- (\x. (\z z) x)
-
- (\z z)
-
-yet when applied to any argument M, all of these will always return M. So they
-have the same extension. It's also true, though you may not yet be in a
-position to see, that no other function can differentiate between them when
-they're supplied as an argument to it. However, these expressions are all
-syntactically distinct.
-
-The first two expressions are (beta-)*convertible*: in particular the first
-reduces to the second via a single instance of beta reduction. So they
-can be regarded as proof-theoretically equivalent even though they're
-not syntactically identical. However, the proof theory we've given so
-far doesn't permit you to reduce the second expression to the
-third. So these lambda expressions are non-equivalent.
-
-In other words, we have here different (non-equivalent) lambda terms with the
-same extension. This introduces some tension between the popular way of
-thinking of functions as represented by (identical to?) their graphs or
-extensions, and the idea that lambda terms express functions. Well, perhaps the
-lambda terms are just a finer-grained way of expressing functions than
-extensions are?
-
-As we'll see, though, there are even further sources of
-tension between the idea of functions-as-extensions and the idea of functions
-embodied in the lambda calculus.
-
-
-1. One reason is that that general
-mathematical conception permits many *uncomputable* functions, but the
-lambda calculus can't express those.
-
-2. More problematically, some lambda terms express "functions" that can take
-themselves as arguments. If we wanted to represent that set-theoretically, and
-identified functions with their extensions, then we'd have to have some
-extension that contained (an ordered pair containing) itself as a member. Which
-we're not allowed to do in mainstream set-theory. But in the lambda calculus
-this is permitted and common --- and in fact will turn out to be indispensable.
-
- Here are some simple examples. We can apply the identity function to itself:
-
- (\x x) (\x x)
-
- This is a redex that reduces to the identity function (of course). We can
-apply the **K** function to another argument and itself:
-
- > <code><b>K</b> z <b>K</b></code>
-
- That is:
-
- (\x (\y x)) z (\x (\y x))
-
- That reduces to just `z`.
-
-3. As we'll see in coming weeks, some lambda terms will turn out to be
-impossible to associate with any extension. This is related to the previous point.
-
-
-In fact it *does* turn out to be possible to represent the Lambda Calculus
-set-theoretically. But not in the straightforward way that identifies
-functions with their graphs. For years, it wasn't known whether it would be possible to do this. But then
-[[!wikipedia Dana Scott]] figured out how to do it in late 1969, that is,
-he formulated the first "denotational semantics" for this lambda calculus.
-Scott himself had expected that this wouldn't be possible to do. He argued
-for its unlikelihood in a paper he wrote only a month before the discovery.
-
-(You can find an exposition of Scott's semantics in Chapters 15 and 16 of the
-Hindley & Seldin book we recommended, and an exposition of some simpler
-models that have since been discovered in Chapter 5 of the Hankin book, and
-Section 16F of Hindley & Seldin. But realistically, you really ought to
-wait a while and get more familiar with these systems before you'll be at all
-ready to engage with those ideas.)
-
-We've characterized the rule of beta-reduction as a kind of "proof theory" for
-the Lambda Calculus. In fact, the usual proof theory is expressed in terms of
-*convertibility* rather than in terms of reduction; but it's natural to
-understand reduction as being the conceptually more fundamental notion. And
-there are some proof theories for this system that are expressed in terms of
-reduction.
-
-To use a linguistic analogy, you can think of what we're calling
-"proof theory" as a kind of syntactic transformation. The
-sentences *John saw Mary* and *Mary was seen by John* are not
-syntactically identical, yet (on some theories) one can be derived
-from the other. The key element in the analogy is that this kind of
-syntactic derivation is supposed to preserve meaning, so that the two
-sentences mean (roughly) the same thing.
-
-There's an extension of the proof-theory we've presented so far which
-does permit a further move of just that sort. It would permit us to
-also count these functions:
-
- (\x. (\z z) x)
-
- (\z z)
-
-as equivalent. This additional move is called **eta-reduction**. It's
-crucial to eta-reduction that the outermost variable binding in the
-abstract we begin with (here, `\x`) be of a variable that occurs free
-exactly once in the body of that abstract, and that it be in the
-rightmost position.
-
-In the extended proof theory/theories we get be permitting eta-reduction/conversion
-as well as beta-reduction, *all computable functions with the same
-extension do turn out to be equivalent*, that is, convertible.
-
-However, we still shouldn't assume we're working with functions
-traditionally conceived as just sets of ordered pairs, for the other
-reasons sketched above.
-
-
-## The analogy with `let` ##
-
-In our basic functional programming language, we used `let`
-expressions to assign values to variables. For instance,
-
- let x match 2
- in (x, x)
-
-evaluates to the ordered pair (2, 2). It may be helpful to think of
-a redex in the lambda calculus as a particular sort of `let`
-construction.
-
- ((\x BODY) ARG) is analogous to
-
- let x match ARG
- in BODY
-
-This analogy should be treated with caution. For one thing, our `letrec`
-allowed us to define recursive functions in which the name `x` appeared within
-`ARG`, but we wanted it there to be bound to the very same `ARG`. We're not
-ready to deal with recursive functions in the lambda calculus yet.
-
-For another, we defined `let` in terms of *values*: we said that the variable
-`x` was bound to whatever *value* `ARG` *evaluated to*. At this point, it's
-not clear what the values are in the lambda calculus. We only have expressions.
-(Though there was a suggestive remark earlier about some of the expressions but
-not others being called "value terms".)
-
-So perhaps we should translate `((\x BODY) ARG)` in purely syntactic terms,
-like: "let `x` be replaced by `ARG` in `BODY`"?
-
-Most problematically, in the lambda
-calculus, an abstract such as `(\x (x x))` is perfectly well-formed
-and coherent, but it is not possible to write a `let` expression that
-does not have an `ARG`. That would be like:
-
- `let x match` *missing*
- `in x x`
-
-Nevertheless, the correspondence is close enough that it can guide our
-intuition.
-