Archive for the 'Lambda-calculus' 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

Monadic presentations of untyped lambda-terms using inductive datatypes

By Thorsten Altenkirch and Bernhard Reus, from CSL 1999, available from Thorsten Altenkirch’s website:

We present a definition of untyped lambda-terms using a heterogeneous datatype, i.e. an inductively defined operator. This operator can be extended a Kleisli triple, which is a concise way to verify the substitution laws for lambda-calculus. We also observe that repetitions in the definition of the monad as well as in the proofs can be avoided by using well-founded recursion and induction instead of structural induction. We extend the construction to the simply typed lambda-calculus using dependent types, and show that this is an instance of a generalisation of Kleisli triples. The proofs for the untyped case have been checked using the LEGO system.

Efficient lambda-evaluation with interaction nets

I was informed of this paper on a trip to the University of Sussex just before Christmas.  Unfortunately, it’s taken me a while to get around to reading it, and therefore posting it to the blog.  The paper’s of interest not only to those who are interested in name binding, where interaction nets appear to provide a graphical representation of lambda-terms (and much more), but also those interested in implementing rewrite systems, wherein interaction nets facilitate a very efficient implementation.

By Ian Mackie, from RTA 2004, available from SpringerLink:

This paper presents an efficient implementation of the lambda-calculus using the graph rewriting formalism of interaction nets. Building upon a series of previous works, we obtain one of the most efficient implementations of this kind to date: out performing existing interaction net implementations, as well as other approaches. We conclude the paper with extensive testing to demonstrate the capabilities of this evaluator.

Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables

By Murdoch J. Gabbay and Dominic P. Mulligan, from LFMTP 2009, available from Murdoch J. Gabbay’s website:

This paper develops the correspondence between equality reasoning with axioms using λ-terms syntax, and reasoning using nominal terms syntax. Both syntaxes involve name-abstraction: λ-terms represent functional abstraction; nominal terms represent atomsabstraction in nominal sets.

It is not evident how to relate the two syntaxes because their intended denotations are so different. We use universal algebra, the logic of equational reasoning, a logical foundation based on an equality judgement form which is spartan but which is sufficiently expressive to encode mathematics in theory and practice.

We investigate how syntax, algebraic theories, and derivability relate across λ-theories (algebra over λ-terms) and nominal algebra theories.

Proof pearl: de Bruijn terms really do work

By Michael Norrish and Rene Vestergaard, from TPHOLs 2007, available from Michael Norrish’s website:

Placing our result in a web of related mechanised results, we give a direct proof that the de Bruijn λ-calculus (a la Huet, Nipkow and Shankar) is isomorphic to an α-quotiented λ-calculus. In order to establish the link, we introduce an “index-carrying” abstraction mechanism over de Bruijn terms, and consider it alongside a simplified substitution mechanism. Relating the new notions to those of the α-quotiented and the proper
de Bruijn formalisms draws on techniques from the theory of nominal sets.

Slides from a related presentation are available here.

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.