A lambda expression that can no longer be reduced is in normal form.

Not every lambda expression can be reduced to normal form! E.g., infinite loops. If all reductions terminated, then the lambda calculus would be weaker than Turing machines.

Diamond property: any reduction to a normal form gives an equivalent normal form.

Standardization Theorem

If an expression E has a normal form, than a strategy that reduces the leftmost outermost redex at each state in the reduction is guaranteed to reach that normal form.

Normal vs Applicative Order

  • Normal order corresponds to call by name
    • parameter is passed as unevaluated expression that is evaluated in the body of the function being executed each time the corresponding formal parameter is referenced. “Expand then reduce”
  • Applicative order corresponds to call by value
    • an arg to a function is evaluated before the function is applied
    • ML and Scheme are applicative order

Lazy Evaluation

Like normal order, but introduce pointer to expression (rather than copying it) and evaluate it only once, when its value is needed. Also called graph reduction.

Allows for elegant handling of infinite data structures. Used by Haskell.

When studying, practice redux formulas for different expressions! E.g., false a b = b is (define false = ($\lambda$ x. $\lambda$ y. y)).

Recursion in $\lambda$ calculus

Can’t just replace a function name with its definition to create a recursive function. Instead, define a variable that represents the function in the RHS of the equation:

define fact = $\lambda$ n. if (iszero n)
                           1
                           (* n (fact (dec n)))

becomes

define
f = $\lambda$ g . $\lambda$ n. if (iszero n) 1 (* ( g (dec n)))

fact is a fixed point of f, because fact = f (fact).

Y-Combinator

Allows recursive functions to be expressed.

Y = $\lambda$ h.($\lambdax$ x. h(x x))($\lambdax$ x. h(x x))

Important property: Y f = f (Y f)

If a function doesn’t have a fixed point, then the evaluation of Y f will not terminate. If there are multiple fixed points, we take the least fixed points.