On Geometry of Interaction

  • Jean-Yves Girard
Conference paper
Part of the NATO ASI Series book series (volume 139)

Abstract

The paper expounds geometry of interaction, for the first time in the full case, i.e. for all connectives of linear logic, including additives and constants. The interpretation is done within a C*-algebra which is induced by the rule of resolution of logic programming, and therefore the execution formula can be presented as a simple logic programming loop. Part of the data is public (shared channels) but part of it can be viewed as private dialect (defined up to isomorphism) that cannot be shared during interaction, thus illustrating the theme of communication without understanding. One can prove a nilpotency (i.e. termination) theorem for this semantics, and also its soundness w.r.t. a slight modification of familiar sequent calculus in the case of exponential-free conclusions.

Keywords

Gasoline Lamination Prefix Hyde Univer 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [A93]
    Asperti, A.: Linear Logic, Comonads and Optimal Reductions, to appear in Fundamenta Informaticae, Special Issue devoted to Categories in Computer Science.Google Scholar
  2. [B92]
    Blass, A.: A game semantics for linear logic, Annals Pure Appi. Logic 56, pp. 183–220, 1992.MATHMathSciNetGoogle Scholar
  3. [DR93]
    Danos, V. & Regnier, L.: GOI 2.0. manuscript, 1993.Google Scholar
  4. [G86]
    Girard, J.-Y.: Linear Logic, Theoretical Computer Science 50.1, pp. 1–102, 1987.MATHMathSciNetGoogle Scholar
  5. [G86A]
    Girard, J.-Y.: Multiplicatives, Rendiconti del Seminario Matematico dell’Università e Policlinico di Torino, special issue on Logic and Computer Science, pp. 11–33, 1987.Google Scholar
  6. [G87]
    Girard, J.-Y.: Towards a Geometry of Interaction, Categories in Computer Science and Logic, Contemporary Mathematics 92, AMS 1989, pp. 69–108.MathSciNetGoogle Scholar
  7. [G88]
    Girard, J.-Y.: Geometry of Interaction I: interpretation of system F, Proceedings Logic Colloquium ’88, eds. Ferro & al., pp. 221–260, North Holland 1989.Google Scholar
  8. [G88A]
    Girard, J.-Y.: Geometry of Interaction II: deadlock-free algorithms, Proceedings of COLOG-88, eds Martin-Lof & Mints, pp. 76–93, LNCS 417, Springer-Verlag 1990.Google Scholar
  9. [G94]
    Girard, J.-Y.: Proof-nets for additives, manuscript, 1994.Google Scholar
  10. [GAL92]
    Gonthier, G. & Abadi, M. & Levy, J.-J.: The Geometry of Optimal Lambda Reduction, Proc. 19-th Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico, ACM Press, New York, 1992.Google Scholar
  11. [J93]
    Jacobs, B.: Semantics of weakening and contraction, Annals of Pure and Applied Logic 69, 1994, pp. 73–106.CrossRefMATHMathSciNetGoogle Scholar
  12. [LMSS90]
    Lincoln, P. & Mitchell, J. & Scedrov, A. & Shankar N.: Decision Problems in Propositional Linear Logic, Annals of Pure and Applied Logic 56, 1992, pp. 239–311.CrossRefMATHMathSciNetGoogle Scholar
  13. [LW92]
    Lincoln, P. & Winkler, T.: Constant-only Multiplicative Linear Logic is NP-complete, Theoretical Computer Science 135, 1994, pp. 155–159.CrossRefMATHMathSciNetGoogle Scholar
  14. [MM93]
    Martini, S. & Masini A.: On the fine structure of the exponential rules, to appear in Advances in Linear Logic, Cambridge University Press 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Jean-Yves Girard
    • 1
  1. 1.Laboratoire de Mathématiques DiscrètesUPR 9016 — CNRSMarseille Cedex 09France

Personalised recommendations