Archive for the 'Alpha-conversion' Category

Five axioms of alpha-conversion

Again, sorry for the delay in updates to the site.  I handed in my thesis this morning, so updates should now become much more frequent.

By Andrew D. Gordon and Tom Melham, from TPHOLs 1996, available from CiteSeer X:

We present five axioms of name-carrying lambda-terms identified up to alpha-conversion—that is, up to renaming of bound variables. We assume constructors for constants, variables, application and lambda-abstraction. Other constants represent a function Fv that returns the set of free variables in a term and a function that substitutes a term for a variable free in another term. Our axioms are (1) equations relating Fv and each constructor, (2) equations relating substitution and each constructor, (3) alpha-conversion itself, (4) unique existence of functions on lambda-terms defined by structural iteration, and (5) construction of lambda-abstractions given certain functions from variables to terms. By building a model from de Bruijn’s nameless lambda-terms, we show that our five axioms are a conservative extension of HOL. Theorems provable from the axioms include distinctness, injectivity and an exhaustion principle for the constructors, principles of structural induction and primitive recursion on lambda-terms, Hindley and Seldin’s substitution lemmas and the existence of their length function. These theorems and the model have been mechanically checked in the Cambridge HOL system.

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.