Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Programming Language Implementation and Logic Programming

PLILP 1995: Programming Languages: Implementations, Logics and Programs pp 357–379Cite as

Local linear logic for locality consciousness in multiset transformation

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 982))

Abstract

We use Girard's linear logic (LL) to produce a semantics for Gamma, a multiset transformation language. The semantics improves on the existing structured operational semantics (SOS) of the language by highlighting Gamma's inefficiencies, which were hidden by the SOS. We propose a new logic called local linear logic (Local LL), which adds locality-consciousness to the resource-consciousness of linear logic. As a case study, we use this logic to propose a new semantics for Gamma. The new semantics suggests an annotation of Gamma which increases its efficiency without compromising its programming style. We show how the new semantics also gives us a better understanding of parallel Gamma and its implementation, and offers insight into the nature of chemicalreaction based computational models in general.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Abramsky. Computational interpretations of linear logic. Theoretical computer science, 111(3):3–57, Oct 1993.

    Google Scholar 

  2. V. M. Abrusci. Non-commutative intuitionistic linear logic. Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, 36(1):297–318, 1990.

    Google Scholar 

  3. V. M. Abrusci. Phase semantics and sequent calculus for pure non-commutative classical linear propositional logic. J. Symbolic Logic, 56(4):1403-1451, Dec 91.

    Google Scholar 

  4. V. Alexiev. Applications of linear logic to computation. Technical Report TR93-18, University of Alberta, Saskatchewan, Canada, 1993.

    Google Scholar 

  5. J.-M. Andreoli. Logic programming with focusing proofs in linear logic. J. Logic and Computation, 2(3):297–347, 1992.

    Google Scholar 

  6. R. J. R. Back and R. Kurki-Suonio. Decentralisation of process nets with centralised control. In 2nd SIGACT-SIGOPS Symp. on Principles of Distr. Computing (PODC), pages 131–142, Montreal, Canada, 1983. Springer Verlag, Berlin.

    Google Scholar 

  7. R. J. R. Back and R. Kurki-Suonio. Distributed co-operation with action systems. ACM transactions on programming languages and systems, 10(4):513–554, 1988.

    Google Scholar 

  8. H. G. Baker Jr. Lively linear Lisp — “look ma, no garbage!”. ACM SIGPLAN notices, 27(8):89–98, Aug 1992.

    Google Scholar 

  9. J.-P. Banâtre, A. Coutant, and D. le Métayer. Parallel machines for multiset transformations and their programming style. Informationstechnik, Oldenbourg Verlag, 30(2):99–109, 1988.

    Google Scholar 

  10. J.-P. Banâtre and D. le Métayer. Programming by multiset transformation. Research report PI 522, IRISA, Rennes, France, Mar 1990.

    Google Scholar 

  11. G. Berry and G. Boudol. The chemical abstract machine. In 17th Principles of programming languages, pages 81–94, San Fransisco, California, Jan 1990. ACM, New York.

    Google Scholar 

  12. K. M. Chandy and J. Misra. Parallel program design: A foundation. Addison Wesley, Reading, Massachusetts, 1988.

    Google Scholar 

  13. C. Creveuil and G. Moguerou. Dérivation systématique d'un algorithme de segmentation d'images — un exemple d'application du formalisme Gamma. Research report 1049, INRIA Rocquencourt, France, Jun 1989.

    Google Scholar 

  14. J. Darlington and Y. Guo. Reduction as deduction. In J. R. W. Glauert, editor, 6th Implementation of Functional Languages, pages 10.1–10.10. School of Information Systems, Univ. of East Anglia, Norwich, UK, Sep 1994.

    Google Scholar 

  15. L. Errington, C. Hankin, and T. Jensen. A congruence for gamma programs. In P. Cousot, M. Falaschi, G. Filè, and A. Rauzy, editors, 3rd Static Analysis (WSA), LNCS 724, Pages 242–253, Padova, Italy, 1993. Springer Verlag, Berlin.

    Google Scholar 

  16. D. Gelernter. Generative communication in linda. ACM transactions on programming languages and systems, 7(1):80–112, 1985.

    Google Scholar 

  17. D. Gelernter and A. J. Bernstein. Distributed communication via global buffer. In 1st SIGACT-SIGOPS Symp. on Principles of Distr. Computing (PODC) pages 10–18, Ottawa, Canada, 1982. ACM, New York.

    Google Scholar 

  18. J.-Y. Girard. Linear logic. Theoretical computer science, 50(1):1–102, 1987.

    Google Scholar 

  19. J.-Y. Girard, A. Scedrov, and P. J. Scott. Bounded linear logic: a modular approach to polynomial-time computability. Theoretical computer science, 97:1–66, 1992.

    Google Scholar 

  20. K. Gladitz and H. Kuchen. Shared memory implementation of the Gammaoperation. In J. R. W. Glauert, editor, 6th Implementation of Functional Languages, pages 26.1–26.13. School of Information Systems, Univ. of East Anglia, Norwich, UK, Sep 1994.

    Google Scholar 

  21. C. L. Hankin, D. le Métayer, and D. Sands. A calculus of Gamma programs. Research Report 92/22, Dept. of Computing, Imperial College London, Jul 1992.

    Google Scholar 

  22. C. L. Hankin, D. le Métayer, and D. Sands. Transformation of Gamma programs. In M. Billaud, P. Castéran, M-M. Corsini, K. Musumbu, and A. Rauzy, editors, Static Analysis (WSA 92), pages 12–19, Bordeaux, France, Sep 1992. BIGRE, 81–82.

    Google Scholar 

  23. P. H. Hartel, M. H. M. Smid, L. Torenvliet, and W. G. Vree. A parallel functional implementation of range queries. In P. G. M. Apers, D. Bosman, and J. van Leeuwen, editors, Computing science in The Netherlands, pages 173–189, Utrecht, The Netherlands, Nov 1989. CWI, Amsterdam.

    Google Scholar 

  24. Y. Lafont. The linear abstract machine. Theoretical Computer Science, 59:157–180, 1988.

    Google Scholar 

  25. Y. Lafont. Interaction nets. In 17th Principles of programming languages, pages 95–108, San Fransisco, California, Jan 1990. ACM, New York.

    Google Scholar 

  26. P. Lincoln and T. Winkler. Constant-only multiplicative linear logic is NP-complete. Theoretical computer science, 135(1):155–169, 1994.

    Google Scholar 

  27. H. McEvoy. Gamma, chromatic typing and vegetation. Technical report in preperation, Dept. of Comp. Sys, Univ. of Amsterdam; Presented at the ESPRIT 9102 coordination meeting, Geneva, Dec 1994.

    Google Scholar 

  28. H. McEvoy and J. Kaandorp. Multisets and their transformers as models for environmentally-sensitive growth. Dept. Comp. Sys., Univ. of Amsterdam, 1995.

    Google Scholar 

  29. J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical computer science, 96(1):73–155, 1992.

    Google Scholar 

  30. T. Toffoli and N. Margolus. Cellular automata machines. MIT press, Cambridge, Massachusetts, 1991.

    Google Scholar 

  31. A. S. Troelstra. Lectures on linear logic. Lecture notes 29, Centre for the Study of Language and Information, Leyland Stanford Junior University, California, 1992.

    Google Scholar 

  32. M. Vieillot. Premiers pas de Gamma avec une PAM. Rapport de stage, IFSIC, IRISA, Univ. de Rennes, France, 1992.

    Google Scholar 

  33. P. L. Wadler. Linear types can change the world! In M. Broy and C. B. Jones, editors, Programming concepts and methods, pages 561–581, Sea of Gallilee, Israel, Apr 1990. North Holland, Amsterdam.

    Google Scholar 

  34. S. Wolfram. Cellular automata and complexity. Addison Wesley, Reading, Massachusetts, 1994.

    Google Scholar 

  35. D. Yetter. Quantales and (noncommutative) linear logic. J. Symbolic logic, 55(1):41–64, 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Systems, University of Amsterdam, Kruislaan 403, 1098, SJ Amsterdam, The Netherlands

    Hugh McEvoy & Pieter H. Hartel

Authors
  1. Hugh McEvoy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pieter H. Hartel
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Manuel Hermenegildo S. Doaitse Swierstra

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

McEvoy, H., Hartel, P.H. (1995). Local linear logic for locality consciousness in multiset transformation. In: Hermenegildo, M., Swierstra, S.D. (eds) Programming Languages: Implementations, Logics and Programs. PLILP 1995. Lecture Notes in Computer Science, vol 982. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0026830

Download citation

  • DOI: https://doi.org/10.1007/BFb0026830

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60359-7

  • Online ISBN: 978-3-540-45048-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation