Alpha-Konversion

Man nennt die Formeln $(Qx.\phi )$ und $(Qz.{\phi }_{x\mapsto z})$ $\alpha$-konvertibel, falls ${\phi }_{x\mapsto z}$ dadurch gebildet wird, dass jedes freie Vorkommen der Variable $x$ durch eine unbenutzte ("frische") Variable $z$ umbenannt wird.

Zwei Formeln $\phi$ und $\psi$ gelten als $\alpha$-gleich ($\phi {=}_{\alpha }\psi$), sofern sie durch eine endliche Anzahl an Ersetzungen von $\alpha$-konvertiblen Teilformeln ineinander transformiert werden können.

Links

• FoG-2526-FS_v5.pdf
• Freie und gebundene Variablen