Ableitungen

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

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

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

• Abschluß unter Kontext:

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

Vorsicht:

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

das freie y mathend000# wird fälschlich gebunden

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