zbMATH — the first resource for mathematics

The structure of multiplicatives. (English) Zbl 0689.03013
This paper is usually thoughtful compared to the bulk of current theoretical computer science even though the jargon is as breezy (and unidiomatic) as the rest. The broad idea is to interpret formulae and operations of multiplicative linear logic; not specifically propositionally, but in terms of general data and their processing (in stages). In the tradition of so-called tense logic - with words like ‘now’, ‘later’ etc. - the formalism does not contain any explicit variable(s) for the stages implicit in the interpretation considered. The present paper is, however, at least to this reviewer, much more compelling than tense logic, simply because the latter remains committed to the propositional oprators familiar from ordinary truth-functional logic (as if it were a matter of course that the privileged role, that is, functional completeness, of those operators for the familiar interpretation would carry over automatically to any new variants). But granted this, and despite its title, the paper does not provide a similarly convincing (completeness) property for its multiplicatives (and their interpretation). According to p. 202, the philosophy of this study is to rely on ‘current theory’ and the particular intuitive support associated with it; tacitly, in circles engaged in the ‘theory’ of linear logic. There is no reference to - intuitive support from - either centuries of experience in planning or, in current jargon, programming computations nor experience with high-speed or other specifically electronic computation (which could modify the ‘intuitive support’ provided by the older experience). At this general level there is another, perhaps even more disturbing reminder. The so-called logical aspects of time, without explicit reference to stages, are of course present in the behaviour of dynamical systems, too: Is the neglect of those aspects in the theory of such systems a mere blind spot?
Reviewer: G.Kreisel

03B70 Logic in computer science
68N25 Theory of operating systems
68Q65 Abstract data types; algebraic specification
Full Text: DOI
[1] Szabo, M.E.: Collected works of Gehrard Gentzen. Amsterdam: North-Holland 1969 · Zbl 0209.30001
[2] Girard, J.Y.: Linear logic. Theoretical Computer Science50 (1987)
[3] Girard, J.Y.: Multiplicatives. To appear in the Proceedings of the Congress of Logic and Computer Science held in Torino, October 1986
[4] Girard, J.Y.: Towards a geometry of interaction. To appear in the acts of AMS conference on categories, Boulder, June 1987
[5] Girard, J.Y.: Quantifiers in linear logic. To appear in the Proceedings of the SILFS conference, held in Cesena, January 1987
[6] Danos, V.: Correctness of proof-nets. Draft, université de Paris VII, March 1988
[7] Van de Wiele, J.: Jeux en Logique Linéaire. Draft, Université de Paris VII, November 1988
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.