Semantik des Lambda-Kalküls

Relation →_β auf Λ (ein Reduktionsschritt)

• Reduktion (λx.B)A→_βB[x : = A] (Vorsicht)

  Kopie von B, jedes freie Vorkommen von x durch A ersetzt

• ...eines beliebigen Teilterms:
  • F→_βF'⇒(FA)→_β(F'A)
  • A→_βA'⇒(FA)→_β(FA')
  • B→_βB'⇒λx.B→_βλx.B'

in autotool-Aufgabe: Position des Teilterms angeben, in welchem reduziert werden soll.