Gebundene Umbenennungen

Relation →_α mathend000# auf Λ mathend000#:

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

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

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

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

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

wir betrachten ab jetzt Λ/≡_α mathend000#

(d. h., Äquivalenzklassen von Termen)

(vgl. rationale Zahlen als Äquivalenzklassen von Paaren)