| Under consideration for publication in J. Functional Programming 1 FUNCTIONAL PEARLS α-conversion is easy (2009) | |||||||||||||||
Abstract | |||||||||||||||
| We present a new and simple account of α-conversion suitable for formal reasoning. Our main tool is to define α-conversion as a a structural congruence parametrized by a partial bijection on free variables. We show a number of basic properties of substitution. e.g. that substitution is monadic which entails all the usual substitution laws. Finally, we relate α-equivalence classes to de Bruijn terms. 1 | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||