Gebundene Umbenennungen

Relation →_α auf Λ:

• Axiom: (λx.B)→_α(λy.B[x : = y]) falls y $\notin$V(B).
• Abschluß unter Kontext:

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

≡_α ist die durch →_α definierte Äquivalenzrelation

(die transitive, reflexive und symmetrische Hülle von →_α)

Bsp. λx.λx.x≡_αλy.λx.x, λx.λx.x $\not\equiv$_αλy.λx.y

wir betrachten ab jetzt Λ/≡_α

(d. h., Äquivalenzklassen von Termen)

(vgl. rationale Zahlen als Äquivalenzklassen von Paaren)