Alpha-conversion is easy

I believe that this submission was the paper mentioned by Andrew Pitts in the comments after Jordi Levy’s talk on efficient nominal unification at RTA 2010.

By Thorsten Altenkirch, unpublished Functional Pearl, available from the Haskell wiki:

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.

0 Responses to “Alpha-conversion is easy”

  1. Leave a Comment

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: