Date: Wed, 18 Oct 1995 09:34:04 +0100
Message-Id: <199510180834.JAA12420@lips.cs.chalmers.se>
From: Christophe Raffalli <raffalli@cs.chalmers.se>
To: cpg@cs.utexas.edu
Subject: Re: Version 1.1 of the bindlib package: a library for abstract syntax with binder.
> 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