Umbenennung von lokalen Variablen

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

  die freien y in (yy) werden fälschlich gebunden.

• deswegen (λx.B)A→_βB[x : = A] nur, falls x $\notin$fvar(A).
• Lösung: vorher lokal umbenennen ( λy.yx→_αλz.zx)

  dann (λx.(λy.yx))(yy)→_α(λx.(λz.zx))(yy)→_βλz.z(yy)

• das falsche Binden muß auch hier verhindert werden:

  Umbenennung von x in y bei: λx.xy$\;\stackrel{{?}}{{\to_\alpha}}\;$λy.yy

• ähnlich bei Refactoring (inline method, rename variable)

autotool-Quelltexte dazu: http://autolat.imn.htwk-leipzig.de/gitweb/?p=tool;a=blob;f=collection/src/Lambda/Derive2.hs;hb=classic-via-rpc#l177