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'

(λx.(λy.xyx))(yy)$\;\stackrel{{?}}{{\to_\beta}}\;$(λy.yx)[x : = (yy)] = λy.y(yy)

das freie y wird fälschlich gebunden. Lösung: vorher umbenennen (später (bei Refactoring) genaueres dazu)