(\x. \z. z x) y
+(\x. \y. y x) y
+(\z. (\z. z z) y
+
+ (λ. λ. _ _) y
+ ^ ^  
+  __ 
+ _______
+
+
+Here there are no bound variables, but there are *bound positions*. We can regard formula like (a) and (b) as just helpfully readable ways to designate these abstract structures.
+
+A version of this last approach is known as **de Bruijn notation** for the lambda calculus.
+
+It doesn't seem to matter which of these approaches one takes; the logical properties of the systems are exactly the same. It just affects the particulars of how one states the rules for substitution, and so on. And whether one talks about expressions being literally "syntactically identical," or whether one instead counts them as "equivalent modulu alphaconversion."
+
+(Linguistic trivia: however, some linguistic discussions do suppose that alphabetic variance has important linguistic consequences; see Ivan Sag's dissertation.)
+
+In a bit, we'll discuss other systems that lack variables. Those systems will not just lack variables in the sense that de Bruijn notation does; they will furthermore lack any notion of a bound position.
+
+
Syntactic equality, reduction, convertibility
=============================================
Define T to be `(\x. x y) z`. Then T and `(\x. x y) z` are syntactically equal, and we're counting them as syntactically equal to `(\z. z y) z` as well. We write:
+Define N to be `(\x. x y) z`. Then N and `(\x. x y) z` are syntactically equal, and we're counting them as syntactically equal to `(\z. z y) z` as well, which we will write as:
T ≡ `(\x. x y) z` ≡ `(\z. z y) z` +
N ≡ (\x. x y) z ≡ (\z. z y) z
+
This:
T ~~> `z y` + N ~~> z y means that T betareduces to `z y`. This: +means that N betareduces to `z y`. This: 
M <~~> T + M <~~> N means that M and T are betaconvertible, that is, that there's something they both reduce to in zero or more steps. +means that M and N are betaconvertible, that is, that there's something they both reduce to in zero or more steps. Combinators and Combinatorial Logic =================================== Lambda expressions that have no free variables are known as **combinators**. Here are some common ones: 
**I** is defined to be `\x x`+> **I** is defined to be `\x x` It's possible to build a logical system equally powerful as the lambda calculus (and straightforwardly intertranslatable with it) using just combinators, considered as atomic operations. Such a language doesn't have any variables in it: not just no free variables, but no variables at all. +> **K** is defined to be `\x y. x`. That is, it throws away its + second argument. So `K x` is a constant function from any + (further) argument to `x`. ("K" for "constant".) Compare K + to our definition of `true`. One can do that with a very spare set of basic combinators. These days the standard base is just three combinators: K and I from above, and also one more, S, which behaves the same as the lambda expression `\f g x. f x (g x)`. behaves.But it's possible to be even more minimalistic, and get by with only a single combinator. (And there are different singlecombinator bases you can choose.) +> **getfirst** was our function for extracting the first element of an ordered pair: `\fst snd. fst`. Compare this to K and `true` as well. These systems are Turing complete. In other words: every computation we know how to describe can be represented in a logical system consisting of only a single primitive operation! +> **getsecond** was our function for extracting the second element of an ordered pair: `\fst snd. snd`. Compare this to our definition of `false`. Here's more to read about combinatorial logic: +> **B** is defined to be: `\f g x. f (g x)`. (So `B f g` is the composition `\x. f (g x)` of `f` and `g`.) MORE +> **C** is defined to be: `\f x y. f y x`. (So `C f` is a function like `f` except it expects its first two arguments in swapped order.) Evaluation strategies ===================== +> **W** is defined to be: `\f x . f x x`. (So `W f` accepts one argument and gives it to `f` twice. What is the meaning of `W multiply`?) In the assignment we asked you to reduce various expressions until it wasn't possible to reduce them any further. For two of those expressions, this was impossible to do. One of them was this: +> **ω** (that is, lowercase omega) is defined to be: `\x. x x`  (\x. x x) (\x. x x) +It's possible to build a logical system equally powerful as the lambda calculus (and readily intertranslatable with it) using just combinators, considered as atomic operations. Such a language doesn't have any variables in it: not just no free variables, but no variables at all. As we saw above, each of the halves of this formula are the combinator ω; so this can also be written: +One can do that with a very spare set of basic combinators. These days the standard base is just three combinators: K and I from above, and also one more, **S**, which behaves the same as the lambda expression `\f g x. f x (g x)`. behaves. But it's possible to be even more minimalistic, and get by with only a single combinator. (And there are different singlecombinator bases you can choose.) **K** is defined to be `\x y. x`, That is, it throws away its second argument. So `K x` is a constant function from any (further) argument to `x`. ("K" for "constant".) Compare K to our definition of **true**.
**getfirst** was our function for extracting the first element of an ordered pair: `\fst snd. fst`. Compare this to K and true as well.
**getsecond** was our function for extracting the second element of an ordered pair: `\fst snd. snd`. Compare this to our definition of false.
**ω** is defined to be: `\x. x x`

ω ω
+There are some wellknown linguistic applications of Combinatory
+Logic, due to Anna Szabolcsi, Mark Steedman, and Pauline Jacobson.
+They claim that natural language semantics is a combinatory system: that every
+natural language denotation is a combinator.
This compound expressionthe selfapplication of ωis named Ω. It has the form of an application of an abstract (ω) to an argument (which also happens to be ω), so it's a redex and can be reduced. But when we reduce it, we get ω ω
again. So there's no stage at which this expression has been reduced to a point where it can't be reduced any further. In other words, evaluation of this expression "never terminates." (This is standard language, however it has the unfortunate connotation that evaluation is a process or operation that is performed in time. You shouldn't think of it like that. Evaluation of this expression "never terminates" in the way that the decimal expansion of π never terminates. This are static, atemporal facts about their mathematical properties.)
+For instance, Szabolcsi argues that reflexive pronouns are argument
+duplicators.
There are infinitely many formulas in the lambda calculus that have this same property. Ω is the syntactically simplest of them. In our metatheory, it's common to assign such formula a special value, ⊥
, pronounced "bottom." When we get to discussing types, you'll see that this value is counted as belonging to every type. To say that a formula has the bottom value means that the computation that formula represents never terminates and so doesn't evaluate to any orthodox value.
+![reflexive](http://lambda.jimpryor.net/szabolcsireflexive.jpg)
From a "Fregean" or "weak Kleene" perspective, if any component of an expression fails to be evaluable (to an orthodox, computed value), then the whole expression should be unevaluable as well.
+Notice that the semantic value of *himself* is exactly `W`.
+The reflexive pronoun in direct object position combines with the transitive verb. The result is an intransitive verb phrase that takes a subject argument, duplicates that argument, and feeds the two copies to the transitive verb meaning.
However, in some such cases it seems *we could* sensibly carry on evaluation. For instance, consider:
+Note that `W <~~> S(CI)`:

(\x. y) (ω ω)

+S(CI) ≡
+S((\fxy.fyx)(\x.x)) ~~>
+S(\xy.(\x.x)yx) ~~>
+S(\xy.yx) ≡
+(\fgx.fx(gx))(\xy.yx) ~~>
+\gx.(\xy.yx)x(gx) ~~>
+\gx.(gx)x ≡
+W
Should we count this as unevaluable, because the reduction of ω ω
never terminates? Or should we count it as evaluating to `y`?
+Ok, here comes a shift in thinking. Instead of defining combinators as equivalent to certain lambda terms,
+we can define combinators by what they do. If we have the I combinator followed by any expression X,
+I will take that expression as its argument and return that same expression as the result. In pictures,
This question highlights that there are different choices to make about how evaluation or computation proceeds. It's helpful to think of three questions in this neighborhood:
+ IX ~~> X
> Q1. When arguments are complex, as ω ω
, do we reduce them before or after substituting them into the abstracts to which they are arguments?
+Thinking of this as a reduction rule, we can perform the following computation
> Q2. Are we allowed to reduce inside abstracts? That is, can we reduce:
+ II(IX) ~~> IIX ~~> IX ~~> X
> (\x y. x z) (\x. x)
+The reduction rule for K is also straightforward:
> only this far:
+ KXY ~~> X
> \y. (\x. x) z
+That is, K throws away its second argument. The reduction rule for S can be constructed by examining
+the defining lambda term:
> or can we continue reducing to:
+S ≡ \fgx.fx(gx)
> \y. z
+S takes three arguments, duplicates the third argument, and feeds one copy to the first argument and the second copy to the second argument. So:
> Q3. Are we allowed to "etareduce"? That is, can we reduce expressions of the form:
+ SFGX ~~> FX(GX)
> \x. M x
+If the meaning of a function is nothing more than how it behaves with respect to its arguments,
+these reduction rules capture the behavior of the combinators S, K, and I completely.
+We can use these rules to compute without resorting to beta reduction. For instance, we can show how the I combinator is equivalent to a certain crafty combination of Ss and Ks:
> where x does not occur free in `M`, to `M`? It should be intuitively clear that `\x. M x` and `M` will behave the same with respect to any arguments they are given. It can also be proven that no other functions can behave differently with respect to them. However, the logical system you get when etareduction is added to the proof theory is importantly different from the one where only betareduction is permitted.
+ SKKX ~~> KX(KX) ~~> X
+So the combinator `SKK` is equivalent to the combinator I.
The evaluation strategy which answers Q1 by saying "reduce arguments first" is known as **callbyvalue**. The evaluation strategy which answers Q1 by saying "substitute arguments in unreduced" is known as **callbyname** or **callbyneed** (the difference between these has to do with efficiency, not semantics).
+Combinatory Logic is what you have when you choose a set of combinators and regulate their behavior with a set of reduction rules. As we said, the most common system uses S, K, and I as defined here.
When one has a callbyvalue strategy that also permits reduction to continue inside unapplied abstracts, that's known as "applicative order" reduction. When one has a callbyname stratehy that oermits reduction inside abstracts, that's known as "normal order" reduction. Consider an expression of the form:
+###The equivalence of the untyped lambda calculus and combinatory logic###
 ((A B) (C D)) (E F)
+We've claimed that Combinatory Logic is equivalent to the lambda calculus. If that's so, then S, K, and I must be enough to accomplish any computational task imaginable. Actually, S and K must suffice, since we've just seen that we can simulate I using only S and K. In order to get an intuition about what it takes to be Turing complete, imagine what a text editor does:
+it transforms any arbitrary text into any other arbitrary text. The way it does this is by deleting, copying, and reordering characters. We've already seen that K deletes its second argument, so we have deletion covered. S duplicates and reorders, so we have some reason to hope that S and K are enough to define arbitrary functions.
Its syntax has the following tree:
+We've already established that the behavior of combinatory terms can be perfectly mimicked by lambda terms: just replace each combinator with its equivalent lambda term, i.e., replace I with `\x.x`, replace K with `\fxy.x`, and replace S with `\fgx.fx(gx)`. How about the other direction? Here is a method for converting an arbitrary lambda term into an equivalent Combinatory Logic term using only S, K, and I. Besides the intrinsic beauty of this mapping, and the importance of what it says about the nature of binding and computation, it is possible to hear an echo of computing with continuations in this conversion strategy (though you wouldn't be able to hear these echos until we've covered a considerable portion of the rest of the course).
 ((A B) (C D)) (E F)
 / \
 / \
((A B) (C D)) \
 /\ (E F)
 / \ /\
 / \ E F
(A B) (C D)
 /\ /\
/ \ / \
A B C D
+Assume that for any lambda term T, [T] is the equivalent combinatory logic term. The we can define the [.] mapping as follows:
Applicative order evaluation does what's called a "postorder traversal" of the tree: that is, we always go left and down whenever we can, and we process a node only after processing all its children. So `(C D)` gets processed before `((A B) (C D))` does, and `(E F)` gets processed before `((A B) (C D)) (E F)` does.
+ 1. [a] a
+ 2. [(M N)] ([M][N])
+ 3. [\a.a] I
+ 4. [\a.M] KM assumption: a does not occur free in M
+ 5. [\a.(M N)] S[\a.M][\a.N]
+ 6. [\a\b.M] [\a[\b.M]]
Normal order evaluation, on the other hand, will substitute the expresion `(C D)` into the abstract that `(A B)` evaluates to, without first trying to compute what `(C D)` evaluates to. That computation may be done later.
+It's easy to understand these rules based on what S, K and I do. The first rule says
+that variables are mapped to themselves.
+The second rule says that the way to translate an application is to translate the
+first element and the second element separately.
+The third rule should be obvious.
+The fourth rule should also be fairly selfevident: since what a lambda term such as `\x.y` does it throw away its first argument and return `y`, that's exactly what the combinatory logic translation should do. And indeed, `Ky` is a function that throws away its argument and returns `y`.
+The fifth rule deals with an abstract whose body is an application: the S combinator takes its next argument (which will fill the role of the original variable a) and copies it, feeding one copy to the translation of \a.M, and the other copy to the translation of \a.N. This ensures that any free occurrences of a inside M or N will end up taking on the appropriate value. Finally, the last rule says that if the body of an abstract is itself an abstract, translate the inner abstract first, and then do the outermost. (Since the translation of [\b.M] will not have any lambdas in it, we can be sure that we won't end up applying rule 6 again in an infinite loop.)
When we have an expression like:
+[Fussy notes: if the original lambda term has free variables in it, so will the combinatory logic translation. Feel free to worry about this, though you should be confident that it makes sense. You should also convince yourself that if the original lambda term contains no free variablesi.e., is a combinatorthen the translation will consist only of S, K, and I (plus parentheses). One other detail: this translation algorithm builds expressions that combine lambdas with combinators. For instance, the translation of our boolean false `\x.\y.y` is `[\x[\y.y]] = [\x.I] = KI`. In the intermediate stage, we have `\x.I`, which mixes combinators in the body of a lambda abstract. It's possible to avoid this if you want to, but it takes some careful thought. See, e.g., Barendregt 1984, page 156.]
 (\x. y) (C D)
+[Various, slightly differing translation schemes from combinatorial logic to the lambda calculus are also possible. These generate different metatheoretical correspondences between the two calculii. Consult Hindley and Seldin for details. Also, note that the combinatorial proof theory needs to be strengthened with axioms beyond anything we've here described in order to make [M] convertible with [N] whenever the original lambdaterms M and N are convertible.]
the computation of `(C D)` won't ever have to be performed, on a normal order or call by name evaluation strategy. Instead, that reduces directly to `y`. This is so even if `(C D)` is the nonevaluable (ω ω)
!
Most programming languages, including Scheme and OCaml, use the callbyvalue evaluation strategy. (But they don't permit evaluation to continue inside an unappplied function.) There are techniques for making them model the other sort of behavior.
+Let's check that the translation of the false boolean behaves as expected by feeding it two arbitrary arguments:
Some functional programming languages, such as Haskell, use the callbyname evaluation strategy. Each has pros and cons.
+ KIXY ~~> IY ~~> Y
The lambda calculus can be evaluated either way. You have to decide what the rules shall be.
+Throws away the first argument, returns the second argumentyep, it works.
One important advantage of the normalorder evaluation strategy is that it can compute an orthodox value for:
+Here's a more elaborate example of the translation. The goal is to establish that combinators can reverse order, so we use the **T** combinator, where T ≡ \x\y.yx
:

(\x. y) (ω ω)

+ [\x\y.yx] = [\x[\y.yx]] = [\x.S[\y.y][\y.x]] = [\x.(SI)(Kx)] = S[\x.SI][\x.Kx] = S(K(SI))(S[\x.K][\x.x]) = S(K(SI))(S(KK)I)
Indeed, it's provable that if there's any reduction path that delivers a value for an expression, the normalorder evalutation strategy will terminate with that value.
+We can test this translation by seeing if it behaves like the original lambda term does.
+The orginal lambda term lifts its first argument (think of it as reversing the order of its two arguments):
An expression is said to be in **normal form** when it's not possible to perform any more reductions. (EVEN INSIDE ABSTRACTS?) There's a sense in which you can't get anything more out of ω ω
, but it's not in normal form because it still has the form of a redex.
+ S(K(SI))(S(KK)I) X Y ~~>
+ (K(SI))X ((S(KK)I) X) Y ~~>
+ SI ((KK)X (IX)) Y ~~>
+ SI (KX) Y ~~>
+ IY (KXY) ~~>
+ Y X
A computational system is said to be **confluent**, or to have the **ChurchRosser** or **diamond** property, if, whenever there are multiple possible evaluation paths, those that terminate always terminate in the same value. In such a system, the choice of which subexpressions to evaluate first will only matter if some of them but not others might lead down a nonterminating path.
+Voilà: the combinator takes any X and Y as arguments, and returns Y applied to X.
The untyped lambda calculus is confluent. So long as a computation terminates, it always terminates in the same way. It doesn't matter which order the subexpressions are evaluated in.
+One very nice property of combinatory logic is that there is no need to worry about alphabetic variance, or
+variable collisionsince there are no (bound) variables, there is no possibility of accidental variable capture,
+and so reduction can be performed without any fear of variable collision. We haven't mentioned the intricacies of
+alpha equivalence or safe variable substitution, but they are in fact quite intricate. (The best way to gain
+an appreciation of that intricacy is to write a program that performs lambda reduction.)
A computational system is said to be **strongly normalizing** if every permitted evaluation path is guaranteed to terminate. The untyped lambda calculus is not strongly normalizing: ω ω
doesn't terminate by any evaluation path; and (\x. y) (ω ω)
terminates only by some evaluation paths but not by others.
+Back to linguistic applications: one consequence of the equivalence between the lambda calculus and combinatory
+logic is that anything that can be done by binding variables can just as well be done with combinators.
+This has given rise to a style of semantic analysis called Variable Free Semantics (in addition to
+Szabolcsi's papers, see, for instance,
+Pauline Jacobson's 1999 *Linguistics and Philosophy* paper, "Towards a variablefree Semantics").
+Somewhat ironically, reading strings of combinators is so difficult that most practitioners of variablefree semantics
+express their meanings using the lambdacalculus rather than combinatory logic; perhaps they should call their
+enterprise Free Variable Free Semantics.
But the untyped lambda calculus enjoys some compensation for this weakness. It's Turing complete! It can represent any computation we know how to describe. (That's the cash value of being Turing complete, not the rigorous definition. We don't know how to rigorously define "any computation we know how to describe." There is however a rigorous definition for being Turing complete.) And in fact, it's been proven that you can't havee both. If a language is Turing complete, it cannot be strongly normalizing.
+A philosophical connection: Quine went through a phase in which he developed a variable free logic.
A computational system is said to be **weakly normalizing** if there's always guaranteed to be *at least one* evaluation path that terminates. The untyped lambda calculus is not weakly normalizing either, as we've seen.
+ Quine, Willard. 1960. "Variables explained away" Proceedings of the American Philosophical Society. Volume 104: 343347. Also in W. V. Quine. 1960. Selected Logical Papers. Random House: New
+ York. 227235.
The *typed* lambda calculus that linguists traditionally work with, on the other hand, is strongly normalizing. (And as a result, is not Turning complete.) It has expressive power that the untyped lambda calculus lacks, but it is also unable to represent some (terminating!) computations that the untyped lambda calculus can represent.
+The reason this was important to Quine is similar to the worries that Jim was talking about
+in the first class in which using nonreferring expressions such as Santa Claus might commit
+one to believing in nonexistant things. Quine's slogan was that "to be is to be the value of a variable."
+What this was supposed to mean is that if and only if an object could serve as the value of some variable, we
+are committed to recognizing the existence of that object in our ontology.
+Obviously, if there ARE no variables, this slogan has to be rethought.
Other morepowerful type systems we'll look at in the course will also fail to be Turing complete, though they will turn out to be pretty powerful.
+Quine did not appear to appreciate that Shoenfinkel had already invented combinatory logic, though
+he later wrote an introduction to Shoenfinkel's key paper reprinted in Jean
+van Heijenoort (ed) 1967 From Frege to Goedel, a source book in mathematical logic, 18791931.
+Cresswell has also developed a variablefree approach of some philosophical and linguistic interest
+in two books in the 1990's.
+A final linguistic application: Steedman's Combinatory Categorial Grammar, where the "Combinatory" is
+from combinatory logic (see especially his 2000 book, The Syntactic Processs). Steedman attempts to build
+a syntax/semantics interface using a small number of combinators, including T ≡ `\xy.yx`, B ≡ `\fxy.f(xy)`,
+and our friend S. Steedman used Smullyan's fanciful bird
+names for the combinators, Thrush, Bluebird, and Starling.
+Many of these combinatory logics, in particular, the SKI system,
+are Turing complete. In other words: every computation we know how to describe can be represented in a logical system consisting of only a single primitive operation!
+Here's more to read about combinatorial logic.
+Surely the most entertaining exposition is Smullyan's [[!wikipedia To_Mock_a_Mockingbird]].
+Other sources include
+* [[!wikipedia Combinatory logic]] at Wikipedia
+* [Combinatory logic](http://plato.stanford.edu/entries/logiccombinatory/) at the Stanford Encyclopedia of Philosophy
+* [[!wikipedia SKI combinatory calculus]]
+* [[!wikipedia B,C,K,W system]]
+* [Chris Barker's Iota and Jot](http://semarch.linguistics.fas.nyu.edu/barker/Iota/)
+* Jeroen Fokker, "The Systematic Construction of a Onecombinator Basis for LambdaTerms" Formal Aspects of Computing 4 (1992), pp. 776780.
+ω
; so this can also be written:
We'll write that like this:
+ω ω
 ((\x (y x)) z) ~~> (y z)
+This compound expressionthe selfapplication of ω
is named Ω. It has the form of an application of an abstract (ω
) to an argument (which also happens to be ω
), so it's a redex and can be reduced. But when we reduce it, we get ω ω
again. So there's no stage at which this expression has been reduced to a point where it can't be reduced any further. In other words, evaluation of this expression "never terminates." (This is the standard language, however it has the unfortunate connotation that evaluation is a process or operation that is performed in time. You shouldn't think of it like that. Evaluation of this expression "never terminates" in the way that the decimal expansion of π never terminates. These are static, atemporal facts about their mathematical properties.)
Different authors use different notations. 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:
+There are infinitely many formulas in the lambda calculus that have this same property. Ω is the syntactically simplest of them. In our metatheory, it's common to assign such formulas a special value, ⊥
, pronounced "bottom." When we get to discussing types, you'll see that this value is counted as belonging to every type. To say that a formula has the bottom value means that the computation that formula represents never terminates and so doesn't evaluate to any orthodox, computed value.
 M ~~> N
+From a "Fregean" or "weak Kleene" perspective, if any component of an expression fails to be evaluable (to an orthodox, computed value), then the whole expression should be unevaluable as well.
We'll mean that you can get from M to N by one or more reduction steps. Hankin uses the symbol →
for onestep contraction, and the symbol ↠
for zeroormore step reduction. Hindley and Seldin use ⊳_{1}
and ⊳
.
+However, in some such cases it seems *we could* sensibly carry on evaluation. For instance, consider:
When M and N are such that there's some P that M reduces to by zero or more steps, and that N also reduces to by zero or more steps, then we say that M and N are **betaconvertible**. We'll write that like this:
+
+(\x. y) (ω ω)
+
 M <~~> N
+Should we count this as unevaluable, because the reduction of (ω ω)
never terminates? Or should we count it as evaluating to `y`?
+
+This question highlights that there are different choices to make about how evaluation or computation proceeds. It's helpful to think of three questions in this neighborhood:
+
+> Q1. When arguments are complex, as (ω ω)
is, do we reduce them before substituting them into the abstracts to which they are arguments, or later?
+
+> Q2. Are we allowed to reduce inside abstracts? That is, can we reduce:
+
+> (\x y. x z) (\x. x)
+
+> only this far:
This is what plays the role of equality in the lambda calculus. Hankin uses the symbol `=` for this. So too do Hindley and Seldin. Personally, I keep confusing that with the relation to be described next, so let's use this notation instead. Note that `M <~~> N` doesn't mean that each of `M` and `N` are reducible to each other; that only holds when `M` and `N` are the same expression. (Or, with our convention of only saying "reducible" for one or more reduction steps, it never holds.)
+> \y. (\x. x) z
In the metatheory, it's also sometimes useful to talk about formulas that are syntactically equivalent *before any reductions take place*. Hankin uses the symbol ≡
for this. So too do Hindley and Seldin. We'll use that too, and will avoid using `=` when discussing the metatheory. Instead we'll use `<~~>` as we said above. When we want to introduce a stipulative definition, we'll write it out longhand, as in:
+> or can we continue reducing to:
+> \y. z
combinators as lambda expressions
combinatorial logic
+> Q3. Are we allowed to "etareduce"? That is, can we reduce expressions of the form:
tuples = possibly typeheterogenous ordered collections, different length > different type
lists = typehomogenous ordered collections, lists of different lengths >=0 can be of same type
+> \x. M x
+> where x does not occur free in `M`, to `M`?
+With regard to Q3, it should be intuitively clear that `\x. M x` and `M` will behave the same with respect to any arguments they are given. It can also be proven that no other functions can behave differently with respect to them. However, the logical system you get when etareduction is added to the proof theory is importantly different from the one where only betareduction is permitted.
+If we answer Q2 by permitting reduction inside abstracts, and we also permit etareduction, then where none of y_{1}, ..., y_{n}
occur free in M, this:
1. Substitution; using alphaconversion and other strategies
1. Conversion versus reduction

1. Different evaluation strategies (call by name, call by value, etc.)
1. Strongly normalizing vs weakly normalizing vs nonnormalizing; ChurchRosser Theorem(s)
1. Lambda calculus compared to combinatorial logic1. Churchlike encodings of numbers, defining addition and multiplication 1. Defining the predecessor function; alternate encodings for the numbers 1. Homogeneous sequences or "lists"; how they differ from pairs, triples, etc. 1. Representing lists as pairs 1. Representing lists as folds 1. Typical higherorder functions: map, filter, fold
1. Recursion exploiting the foldlike representation of numbers and lists ([[!wikipedia Deforestation (computer science)]], [[!wikipedia Zipper (data structure)]]) 1. General recursion using omega +
\x y_{1}... y_{n}. M y_{1}... y_{n}
1. Eta reduction and "extensionality" ??
Undecidability of equivalence
+will etareduce by n steps to:
There is no algorithm which takes as input two lambda expressions and outputs TRUE or FALSE depending on whether or not the two expressions are equivalent. This was historically the first problem for which undecidability could be proven. As is common for a proof of undecidability, the proof shows that no computable function can decide the equivalence. Church's thesis is then invoked to show that no algorithm can do so.
+ \x. M
Church's proof first reduces the problem to determining whether a given lambda expression has a normal form. A normal form is an equivalent expression which cannot be reduced any further under the rules imposed by the form. Then he assumes that this predicate is computable, and can hence be expressed in lambda calculus. Building on earlier work by Kleene and constructing a GÃ¶del numbering for lambda expressions, he constructs a lambda expression e which closely follows the proof of GÃ¶del's first incompleteness theorem. If e is applied to its own GÃ¶del number, a contradiction results.
+When we add etareduction to our proof system, we end up reconstruing the meaning of `~~>` and `<~~>` and "normal form", all in terms that permit etareduction as well. Sometimes these expressions will be annotated to indicate whether only betareduction is allowed (~~>_{β}
) or whether both beta and etareduction is allowed (~~>_{βη}
).
+The logical system you get when etareduction is added to the proof system has the following property:
+> if `M`, `N` are normal forms with no free variables, then M ≡ N
iff `M` and `N` behave the same with respect to every possible sequence of arguments.
1. The Y combinator(s); more on evaluation strategies
1. Introducing the notion of a "continuation", which technique we'll now already have used a few times
+This implies that, when `M` and `N` are (closed normal forms that are) syntactically distinct, there will always be some sequences of arguments L_{1}, ..., L_{n}
such that:
+
M L_{1} ... L_{n} x y ~~> x
+N L_{1} ... L_{n} x y ~~> y
+
+So closed betaplusetanormal forms will be syntactically different iff they yield different values for some arguments. That is, iff their extensions differ.
alphaconvertible
+So the proof theory with etareduction added is called "extensional," because its notion of normal form makes syntactic identity of closed normal forms coincide with extensional equivalence.
syntactic equality `===`
contract/reduce/`~~>`
convertible `<~~>`
+See Hindley and Seldin, Chapters 78 and 14, for discussion of what should count as capturing the "extensionality" of these systems, and some outstanding issues.
normalizing
 weakly normalizable
 strongly normalizable
 "normal order" reduction vs "applicative order"
 eval strategy choices

 Reduction strategies For more details on this topic, see Evaluation
 strategy.

 Whether a term is normalising or not, and how much work needs to be
 done in normalising it if it is, depends to a large extent on the reduction
 strategy used. The distinction between reduction strategies relates to the
 distinction in functional programming languages between eager evaluation and
 lazy evaluation.

 Full beta reductions Any redex can be reduced at any time. This means
 essentially the lack of any particular reduction strategyâwith regard to
 reducibility, "all bets are off". Applicative order The leftmost, innermost
 redex is always reduced first. Intuitively this means a function's arguments
 are always reduced before the function itself. Applicative order always
 attempts to apply functions to normal forms, even when this is not possible.
 Most programming languages (including Lisp, ML and imperative languages like C
 and Java) are described as "strict", meaning that functions applied to
 nonnormalising arguments are nonnormalising. This is done essentially using
 applicative order, call by value reduction (see below), but usually called
 "eager evaluation". Normal order The leftmost, outermost redex is always
 reduced first. That is, whenever possible the arguments are substituted into
 the body of an abstraction before the arguments are reduced. Call by name As
 normal order, but no reductions are performed inside abstractions. For example
 Î»x.(Î»x.x)x is in normal form according to this strategy, although it contains
 the redex (Î»x.x)x. Call by value Only the outermost redexes are reduced: a
 redex is reduced only when its right hand side has reduced to a value (variable
 or lambda abstraction). Call by need As normal order, but function applications
 that would duplicate terms instead name the argument, which is then reduced
 only "when it is needed". Called in practical contexts "lazy evaluation". In
 implementations this "name" takes the form of a pointer, with the redex
 represented by a thunk.

 Applicative order is not a normalising strategy. The usual
 counterexample is as follows: define Î© = ÏÏ where Ï = Î»x.xx. This entire
 expression contains only one redex, namely the whole expression; its reduct is
 again Î©. Since this is the only available reduction, Î© has no normal form
 (under any evaluation strategy). Using applicative order, the expression KIÎ© =
 (Î»xy.x) (Î»x.x)Î© is reduced by first reducing Î© to normal form (since it is the
 leftmost redex), but since Î© has no normal form, applicative order fails to
 find a normal form for KIÎ©.

 In contrast, normal order is so called because it always finds a
 normalising reduction if one exists. In the above example, KIÎ© reduces under
 normal order to I, a normal form. A drawback is that redexes in the arguments
 may be copied, resulting in duplicated computation (for example, (Î»x.xx)
 ((Î»x.x)y) reduces to ((Î»x.x)y) ((Î»x.x)y) using this strategy; now there are two
 redexes, so full evaluation needs two more steps, but if the argument had been
 reduced first, there would now be none).

 The positive tradeoff of using applicative order is that it does not
 cause unnecessary computation if all arguments are used, because it never
 substitutes arguments containing redexes and hence never needs to copy them
 (which would duplicate work). In the above example, in applicative order
 (Î»x.xx) ((Î»x.x)y) reduces first to (Î»x.xx)y and then to the normal order yy,
 taking two steps instead of three.

 Most purely functional programming languages (notably Miranda and its
 descendents, including Haskell), and the proof languages of theorem provers,
 use lazy evaluation, which is essentially the same as call by need. This is
 like normal order reduction, but call by need manages to avoid the duplication
 of work inherent in normal order reduction using sharing. In the example given
 above, (Î»x.xx) ((Î»x.x)y) reduces to ((Î»x.x)y) ((Î»x.x)y), which has two redexes,
 but in call by need they are represented using the same object rather than
 copied, so when one is reduced the other is too.




 Strict evaluation Main article: strict evaluation

 In strict evaluation, the arguments to a function are always evaluated
 completely before the function is applied.

 Under Church encoding, eager evaluation of operators maps to strict evaluation
 of functions; for this reason, strict evaluation is sometimes called "eager".
 Most existing programming languages use strict evaluation for functions. [edit]
 Applicative order

 Applicative order (or leftmost innermost) evaluation refers to an evaluation
 strategy in which the arguments of a function are evaluated from left to right
 in a postorder traversal of reducible expressions (redexes). Unlike
 callbyvalue, applicative order evaluation reduces terms within a function
 body as much as possible before the function is applied. [edit] Call by value

 Callbyvalue evaluation (also referred to as passbyvalue) is the most common
 evaluation strategy, used in languages as different as C and Scheme. In
 callbyvalue, the argument expression is evaluated, and the resulting value is
 bound to the corresponding variable in the function (frequently by copying the
 value into a new memory region). If the function or procedure is able to assign
 values to its parameters, only its local copy is assigned â that is, anything
 passed into a function call is unchanged in the caller's scope when the
 function returns.

 Callbyvalue is not a single evaluation strategy, but rather the family of
 evaluation strategies in which a function's argument is evaluated before being
 passed to the function. While many programming languages (such as Eiffel and
 Java) that use callbyvalue evaluate function arguments lefttoright, some
 evaluate functions and their arguments righttoleft, and others (such as
 Scheme, OCaml and C) leave the order unspecified (though they generally require
 implementations to be consistent).

 In some cases, the term "callbyvalue" is problematic, as the value which is
 passed is not the value of the variable as understood by the ordinary meaning
 of value, but an implementationspecific reference to the value. The
 description "callbyvalue where the value is a reference" is common (but
 should not be understood as being callbyreference); another term is
 callbysharing. Thus the behaviour of callbyvalue Java or Visual Basic and
 callbyvalue C or Pascal are significantly different: in C or Pascal, calling
 a function with a large structure as an argument will cause the entire
 structure to be copied, potentially causing serious performance degradation,
 and mutations to the structure are invisible to the caller. However, in Java or
 Visual Basic only the reference to the structure is copied, which is fast, and
 mutations to the structure are visible to the caller. [edit] Call by reference

 In callbyreference evaluation (also referred to as passbyreference), a
 function receives an implicit reference to the argument, rather than a copy of
 its value. This typically means that the function can modify the argument
 something that will be seen by its caller. Callbyreference therefore has the
 advantage of greater time and spaceefficiency (since arguments do not need to
 be copied), as well as the potential for greater communication between a
 function and its caller (since the function can return information using its
 reference arguments), but the disadvantage that a function must often take
 special steps to "protect" values it wishes to pass to other functions.

 Many languages support callbyreference in some form or another, but
 comparatively few use it as a default; Perl and Visual Basic are two that do,
 though Visual Basic also offers a special syntax for callbyvalue parameters.
 A few languages, such as C++ and REALbasic, default to callbyvalue, but offer
 special syntax for callbyreference parameters. C++ additionally offers
 callbyreferencetoconst. In purely functional languages there is typically
 no semantic difference between the two strategies (since their data structures
 are immutable, so there is no possibility for a function to modify any of its
 arguments), so they are typically described as callbyvalue even though
 implementations frequently use callbyreference internally for the efficiency
 benefits.

 Even among languages that don't exactly support callbyreference, many,
 including C and ML, support explicit references (objects that refer to other
 objects), such as pointers (objects representing the memory addresses of other
 objects), and these can be used to effect or simulate callbyreference (but
 with the complication that a function's caller must explicitly generate the
 reference to supply as an argument). [edit] Call by sharing

 Also known as "call by object" or "call by objectsharing" is an evaluation
 strategy first named by Barbara Liskov et al. for the language CLU in 1974[1].
 It is used by languages such as Python[2], Iota, Java (for object
 references)[3], Ruby, Scheme, OCaml, AppleScript, and many other languages.
 However, the term "call by sharing" is not in common use; the terminology is
 inconsistent across different sources. For example, in the Java community, they
 say that Java is passbyvalue, whereas in the Ruby community, they say that
 Ruby is passbyreference, even though the two languages exhibit the same
 semantics. Callbysharing implies that values in the language are based on
 objects rather than primitive types.

 The semantics of callbysharing differ from callbyreference in that
 assignments to function arguments within the function aren't visible to the
 caller (unlike byreference semantics)[citation needed]. However since the
 function has access to the same object as the caller (no copy is made),
 mutations to those objects within the function are visible to the caller, which
 differs from callbyvalue semantics.

 Although this term has widespread usage in the Python community, identical
 semantics in other languages such as Java and Visual Basic are often described
 as callbyvalue, where the value is implied to be a reference to the object.
 [edit] Call by copyrestore

 Callbycopyrestore, callbyvalueresult or callbyvaluereturn (as termed
 in the Fortran community) is a special case of callbyreference where the
 provided reference is unique to the caller. If a parameter to a function call
 is a reference that might be accessible by another thread of execution, its
 contents are copied to a new reference that is not; when the function call
 returns, the updated contents of this new reference are copied back to the
 original reference ("restored").

 The semantics of callbycopyrestore also differ from those of
 callbyreference where two or more function arguments alias one another; that
 is, point to the same variable in the caller's environment. Under
 callbyreference, writing to one will affect the other; callbycopyrestore
 avoids this by giving the function distinct copies, but leaves the result in
 the caller's environment undefined (depending on which of the aliased arguments
 is copied back first).

 When the reference is passed to the callee uninitialized, this evaluation
 strategy may be called callbyresult. [edit] Partial evaluation Main article:
 Partial evaluation

 In partial evaluation, evaluation may continue into the body of a function that
 has not been applied. Any subexpressions that do not contain unbound variables
 are evaluated, and function applications whose argument values are known may be
 reduced. In the presence of sideeffects, complete partial evaluation may
 produce unintended results; for this reason, systems that support partial
 evaluation tend to do so only for "pure" expressions (expressions without
 sideeffects) within functions. [edit] Nonstrict evaluation

 In nonstrict evaluation, arguments to a function are not evaluated unless they
 are actually used in the evaluation of the function body.

 Under Church encoding, lazy evaluation of operators maps to nonstrict
 evaluation of functions; for this reason, nonstrict evaluation is often
 referred to as "lazy". Boolean expressions in many languages use lazy
 evaluation; in this context it is often called short circuiting. Conditional
 expressions also usually use lazy evaluation, albeit for different reasons.
 [edit] Normal order

 Normalorder (or leftmost outermost) evaluation is the evaluation strategy
 where the outermost redex is always reduced, applying functions before
 evaluating function arguments. It differs from callbyname in that
 callbyname does not evaluate inside the body of an unapplied
 function[clarification needed]. [edit] Call by name

 In callbyname evaluation, the arguments to functions are not evaluated at all
 â rather, function arguments are substituted directly into the function body
 using captureavoiding substitution. If the argument is not used in the
 evaluation of the function, it is never evaluated; if the argument is used
 several times, it is reevaluated each time. (See Jensen's Device.)

 Callbyname evaluation can be preferable over callbyvalue evaluation because
 callbyname evaluation always yields a value when a value exists, whereas
 callbyvalue may not terminate if the function's argument is a nonterminating
 computation that is not needed to evaluate the function. Opponents of
 callbyname claim that it is significantly slower when the function argument
 is used, and that in practice this is almost always the case as a mechanism
 such as a thunk is needed. [edit] Call by need

 Callbyneed is a memoized version of callbyname where, if the function
 argument is evaluated, that value is stored for subsequent uses. In a "pure"
 (effectfree) setting, this produces the same results as callbyname; when the
 function argument is used two or more times, callbyneed is almost always
 faster.

 Because evaluation of expressions may happen arbitrarily far into a
 computation, languages using callbyneed generally do not support
 computational effects (such as mutation) except through the use of monads and
 uniqueness types. This eliminates any unexpected behavior from variables whose
 values change prior to their delayed evaluation.

 This is a kind of Lazy evaluation.

 Haskell is the most wellknown language that uses callbyneed evaluation.

 R also uses a form of callbyneed. [edit] Call by macro expansion

 Callbymacroexpansion is similar to callbyname, but uses textual
 substitution rather than captureavoiding substitution. With uncautious use,
 macro substitution may result in variable capture and lead to undesired
 behavior. Hygienic macros avoid this problem by checking for and replacing
 shadowed variables that are not parameters.




 Eager evaluation or greedy evaluation is the evaluation strategy in most
 traditional programming languages.

 In eager evaluation an expression is evaluated as soon as it gets bound to a
 variable. The term is typically used to contrast lazy evaluation, where
 expressions are only evaluated when evaluating a dependent expression. Eager
 evaluation is almost exclusively used in imperative programming languages where
 the order of execution is implicitly defined by the source code organization.

 One advantage of eager evaluation is that it eliminates the need to track and
 schedule the evaluation of expressions. It also allows the programmer to
 dictate the order of execution, making it easier to determine when
 subexpressions (including functions) within the expression will be evaluated,
 as these subexpressions may have sideeffects that will affect the evaluation
 of other expressions.

 A disadvantage of eager evaluation is that it forces the evaluation of
 expressions that may not be necessary at run time, or it may delay the
 evaluation of expressions that have a more immediate need. It also forces the
 programmer to organize the source code for optimal order of execution.

 Note that many modern compilers are capable of scheduling execution to better
 optimize processor resources and can often eliminate unnecessary expressions
 from being executed entirely. Therefore, the notions of purely eager or purely
 lazy evaluation may not be applicable in practice.



 In computer programming, lazy evaluation is the technique of delaying a
 computation until the result is required.

 The benefits of lazy evaluation include: performance increases due to avoiding
 unnecessary calculations, avoiding error conditions in the evaluation of
 compound expressions, the capability of constructing potentially infinite data
 structures, and the capability of defining control structures as abstractions
 instead of as primitives.

 Languages that use lazy actions can be further subdivided into those that use a
 callbyname evaluation strategy and those that use callbyneed. Most
 realistic lazy languages, such as Haskell, use callbyneed for performance
 reasons, but theoretical presentations of lazy evaluation often use
 callbyname for simplicity.

 The opposite of lazy actions is eager evaluation, sometimes known as strict
 evaluation. Eager evaluation is the evaluation behavior used in most
 programming languages.

 Lazy evaluation refers to how expressions are evaluated when they are passed as
 arguments to functions and entails the following three points:[1]

 1. The expression is only evaluated if the result is required by the calling
 function, called delayed evaluation.[2] 2. The expression is only evaluated to
 the extent that is required by the calling function, called shortcircuit
 evaluation. 3. The expression is never evaluated more than once, called
 applicativeorder evaluation.[3]

 Contents [hide]

 * 1 Delayed evaluation
 o 1.1 Control structures
 * 2 Controlling eagerness in lazy languages 3 Other uses 4 See also 5
 * References 6 External links

 [edit] Delayed evaluation

 Delayed evaluation is used particularly in functional languages. When using
 delayed evaluation, an expression is not evaluated as soon as it gets bound to
 a variable, but when the evaluator is forced to produce the expression's value.
 That is, a statement such as x:=expression; (i.e. the assignment of the result
 of an expression to a variable) clearly calls for the expression to be
 evaluated and the result placed in x, but what actually is in x is irrelevant
 until there is a need for its value via a reference to x in some later
 expression whose evaluation could itself be deferred, though eventually the
 rapidlygrowing tree of dependencies would be pruned in order to produce some
 symbol rather than another for the outside world to see.
 Some programming languages delay evaluation of expressions by default, and some
 others provide functions or special syntax to delay evaluation. In Miranda and
 Haskell, evaluation of function arguments is delayed by default. In many other
 languages, evaluation can be delayed by explicitly suspending the computation
 using special syntax (as with Scheme's "delay" and "force" and OCaml's "lazy"
 and "Lazy.force") or, more generally, by wrapping the expression in a thunk.
 The object representing such an explicitly delayed evaluation is called a
 future or promise. Perl 6 uses lazy evaluation of lists, so one can assign
 infinite lists to variables and use them as arguments to functions, but unlike
 Haskell and Miranda, Perl 6 doesn't use lazy evaluation of arithmetic operators
 and functions by default.
+The evaluation strategy which answers Q1 by saying "reduce arguments first" is known as **callbyvalue**. The evaluation strategy which answers Q1 by saying "substitute arguments in unreduced" is known as **callbyname** or **callbyneed** (the difference between these has to do with efficiency, not semantics).
 Delayed evaluation has the advantage of being able to create calculable
 infinite lists without infinite loops or size matters interfering in
 computation. For example, one could create a function that creates an infinite
 list (often called a stream) of Fibonacci numbers. The calculation of the nth
 Fibonacci number would be merely the extraction of that element from the
 infinite list, forcing the evaluation of only the first n members of the list.
+When one has a callbyvalue strategy that also permits reduction to continue inside unapplied abstracts, that's known as "applicative order" reduction. When one has a callbyname strategy that permits reduction inside abstracts, that's known as "normal order" reduction. Consider an expression of the form:
 For example, in Haskell, the list of all Fibonacci numbers can be written as
+ ((A B) (C D)) (E F)
 fibs = 0 : 1 : zipWith (+) fibs (tail fibs)
+Its syntax has the following tree:
 In Haskell syntax, ":" prepends an element to a list, tail returns a list
 without its first element, and zipWith uses a specified function (in this case
 addition) to combine corresponding elements of two lists to produce a third.
+ ((A B) (C D)) (E F)
+ / \
+ / \
+ ((A B) (C D)) \
+ /\ (E F)
+ / \ /\
+ / \ E F
+ (A B) (C D)
+ /\ /\
+ / \ / \
+ A B C D
 Provided the programmer is careful, only the values that are required to
 produce a particular result are evaluated. However, certain calculations may
 result in the program attempting to evaluate an infinite number of elements;
 for example, requesting the length of the list or trying to sum the elements of
 the list with a fold operation would result in the program either failing to
 terminate or running out of memory. [edit] Control structures
+Applicative order evaluation does what's called a "postorder traversal" of the tree: that is, we always go down when we can, first to the left, and we process a node only after processing all its children. So `(C D)` gets processed before `((A B) (C D))` does, and `(E F)` gets processed before `((A B) (C D)) (E F)` does.
 Even in most eager languages if statements evaluate in a lazy fashion.
+Normal order evaluation, on the other hand, will substitute the expresion `(C D)` into the abstract that `(A B)` evaluates to, without first trying to compute what `(C D)` evaluates to. That computation may be done later.
 if a then b else c
+With normalorder evaluation (or callbyname more generally), if we have an expression like:
 evaluates (a), then if and only if (a) evaluates to true does it evaluate (b),
 otherwise it evaluates (c). That is, either (b) or (c) will not be evaluated.
 Conversely, in an eager language the expected behavior is that
+ (\x. y) (C D)
 define f(x,y) = 2*x set k = f(e,5)
+the computation of `(C D)` won't ever have to be performed. Instead, `(\x. y) (C D)` reduces directly to `y`. This is so even if `(C D)` is the nonevaluable (ω ω)
!
 will still evaluate (e) and (f) when computing (k). However, userdefined
 control structures depend on exact syntax, so for example
+Callbyname evaluation is often called "lazy." Callbyvalue evaluation is also often called "eager" or "strict". Some authors say these terms all have subtly different technical meanings, but I haven't been able to figure out what it is. Perhaps the technical meaning of "strict" is what I above called the "Fregean" or "weak Kleene" perspective: if any argument of a function is nonevaluable or nonnormalizing, so too is the application of the function to that argument.
 define g(a,b,c) = if a then b else c l = g(h,i,j)
 (i) and (j) would both be evaluated in an eager language. While in
+Most programming languages, including Scheme and OCaml, use the callbyvalue evaluation strategy. (But they don't permit evaluation to continue inside an unappplied function.) There are techniques for making them model callbyname evaluation, when necessary. But by default, arguments will always be evaluated before being bound to the parameters (the `\x`s) of a function.
 l' = if h then i else j
+For languages like Scheme that permit functions to take more than one argument at a time, a further question arises: whether the multiple arguments are evaluated lefttoright, or righttoleft, or nothing is guaranteed about what order they are evaluated in. Different languages make different choices about this.
 (i) or (j) would be evaluated, but never both.
+Some functional programming languages, such as Haskell, use the callbyname evaluation strategy.
 Lazy evaluation allows control structures to be defined normally, and not as
 primitives or compiletime techniques. If (i) or (j) have side effects or
 introduce run time errors, the subtle differences between (l) and (l') can be
 complex. As most programming languages are Turingcomplete, it is of course
 possible to introduce lazy control structures in eager languages, either as
 builtins like C's ternary operator ?: or by other techniques such as clever
 use of lambdas, or macros.
+The lambda calculus can be evaluated either way. You have to decide what the rules shall be.
 Shortcircuit evaluation of Boolean control structures is sometimes called
 "lazy". [edit] Controlling eagerness in lazy languages
+As we'll see in several weeks, there are techniques for *forcing* callbyvalue evaluation of a computation, and also techniques for forcing callbyname evaluation. If you liked, you could even have a nested hierarchy, where blocks at each level were forced to be evaluated in alternating ways.
 In lazy programming languages such as Haskell, although the default is to
 evaluate expressions only when they are demanded, it is possible in some cases
 to make code more eagerâor conversely, to make it more lazy again after it has
 been made more eager. This can be done by explicitly coding something which
 forces evaluation (which may make the code more eager) or avoiding such code
 (which may make the code more lazy). Strict evaluation usually implies
 eagerness, but they are technically different concepts.
+Callbyvalue and callbyname have different pros and cons.
 However, there is an optimisation implemented in some compilers called
 strictness analysis, which, in some cases, allows the compiler to infer that a
 value will always be used. In such cases, this may render the programmer's
 choice of whether to force that particular value or not, irrelevant, because
 strictness analysis will force strict evaluation.
+One important advantage of normalorder evaluation in particular is that it can compute orthodox values for:
 In Haskell, marking constructor fields strict means that their values will
 always be demanded immediately. The seq function can also be used to demand a
 value immediately and then pass it on, which is useful if a constructor field
 should generally be lazy. However, neither of these techniques implements
 recursive strictnessâfor that, a function called deepSeq was invented.
++ +Indeed, it's provable that if there's *any* reduction path that delivers a value for a given expression, the normalorder evalutation strategy will terminate with that value. + +An expression is said to be in **normal form** when it's not possible to perform any more reductions (not even inside abstracts). +There's a sense in which you *can't get anything more out of*+(\x. y) (ω ω)
+\z. (\x. y) (ω ω) +
ω ω
, but it's not in normal form because it still has the form of a redex.
+
+A computational system is said to be **confluent**, or to have the **ChurchRosser** or **diamond** property, if, whenever there are multiple possible evaluation paths, those that terminate always terminate in the same value. In such a system, the choice of which subexpressions to evaluate first will only matter if some of them but not others might lead down a nonterminating path.
 Also, pattern matching in Haskell 98 is strict by default, so the ~ qualifier
 has to be used to make it lazy. [edit]
+The untyped lambda calculus is confluent. So long as a computation terminates, it always terminates in the same way. It doesn't matter which order the subexpressions are evaluated in.
+
+A computational system is said to be **strongly normalizing** if every permitted evaluation path is guaranteed to terminate. The untyped lambda calculus is not strongly normalizing: ω ω
doesn't terminate by any evaluation path; and (\x. y) (ω ω)
terminates only by some evaluation paths but not by others.
+But the untyped lambda calculus enjoys some compensation for this weakness. It's Turing complete! It can represent any computation we know how to describe. (That's the cash value of being Turing complete, not the rigorous definition. There is a rigrous definition. However, we don't know how to rigorously define "any computation we know how to describe.") And in fact, it's been proven that you can't have both. If a computational system is Turing complete, it cannot be strongly normalizing.
+A computational system is said to be **weakly normalizing** if there's always guaranteed to be *at least one* evaluation path that terminates. The untyped lambda calculus is not weakly normalizing either, as we've seen.
+
+The *typed* lambda calculus that linguists traditionally work with, on the other hand, is strongly normalizing. (And as a result, is not Turing complete.) It has expressive power (concerning types) that the untyped lambda calculus lacks, but it is also unable to represent some (terminating!) computations that the untyped lambda calculus can represent.
+Other morepowerful type systems we'll look at in the course will also fail to be Turing complete, though they will turn out to be pretty powerful.
confluence/ChurchRosser
+Further reading:
+* [[!wikipedia Evaluation strategy]]
+* [[!wikipedia Eager evaluation]]
+* [[!wikipedia Lazy evaluation]]
+* [[!wikipedia Strict programming language]]
+* [[!wikipedia ChurchRosser theorem]]
+* [[!wikipedia Normalization property]]
+* [[!wikipedia Turing completeness]]
"combinators", useful ones:
+Decidability
+============
composition
nary[sic] composition
"foldbased"[sic] representation of numbers
defining some operations, not yet predecessor
 iszero,succ,add,mul,...?
+The question whether two formulas are syntactically equal is "decidable": we can construct a computation that's guaranteed to always give us the answer.
lists?
 explain differences between list and tuple (and stream)
 FIFO queue,LIFO stack,etc...
"pairbased" representation of lists (1,2,3)
nil,cons,isnil,head,tail
+What about the question whether two formulas are convertible? Well, to answer that, we just need to reduce them to normal form, if possible, and check whether the results are syntactically equal. The crux is that "if possible." Some computations can't be reduced to normal form. Their evaluation paths never terminate. And if we just kept trying blindly to reduce them, our computation of what they're convertible to would also never terminate.
explain operations like "map","filter","fold_left","fold_right","length","reverse"
but we're not yet in position to implement them because we don't know how to recurse
+So it'd be handy to have some way to check in advance whether a formula has a normal form: whether there's any evaluation path for it that terminates.
Another way to do lists is based on model of how we did numbers
"foldbased" representation of lists
One virtue is we can do some recursion by exploiting the foldbased structure of our implementation; don't (yet) need a general method for recursion
+Is it possible to do that? Sure, sometimes. For instance, check whether the formula is syntactically equal to Ω. If it is, it never terminates.
Go back to numbers, how to do predecessor? (a few ways)
For some purposes may be easier (to program,more efficient) to use "pairbased" representation of numbers
("More efficient" but these are still base1 representations of numbers!)
In this case, too you'd need a general method for recursion
(You could also have a hybrid, pairandfold based representation of numbers, and a hybrid, pairandfold based representation of lists. Works quite well.)
+But is there any method for doing this in generalfor telling, of any given computation, whether that computation would terminate? Unfortunately, there is not. Church proved this in 1936; Turing also essentially proved it at the same time. Geoff Pullum gives a very readerfriendly outline of the proofs here:
Recursion
Even if we have foldbased representation of numbers, and predecessor/equal/subtraction, some recursive functions are going to be out of our reach
Need a general method, where f(n) doesn't just depend on f(n1) (or