Abstract
In programming languages based on linear logic, the program can grow and shrink in a nearly arbitrary manner over the course of execution. Since the introduction of the I/O model of proof search [11, 12], a number of refinements have been proposed with the intention of reducing its degree of non-determinism [3, 4, 12, 13, 14]. Unfortunately each of these systems has had some limitations. In particular, while the resource management systems of Cervesato et al. [3, 4] and the frame system of López and Pimentel [14] obtained the greatest degree of determinism, they required global operations on the set of clauses which were suitable only for interpreter-based implementations. In contrast the level-tags system of Hodas, et al. relied only on relabeling tags attached to individual formulas, and was hence appropriate as the specification of an abstract machine. However it retained more non-determinism than the resource management systems. This led to a divergence in the operational semantics of the interpreted and compiled versions of the language Lolli. In this paper we propose a tag-frame system which recaptures the behavior of the resource management systems, while being appropriate as a foundation of a compiled implementation.
López and Pimentel were supported in part by the project TIC2001-2705-C03-02 funded by the Spanish Ministry of Science and Technology. During the summer of 2001, López was also supported in part by a travel grant from Harvey Mudd College.
Stoilova was supported in part by a grant from the Harvey Mudd College Computer Science Clinic Program.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 1992.
Jean-Marc Andreoli. Focusing and proof construction. Annals of Pure and Applied Logic, 107(1-3):131–163, 2001.
Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning. Efficient resource management for linear logic proof search. In Roy Dyckhoff, Heinrich Herre, and Peter Schroeder-Heister, editors, Proceedings of the Fifth International Workshop on Extensions of Logic Programming, volume 1050 of Lecture Notes in Artificial Intelligence, pages 67–81. Springer-Verlag, March 1996.
Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning. Efficient resource management for linear logic proof search. Theoretical Computer Science, 232(1-2), February 2000.
James Harland and David Pym. The uniform proof-theoretic foundation of linear logic programming. In V. Saraswat and K. Ueda, editors, Proceedings of the 1991 International Logic Programming Symposium, pages 304–318. M. I. T. Press, 1991.
James Harland and David Pym. A uniform proof-theoretic investigation of linear logic programming. Journal of Logic and Computation, 4(2):175–207, April 1994.
James Harland and David Pym. Resource distribution via boolean constraints. In W. McCune, editor, Proceedings of the Fourteenth International Conference on Automated Deduction — CADE-14, Townsville, Australia, 1997.
James Harland, David Pym, and Michael Winikoff. Programming in Lygon: An overview. In M. Wirsing and M. Nivat, editors, Algebraic Methodology and Software Technology, pages 391–405, Munich, Germany, 1996. Springer-Verlag LNCS 1101.
James Harland and Michael Winikoff. Implementing the linear logic programming language Lygon. In John Lloyd, editor, Proceedings of the 1995 International Logic Programming Symposium, pages 66–80, 1995.
J. S. Hodas. Logic Programming in Intuitionistic Linear Logic: Theory, Design and Implementation. PhD thesis, University of Pennsylvania, Department of Computer and Information Science, 1994.
J. S. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science, July 15-18 1991.
J. S. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. Information and Computation, 110(2):327–365, 1994. Extended abstract in the Proceedings of the Sixth Annual Symposium on Logic in Computer Science, Amsterdam, July 15-18, 1991.
J. S. Hodas, K. Watkins, N. Tamura, and K.-S. Kang. Efficient implementation of a linear logic programming language. In Proceedings of the 1998 Joint International Conference and Symposium on Logic Programming, pages 145–159, June 1998.
Pablo L’opez and Ernesto Pimentel. Resource management in linear logic proof search revisited. In Logic for Programming and Automated Reasoning, volume 1705, pages 304–319. Springer Verlag, 1999.
D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.
N. Tamura and Y. Kaneda. Extension of WAM for a linear logic programming language. In T. Ida, A. Ohori, and M. Takeichi, editors, Second Fuji International Workshop on Functional and Logic Programming, pages 33–50. World Scientific, Nov. 1996.
Kevin Watkins. Unpublished Note, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hodas, J.S., López, P., Polakow, J., Stoilova, L., Pimentel, E. (2002). A Tag-Frame System of Resource Management for Proof Search in Linear-Logic Programming. In: Bradfield, J. (eds) Computer Science Logic. CSL 2002. Lecture Notes in Computer Science, vol 2471. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45793-3_12
Download citation
DOI: https://doi.org/10.1007/3-540-45793-3_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44240-0
Online ISBN: 978-3-540-45793-0
eBook Packages: Springer Book Archive