Lambda the Ultimate

I originally wrote that evaluator to try and experiment with the lambda-sigma calculus. About all I concluded was that de Bruijn indices make my brain hurt. I never could quite figure out what explicit substitution calculi were for. Do you have some insight about them?

Hi Dave! Nice work on that lambda-sigma evaluator. It needs a bit of updating to work with the latest CVS PLT Scheme, by the way.

As usual, Pierce explains the use of explicit substitution nicely. I'll try not to quote all of Ch. 6 of "Types and Programming Languages," but here's the framework:

"In the previous chapter, we worked with terms 'up to renaming of bound variables,' introducing a general convention that bound variables can be renamed, at any moment, to enable substitution or because a new name is convenient for some other reason... we must decide how occurrences of variables are to be represented. There is more than one way to do this:

1. We can represent variables symbolically as we have done so far...
2. We can represent variables symbolically, but introduce a general condition that the names of all bound variables must be different from each other and from any free variables we may use...
3. We can devise some 'canonical' representation of variables and terms that does not require renaming.
4. We can avoid substitution altogether by introducing mechanisms such as explicit substitutions (Abadi, Cardelli, Curien, and Lèvy, 1991a).
5. We can avoid variables altogether by working in a language based directly on combinators..."

Pierce goes on to observe that the book makes choice #3 as does most of the real world, apparently.

"Avoiding substitution altogether" is a worthwhile goal because, as I'm sure you're aware, substitution calculi insert a distance between a theoretical lambda calculus and its pragmatic implementation, making it hard to maintain an intuitive mapping from theory to practice, and also tends to be error prone, witness the care the PLT team put into defining a "substitution pattern language" with which to implement concrete substitution strategies in PLT-Redex.

de Bruijn indices make everyone's brain hurt, most likely including de Bruijn, which is why theoreticians write things down. It turns out there's a newish calculus of explicit substitutions, <http://formal.cs.uiuc.edu/stehr/cinni_eng.html>:

that combines names and indices in a uniform way. It contains the standard named notation used in logics and programming languages as well as de'Bruijn's indexed notation as sublanguages. CINNI is a first-order calculus of extreme simplicity that can serve as a generic basis for representing and implementing higher-order languages in a first-order framework. More precisely, CINNI should not be regarded as a single calculus but merely as a family of calculi that is parameterized by syntax of the language to be represented.

We think that CINNI is a suitable basis to deal with the problem of binding and substitution in implementations of logics and other languages, in particular those of higher-order nature. A distinctive advantage of CINNI is that it completely eliminates the problematic translation between the notation that is visible by the user of a system and the internal representation.

As concrete examples we have studied the application of CINNI to the untyped lambda calculus, the object calculus (introduced by Cardelli and Abadi) and to a rich class of typed lambda calculi, namely pure type systems, and, last but not least the proof assistant for OCC, the open calculus of constructions, makes essential use of CINNI. Since CINNI is a calculus that has an executable semantics in terms of rewriting we have indeed obtained with very moderate effort representations of these formalisms that can be executed using the Maude engine.

So here we have the tie-in to our other poster as of this writing! I personally wasn't thinking in terms of using PLT-Redex as a pre-step to working in Maude, but I was indeed thinking of <http://www.metaprl.org>, another rewriting-based theorem prover that I have installed and started working through the tutorial of.

Or should I use a lowly "DT" acronym? :)

Dependent Types and Explicit Substitutions

We present a dependent-type system for a λ-calculus with explicit substitutions. In this
system, meta-variables, as well as substitutions, are first-class objects. We show that the system enjoys
properties like type uniqueness, subject reduction, soundness, confluence and weak normalization.

3. We can devise some 'canonical' representation of variables and terms that does not require renaming.

That seems like a strange motivation, considering section 6.2 starts off as...

Our next job is defining a substitution operation ([k->s]t) on nameless terms. To do this, we need one auxiliary operation, called "shifting," which renumber the indices of the free variables in a term.

But I guess the real reason is (as Pierce states) "that it (de Brujin indicies) tends to fail catastrophically rather than subtly when it is implemented wrong, allowing mistakes to be detected and corrected sooner rather that later."