From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.6.10/8.6.6) id PAA28543 for caml-redistribution; Wed, 18 Oct 1995 15:05:45 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.6.10/8.6.6) with ESMTP id JAA20629 for ; Wed, 18 Oct 1995 09:34:02 +0100 Received: from margaux.inria.fr (margaux.inria.fr [128.93.8.2]) by concorde.inria.fr (8.6.10/8.6.9) with ESMTP id JAA21408 for ; Wed, 18 Oct 1995 09:34:01 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by margaux.inria.fr (8.6.10/8.6.6) with ESMTP id JAA26191 for ; Wed, 18 Oct 1995 09:34:01 +0100 Received: from lips.cs.chalmers.se (raffalli@lips.cs.chalmers.se [129.16.225.31]) by concorde.inria.fr (8.6.10/8.6.9) with ESMTP id JAA21404 for ; Wed, 18 Oct 1995 09:34:00 +0100 Received: (from raffalli@localhost) by lips.cs.chalmers.se (8.6.11/8.6.9) id JAA12420; Wed, 18 Oct 1995 09:34:04 +0100 Date: Wed, 18 Oct 1995 09:34:04 +0100 Message-Id: <199510180834.JAA12420@lips.cs.chalmers.se> From: Christophe Raffalli To: cpg@cs.utexas.edu CC: caml-list@margaux.inria.fr In-reply-to: <199510172303.SAA01637@tofu.cs.utexas.edu> (cpg@cs.utexas.edu) Subject: Re: Version 1.1 of the bindlib package: a library for abstract syntax with binder. Sender: weis > 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