The lambda-context calculus (extended version)

We present the Lambda Context Calculus. This simple lambda-calculus features variables arranged in a hierarchy of strengths such that Substitution of a strong variable does not avoid capture with respect to abstraction by a weaker variable. This allows the calculus to express both capture-avoiding and capturing substitution (instantiation). The reduction rules extend the 'vanilla' lambda-calculus in a simple and modular way and preserve the look and feel of a standard lambda-calculus with explicit substitutions. Good properties of the lambda-calculus are preserved. The LamCC is confluent, and a natural injection into the LamCC of the untyped lambda-calculus exists and preserves strong normalisation. We discuss the calculus and its design with full proofs. In the presence of the hierarchy of variables, functional binding splits into a functional abstraction lambda (lambda) and a name-binder tf (sic)(new). We investigate how the components of this calculus interact with each other and with the reduction rules, with examples. In two more extended case studies we demonstrate how global state can be expressed, and how contexts and contextual equivalence can be naturally internalised using function application. (C) 2009 Elsevier Inc. All rights reserved.