Ableitungen

Absicht: Relation →_β auf Λ/≡_α (Ein-Schritt-Ersetzung):

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

  ein Term der Form (λx.B)A heißt Redex (= reducible expression)

• Abschluß unter Kontext:

  $${\frac{{F\to_\beta F'}}{{(F A)\to_\beta (F' A)}}}$$,  $${\frac{{A\to_\beta A'}}{{(F A)\to_\beta (F A')}}}$$,  $${\frac{{B\to_\beta B'}}{{\lambda x.B\to_\beta \lambda x.B'}}}$$

Vorsicht:

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

das freie y wird fälschlich gebunden

die Substitution ist nicht ausführbar, man muß vorher lokal umbenennen