Substitution

A[x : = N] ist (eine Kopie von) A, wobei jedes freie Vorkommen von x durch N ersetzt ist.

Definition durch strukturelle Induktion

• A ist Variable (2 Fälle)
• A ist Applikation
• A ist Abstraktion
  • (λx.B)[x : = N] = λx.B
  • (λy.B)[x : = N] = λy.(B[x : = N]), falls x≠y und ...