Archive for the 'Cambridge HOL' 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.

Advertisements

Five axioms of alpha-conversion

By Andrew D. Gordon and Tom Melham, from TPHOLs 1996, available from Andrew D. Gordon’s website:

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.