Redex and reduction strategies

lambda

I'm studying Types and Programming Languages, and have some trouble getting my head around the concepts of the 5th chapter, The Untyped Lambda Calculus.

Specifically, redex, reduction and the various evaluation strategies are doing my head in. The following is what I understand put into my own words, in an attempt to explain things to myself and get more knowledgeable people to correct my mistakes / imprecisions. I am honestly unsure as to whether this is an acceptable format for stackexchange, and am open to suggestions to make this a better fit.

Note that others have tried to answer a very similar question, but have still left me confused:

Redex

If my understanding is correct, a redex is a reducible expression, that is, the application of a lambda term to a lambda abstraction.

Or, more concretely, a redex is always of the form (λx.s)t.

Redex reduction

Reducing (λx.s)t is done by replacing all free occurrences of x in s by t.
For example:

(λx.x + 2) 1
→ 1 + 2
→ 3

The process of reducing a lambda expression to its normal form is driven by an evaluation strategy: an algorithm for picking which redex to reduce first. In order to describe these however, we need some more vocabulary.

Redex qualifications

Leftmost and rightmost

the leftmost redex is the one whose abstraction is textually to the left of all other redexes.
the rightmost redex is the one whose abstraction is textually to the right of all other redexes.

So, for example, in (λx.x + 2) (λy.y + 1), we have:

leftmost redex: λx.x + 2
rightmost redex: λy.y + 1

There can only be one leftmost and one rightmost redex in a given expression. I'm assuming that in an expression composed of a single redex, that redex is both the leftmost and the rightmost.

Innermost and outermost

an innermost redex is one that contains no other redex.
an outermost redex is one that is contained within no other redex.

So, for example, in (λx.(λy.y + 1) x) 2, we have:

innermost: λy.y + 1, as it contains no other redex.
outermost: λx.[...], as it isn't contained in any other redex.

I'm assuming that in an expression composed of a single redex, that redex is both outermost and innermost.

Evaluation strategies

Having defined this, we can talk about the two evaluation strategies that I'm struggling with: call by name and call by value.

Call by name

In call by name, the leftmost outermost redex is always picked for reduction. Additionally, no reduction can occur within a lambda abstraction.
The example given by Types and Programming Languages is:

id (id (λz. id z)) # the leftmost, outermost redex is the very first id
→ id (λz. id z)    # the leftmost, outermost redex is still the first id
→ λz. id z         # there is no outermost redex remaining, we're done.

I do not understand the need for the definition of the strategy to include no reduction can occur within a lambda abstraction: is that not implied by the fact that only outermost redexes are eligible for reduction?

Call by value

In call by value the rightmost outermost redex is always picked for reduction.
The example given by Types and Programming Languages is:

id (id (λz. id z)) # the rightmost, outermost redex is the second id
→ id (λz. id z)    # the rightmost, outermost redex is the first id
                   # (it's textualy on the left, but there is no redex to its right)
→ λz. id z         # the only remaining redex is not outermost (it's contained within
                   # an abstraction) and cannot be reduced.

Best Answer

In Call by name:

I do not understand the need for the definition of the strategy to include no reduction can occur within a lambda abstraction: is that not implied by the fact that only outermost redexes are eligible for reduction?

No. According to your definition of outermost, a redex is outermost if it is not contained within any other redex. In the following code, id z is the outermost redex, not λz. id z (which is an abstraction, not a redex).

id (id (λz. id z)) # the leftmost, outermost redex is the very first id
→ id (λz. id z)    # the leftmost, outermost redex is still the first id
→ λz. id z         # there is no outermost redex remaining, we're done.

Note that in the description of call by value in TAPL, there is a missing word in the definition of value:

p 57, definition of call-by-value

"a term that is finished computing..." should be "a CLOSED term that is finished computing..."

This is probably the reason for your confusion.

Edited to add: It turns out that the author's description of call-by-value is inconsistent with the operational semantics given in the book for the untyped lambda-calculus under call-by-value evaluation. According to the description of call-by-value on page 57, λx. id id would evaluate to λx. id since id is a value. (a closed term that cannot be reduced) and id id is the outermost redex. However the operational semantics (on page 72) do not have a rule that can reduce this term in this way. In addition, on the same page the author writes "Since (call-by-value) evaluation stops when it reaches a lambda, values can be arbitrary lambda-terms" suggesting that reductions are not allowed inside abstractions.

In the description of call-by-name, the author mentions that no reductions are allowed inside abstractions but neglects to do so in the description of call-by-value.

Second edit: I believe the correction that adds the word "CLOSED" to the definition of call-by-value that I mentioned above causes an inconsistency with the operational semantics. For instance, id (λx. x y) reduces to λx. x y according to the operational semantics given. (Since values are arbitrary lambda-abstractions and the rule 'E-AppAbs' applies here) However, λx. x y is not a closed term since the occurrence of y in it is not bound.

Errata for the book are available at: http://www.cis.upenn.edu/~bcpierce/tapl/errata.txt

Related Solutions

Delphi doesn’t have Lambda Expressions and I’m a Delphi programmer, what am I missing out on

Let's say in Delphi you have anonymous inline methods like the delegate in this C# code:

var squared = Enumerable.Range(0, 100)
    .Select(
         delegate(int a)
         {
             return a * a;
         }
    );

Then the lambdas are simply a shorter way of writing that:

var squared = Enumerable.Range(0, 100)
    .Select(
         a => a * a
    );

The code snippets above are identical from the IL point of view.

The difference between a function and a lambda

The word "lambda" or "lambda expressions" most often refers to anonymous functions. So in that sense a lambda is a kind of function, but not every function is a lambda (i.e. named functions aren't usually referred to as lambdas). Depending on the language, anonymous functions are often implemented differently than named functions (particularly in languages where anonymous functions are closures and named functions are not), so referring to them with different terms can make sense.

The difference between scheme's lambda keyword and Javascript's function keyword is that the latter can be used to create both anonymous functions and named functions while the former only creates anonymous functions (and you'd use define to create named functions).

The lambda calculus is a minimal programming language/mathematical model of computation, which uses functions as its only "data structure". In the lamdba calculus the lambda-symbol is used to create (anonymous) functions. This is where the usage of the term "lambda" in other languages comes from.