A New Approach to Abstract Syntax with Variable Binding

Pitts and Gabbay, A New Approach to Abstract Syntax with Variable Binding, FAC 2001.

In the lambda calculus, the particular choice of variable names - even free variables - is irrelevant. Names serve two purposes:

as mnemonics to help human readers understand their role, and
to distinguish variables that are meant to be different and unify variables that are meant to be the same.

In a theory of binders, only the latter purpose is relevant. This is why it's so annoying to have to deal with capture-avoiding substitution, the Barendregt variable convention, gensym, and the like. These are all ways of getting around the fact that we've committed to a particular name when we really shouldn't have cared what the name was.

There are several standard ways to deal with this. Generating fresh names with gensym is awkward and forces the implementer to reimplement binding and substitution from scratch for each new object language; not to mention its violation of referential transparency. de Bruijn indices remove the variable names but are hard to read and understand. Higher-order abstract syntax implements binders in the object language as functions in the metalanguage, in order to reuse the built-in mechanisms of binding and substitution; but by mixing higher-order values in algebraic datatypes, structural induction is hard to recover.

This paper introduces a theory of fresh names that restores algebraic reasoning, referential transparency, and structural induction to algebraic datatypes with a HOAS-like notation for introducing binders into an abstract syntax. This is the set-theoretical basis for the authors' work on FreshML and FreshO'Caml, which we've discussed a little bit on LtU in the past.

This paper is excellent, read it!

...if only to see what alpha equivalence and structural induction have to do with denying the truth of the axiom of choice. Beautiful, nonobvious, well-motivated work that really succeeds in making things simpler, and is rich in connections with all kinds of other topics. What theory should be about.

By Charles A Stewart at Tue, 2005-03-15 15:00 | login or register to post comments

Quibble

if only to see what alpha equivalence and structural induction have to do with denying the truth of the axiom of choice

I agree that this is an interesting paper, but I have to take exception with your wording regarding the AC.

First of all, the authors simply point out that the AC is inconsistent with the FM(A) set theory they are using, which is no surprise since that theory was used to prove the independence of the AC from the other ZF axioms.

Secondly, it is obvious that any computational process bound by the limits of Turing Completeness cannot properly avail itself of the AC, since the AC allows that you can select any item or subset of items from an infinite set in finite time.

In this sense, all computer science in necessarily constructivist, even if I'm sure some cheat now and again. ;-)

By Marc Hamann at Tue, 2005-03-15 21:15 | login or register to post comments

I think what I said was right....

The key point is that if you want to represent terms by sets, then structural induction (which might need to be over uncomputable objects) isn't a special case of epsilon induction if you have AC (I hope what I wrote is right). But in FM set theory it all works.

By Charles A Stewart at Wed, 2005-03-16 18:28 | login or register to post comments

Prior art

As an aside to this, there was something very familiar about this trick with atoms as "variables".

Then it struck me that in Vicious Circles, Barwise and Moss had a similar trick for similar reasons, but in a different set theory (Aczel's anti-founded set theory).

They use atoms as bound variables representing a "solution" to an anti-founded set structure.

IIRC, in that context, AC was NOT inconsistent with the rest of the axioms; you could use it or not.

By Marc Hamann at Wed, 2005-03-16 20:07 | login or register to post comments

...and NF too

Then it struck me that in Vicious Circles, Barwise and Moss had a similar trick for similar reasons, but in a different set theory (Aczel's anti-founded set theory).

Sort of similar, but not as simple: AFA is based upon ideas like coinduction and bisimilarity. What FM set theory gives you is structural induction on the nose for terms up to alpha equivalence by plain old simple epsilon induction.

A third sort of set theory for doing these sorts of tricks is to use stratified set theory in the vein of Quine's New Foundations. Essentially, where the hereditarilly finite sets of ZFC are finite trees where no node has two equal children and all leaves are empty sets, the hereditarilly finite sets of NF are these sorts of trees but leaves may also be the whole universe. Every set is a subset of the universe, which can be handy for parametricity tricks.

I doubt that it's much of a coincidence that Andrew Pitts, Jamie Gabbay's supervisor, and Thomas Forster, author of "Set Theory with a Universal Set" are both members of Cambridge Computer Science theory group...

By Charles A Stewart at Wed, 2005-03-16 22:46 | login or register to post comments

Mugshots

...as well as a very brief introduction to some ideas of ZF: Zermelo-Fraenkel Set Theory

[on edit: a more organised info on Non-well-founded set theory]

By Andris Birkmanis at Thu, 2005-03-17 08:42 | login or register to post comments

I will have to read it...

...so that I can compare and contrast with CINNI - A Calculus of Indexed Names and Named Indices, which is where my current focus on issues of names and binding lies. I like that CINNI is executable in terms of rewriting; this suggests that it should be possible to implement in terms of PLT Redex, Maude as they have already done, or MetaPRL, which I would prefer because they seem to have gone farthest in implementing a full-on "language designer's workbench."

By Paul Snively at Tue, 2005-03-15 21:15 | login or register to post comments

Lambda the Ultimate

User login

Navigation