Linear Contexts and the Sharing Functor: Techniques for Symbolic Computation Export

@inproceedings{citeulike:169628, abstract = {We present in this paper two design issues concerning fundamental representation structures for symbolic and logic computations. The first one concerns structured editing, or more generally the possibly destructive update of tree-like data-structures of inductive types. Instead of the standard implementation of mutable data structures containing references, we advocate the zipper technology, fully applicative. This may be considered a disciplined use of pointer reversal techniques. We argue that zippers, i.e. unary contexts generalizing stacks, are concrete representations of linear functions on algebraic data types. The second method is a uniform sharing functor, which is a variation on the traditional technique of hashing, but controling the indexing function on the client side rather than on the server side, which allows the fine-tuning of bucket balancing, taking into account specific statistical properties of the application data. Such techniques are of general interest for symbolic computation applications such as structure editors, proof assistants, algebraic computation systems, and computational linguistics platforms.}, author = {Huet, G\'{e}rard}, citeulike-article-id = {169628}, citeulike-linkout-0 = {http://pauillac.inria.fr/~huet/PUBLIC/DB.pdf}, editor = {Kamareddine, Fairouz}, journal = {Thirty Five Years of Automating Mathematics}, keywords = {contexts, linear}, posted-at = {2006-08-18 11:51:35}, priority = {2}, publisher = {Kluwer}, title = {Linear Contexts and the Sharing Functor: Techniques for Symbolic Computation}, url = {http://pauillac.inria.fr/~huet/PUBLIC/DB.pdf}, year = {2003} }

TY - CONF ID - citeulike:169628 L3 - citeulike-article-id:169628 N2 - We present in this paper two design issues concerning fundamental representation structures for symbolic and logic computations. The first one concerns structured editing, or more generally the possibly destructive update of tree-like data-structures of inductive types. Instead of the standard implementation of mutable data structures containing references, we advocate the zipper technology, fully applicative. This may be considered a disciplined use of pointer reversal techniques. We argue that zippers, i.e. unary contexts generalizing stacks, are concrete representations of linear functions on algebraic data types. The second method is a uniform sharing functor, which is a variation on the traditional technique of hashing, but controling the indexing function on the client side rather than on the server side, which allows the fine-tuning of bucket balancing, taking into account specific statistical properties of the application data. Such techniques are of general interest for symbolic computation applications such as structure editors, proof assistants, algebraic computation systems, and computational linguistics platforms. JF - Thirty Five Years of Automating Mathematics TI - Linear Contexts and the Sharing Functor: Techniques for Symbolic Computation PB - Kluwer KW - contexts KW - linear AU - Huet, Gérard A2 - Kamareddine, Fairouz PY - 2003/// UR - http://pauillac.inria.fr/~huet/PUBLIC/DB.pdf ER -