Substitution

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

Definition durch strukturelle Induktion

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

    falls x≠y mathend000# und BV(B)∩FV(N) = ∅ mathend000#