Lambda Calculus – Call by Value vs. Call by Name (Lazy Evaluation)

Python lambda expressions are real, formal untyped λ-calculus lambda expressions.

They fit the formal definition; they can only represent one python expression, based on variables (free or otherwise) and references to other functions (abstract symbols). Python uses parenthesis in expressions too.

You use them wherever a lambda is more suitable and convenient than a full function definition. The python def functionname(argumentlist): syntax forms a statement; in Python you cannot put statements inside of expressions, only the other way around. A lambda on the other hand, is an expression, so you can use a lambda to insert a callback function inline:

map(lambda x, y: x[y+5], [(mapping1, integerkey1), (mapping2, integerkey2)])

The above example consists only of an expression. The python map() function takes, as its first argument, a callable, which is applied to each and every element in the list given by the second argument. In the above example, using a lambda expression to define that callable is much easier than using a function statement:

def mapcallback(x, y):
    return x[y + 5]

map(mapcallback, [(mapping1, integerkey1), (mapping2, integerkey2)])

For the full function syntax I need to assign a name, put the function definition on separate lines, and use the return statement to return the result of the expression.

Yes, the evaluation strategy as described leads to strict semantics, and the examples are spectacularly badly chosen to conceal the difference between the two semantics. I think it goes something like this:

id (id (λz. id z))  # strict means we evaluate the right hand side
→ id (λz. id z)     # RHS has been reduced (id (λz. id z)) → (λz. id z) by inner id 
→ λz. id z          # now we have called the outer id to obtain the final value

id (id (λz. id z))  # normal form means we call the outer id and pass RHS as a closure
→ id (λz. id z)     # outer id just returned its argument unevaluated → id (λz. id z) 
→ λz. id z          # now same thing is repeated with inner id

So the derivation steps look syntactically the same, but different things are happening. Under the lazy evaluation scheme, id doesn't actually force evaluation of its argument: it simply returns that argument itself. So not only do id x and x yield the same value, but they are actually equivalent: id x really yields x itself, and then x yields its value later when actually needed. So likewise, id (id (λz. id z)) simply yields the unevaluated right hand side (id (λz. id z)).

What's confusing in the example is that it's based on nesting the same function, which is just id, such that two different reductions both yield id (λz. id z). In one this is just a copy of the inner id expression, and in the other, it's the value of the inner expression, being passed an argument to the outer id.