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.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
Bibliography
Alfred V. Aho, Ravi Sethi and Jeffrey D. Ullman. “Compilers - Principles, Techniques and Tools.” Addison-Wesley, 1986.
Jon L. Bentley and Robert Sedgewick. “Fast Algorithms for Sorting and Searching Strings.” Proceedings, 8th Annual ACM-SIAM Symposium on Discrete Algorithms, Jan. 1997.
N.G. de Bruijn. “The mathematical language AUTOMATH, its usage and some of its extensions.” Symposium on Automatic Demonstration, IRIA, Versailles, 1968. Printed as Springer-Verlag Lecture Notes in Mathematics 125, (1970) 29–61.
N.G. de Bruijn. “Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem.” Indag. Math. 34,5 (1972), 381–392.
Guy Cousineau and Michel Mauny. “The Functional Approach to Programming.” Cambridge University Press, 1998.
Philippe Flajolet, Paola Sipala and Jean-Marc Steyaert. “Analytic Variations on the Common Subexpresssion Problem.” Proceedings of 17th ICALP Colloquium, Warwick (1990), LNCS 443, Springer-Verlag, pp. 220–234.
R. Hinze, J. Jeuring and A. Löh. “Type-indexed data types.” In Mathematics for Program Construction, Springer-Verlag LNCS 2386 (2002).
G. Huet. “An analysis of Böhm’s theorem.” In “To C. Böhm: Essays on Lambda-Calculus and Functional Programming”, eds. M. Dezani-Ciancaglini, S. Ronchi della Rocca and M. Venturini Zilli. Also Theoretical Computer Science 121 (1993) 145–167.
Gérard Huet. “The Zipper”. J. Functional Programming 7,5 (Sept. 1997), pp. 549–554.
G. Huet. “Transducers as Lexicon Morphisms, Phonemic Segmentation by Euphony Analysis, Application to a Sanskrit Tagger.” Available as: http://pauillac.inria.fr/~huet/PUBLIC/tagger.pdt.
G. Huet. The Zen Computational Linguistics Toolkit. ESSLLI 2002 Lectures, Trento, Italy, Aug. 2002. Available as: http://pauillac.tarts.ir/~huet/PUBLIC/esslli.pd!.
G. Huet. “Mixed Automata.” To appear, Festschrift volume for Zohar Manna’s 64th anniversary. LNCS, Springer-Verlag, 2003.
A. K. Joshi, and Y. Schabes. “Tree-adjoining grammars.” In A. Salomma and G. Rozenberg, Eds., Handbook of Formal Languages and Automata. Springer, Berlin (1997).
Yves Lafont. “Interaction Combinators.” Information and Computation 137,1 (1997) pp. 69–101.
Xavier Leroy et al. “Objective Caml.” See: http://caml.inria.fr/ocaml/inder.html.
Conor McBride. “The Derivative of a Regular Type is its Type of One-Hole Contexts.” Available from:http://vw.dur.ac.uk/dcslvtm/difl.ps.
Jean-Michel Muller. “Elementary Functions - Algorithms and Implementation.” Birkhäuser, 1997.
Daniel de Rauglaudre. “The Camlp4 preprocessor.” See: http://caml.inria.fr/camlp4/.
Pierre Weis and Xavier Leroy. “Le langage Caanl.” 2ème édition, Dunod, Paris, 1999.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Huet, G. (2003). Linear Contexts, Sharing Functors: Techniques for Symbolic Computation. In: Kamareddine, F.D. (eds) Thirty Five Years of Automating Mathematics. Applied Logic Series, vol 28. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-0253-9_4
Download citation
DOI: https://doi.org/10.1007/978-94-017-0253-9_4
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-6440-0
Online ISBN: 978-94-017-0253-9
eBook Packages: Springer Book Archive