Skip to content

Computation with the Lambda Calculus

Normal Form

  • A Term is in -normal form, iff no further reductions can be applied to it
  • It's possible to have a different ordering of the resolution, but they all lead to the normal form
  • Every -term has at most one normal form
    • That makes computation deterministic
  • Not all -terms terminate i.e. have a normal form
    • e.g.
    • Necessary to make it Turing-complete

Currying

  • -terms only allow single argument functions
  • How to implement functions with multiple Arguments?
  • Currying:
    • Apply to , which returns a function that takes
    • Apply this function to

-Reduction

  • Substitute a defined symbol with its definition
  • e.g. substituted is

Higher Order Functions

  • Functions that either takes a function as input or returns a function
  • functions are "first-class citizens"

Evaluation Strategies

  • A redex (reducible expression) is a any Delta- oder Beta-reducible lambda term
  • Strategie plays a role in the length of derivations and if they terminate
  • There are an arbitrary number of evaluation strategies
  • Innermost- and Outermost-First are "extreme" cases

Innermost-first (applicative order)

  • The innermost redex is reduced first
  • If multiple possible, the leftmost is reduced first
  • A redex is innermost if there is no other redex inside it

Outermost-first (normal order)

  • The outermost redex is reduced first
  • If multiple possible, the leftmost is reduced first
  • A redex is outermost if there is no other redex outside it

Comparison

  • innermost-first: Arguments are reduced exactly once (even if they're not used)
  • outermost-first: Arguments are reduced as often as they're needed (can be multiple times for one)
  • innermost-first doesn't always result in shorter derivations
  • Outermost-first always ends in a normal form if it exists
    • innermost-first may not terminate, e.g. when a non-terminating redux is an argument, but never used
  • innermost-first is like "call by value", outermost-first like "call by ref"

Lazy Evaluation

  • Make call-by-name more efficient
  • Cache evaluations to evaluate arguments only once
  • Default for Haskell

Encoding Data and Operations

  • Pure lambda does not have primitive data types
  • We need numbers, booleans & pairs to construct arbitrary data types
  • These definitions correspond to AND/OR-Gates on a real CPU (low-level)

Booleans

  • It's hard to have an intuition for these, try to prove some properties that must hold (truth tables)

Arithmetic

  • For every number n, apply a function n times