Hostname: page-component-78c5997874-4rdpn Total loading time: 0 Render date: 2024-11-05T12:11:24.591Z Has data issue: false hasContentIssue false
  • English
  • Français

Causal dependencies in multiplicative linear logic with MIX

Published online by Cambridge University Press:  04 March 2009

Andrea Asperti
Andrea Asperti
Affiliation:
Dip. di Matematica, Universitá di Bologna, P.za di Porta S.Donato, 40126, Bologna, Italy. Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

A new correctness criterion for discriminating Proof Nets among Proof Structures of Multiplicative Linear Logic with the MIX rule is provided. This criterion is inspired by an original interpretation of Proof Structures as distributed systems, and logical formulae as processes. The computation inside a system corresponds to the logical flow of information inside a proof, that is, roughly speaking, a distributed version of Girard's token trip. Proof Nets are then characterised as deadlock free Proof Structures (deadlock free distributed systems). This result follows by explicitly considering the causal dependencies among logical formulae inside proofs, and it provides a new understanding of notions such as acyclicity, chains and empires in terms of concurrent computations.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 5 , Issue 3 , September 1995 , pp. 351 - 380
Copyright
Copyright © Cambridge University Press 1995

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Asperti, A. (1991) A linguistic approach to deadlock. Rapport de Recherche du Laboratoire d'Informatique de l'Ecole Normale Supérieure de Paris, LIENS–91–15.Google Scholar
Asperti, A., Ferrari, G. and Gorrieri, R. (1990) Implicative Formulae in the 'Proofs-as-Computations analogy. Proc. of the 17th Symposium on Principles of Programming Languages (POPL 90), San Francisco.CrossRefGoogle Scholar
Asperti, A. and Longo, G. (1991) Categories. Types and Structures. An introduction to Category Theory for the working computer scientist. Foundations of Computing series, M.I.T. Press.Google Scholar
Bellin, G. (1990) Mechanizing Proof theory: Resource-Aware Logics and Proof-Transformations to Extract Implicit Information. Ph.D Thesis, Report CST–80–91, Department of Computer Science, University of Edinburgh.Google Scholar
Bellin, G. (1993) Proof Nets for Multiplicative and Additive Linear Logic. (Draft; early version as Report LFCS–91–161, May 1991, Department of Computer Science, University of Edinburgh.)Google Scholar
Bellin, G. and Ketonen, J. (1992) A decison procedure revisited: Notes on direct logic, linear logic and its implementation. Theoretical Computer Science 95 115–142.Google Scholar
Bellin, G. and van de Wiele, J. (1993) Proof Nets and Typed lambda Calculus. I. Empires and Kingdoms. (Draft)Google Scholar
Danos, V. (1990) La Logique Linéaire appliquée à l'étude de divers processus de normalization. These de doctorat, Université Paris VII.Google Scholar
Danos, V. and Regnier, L. (1989) The Structure of Multiplicatives. Arch. Math. Logic 28.CrossRefGoogle Scholar
Fleury, A. and Retoré, C. (1991) The MIX rule. (Draft)Google Scholar
Gallier, J. (1991) Constructive Logics. Part II: Linear logic and Proof Nets. Technical Report of Digital Paris Research Laboratory 9.Google Scholar
Girard, J. Y. (1986) Linear Logic. Theoretical Computer Science 50.Google Scholar
Ketonen, J. and Weyhrauch, R. (1984) A Decidable Fragment of Predicate Calculus. Theoretical Computer Science 32.Google Scholar
Marti-Oliet, N. and Meseguer, J. (1989) From Petri Nets to Linear Logic. In: Pitt, D. H. and Rydeheard, D. E. (eds.) Proc. of the third conference on Category Theory and Computer Science. Springer-Verlag Lecture Notes in Computer Science 389.CrossRefGoogle Scholar
Petri, C. A. (1962) Kommunication mit Automaten. Schriften des Institutes für Instruentelle Mathematik, Bonn.Google Scholar
Reisig, W. (1985) Petri Nets, an introduction. EATCS Monographs on Theoretical Computer Science 4, Springer-Verlag.Google Scholar
Retoré, C. (1990) A First Move from non Commutative Linear Logic to True Concurrency: the calculus of ordered sequents. (Draft)Google Scholar
Retore, C. (1993) Réseaux et Séquents Ordonnés. Thése de doctorat, Université Paris VII.Google Scholar
Roorda, D. (1990) Quantum Graphs and Proof Nets. (Draft)Google Scholar
Roorda, D. (1991) Resource Logics: Proof-theoretical Investigations. Ph.D. Thesis, University of Amsterdam.Google Scholar
Troelstra, A. S. (1990) Lectures on Linear logic. Techical Report X–90–15, University of Amsterdam.Google Scholar