> excuse my ignorance, but, what do you call "bindings"?

That is a very good questions !

A binder is a constructer which binds a variable ! This means to take the
exemple of a constructor of arity one that if C is a binder then in "C(x,t)",
where "x" is the bound variable and "t" is the argument of C then "x" does not
appear as a "free" variable in "C(x,t)".

Common exemples:

>From your favorite functionnal language:

let x = expr1 in expr2 : x in bound in expr2 : let ... in is a binder
function x -> expr : x in bound in expr : function is a binder

>From mathematics:

Sum for i = 0 to n of expr : i is bound in expr

>From logic:

Forall X we have expr : X is bound in expr

I hope you see what a binding is. The problem is that each time you must
implement such a data structure, you have to make a choice to implement the
binding. Sometimes simple choices are quite ok (ex: writing a compiler),
sometimes they are inefficient or they increase too much the complexity of the
code (ex: a proof editor, a normaliser for pure lambda-calculus). It is why I
implemented my package which provides an efficient solution which results also
in simpler code.

Hope this helps.


----
Christophe Raffalli
Dept. of Computer Sciences
Chalmers University of Technology

URL: http://www.logique.jussieu.fr/www.raffalli