Re: Version 1.1 of the bindlib package: a library for abstract syntax with binder.
 Christophe Raffalli
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Christophe Raffalli <raffalli@c...> 
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 lambdacalculus). 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