zbMATH — the first resource for mathematics

Linear logic and parallelism. (English) Zbl 0629.03036
Mathematical models for the semantics of parallelism, Proc. Adv. Sch., Rome/Italy 1986, Lect. Notes Comput. Sci. 280, 166-182 (1987).
[For the entire collection see Zbl 0623.00021.]
The author presents his ideas on using linear logic for programming (especially, parallel) computations more compactly than in Theor. Comput. Sci. 50, 1-102 (1987; Zbl 0625.03037), [LL] for short; in fact, except for the botched syntax, remarkably elegantly. But the general literary form used is the same. It is familiar from (other) mathematics applied - to science and, what is more to the point here - to engineering: words in the jargon of the trade (of programming) are attached to mathematical, here, proof-theoretic, notions; to be compared to ‘heat equation’, ‘energy integral’ and the like. What is missing corresponds to what scientists and engineers call ‘remembering Nature’, resp. ‘the market behind the mathematics’. Taken literally, several passages suggest that this omission is not haphazard, but related to the author’s particular idea(l)s of theory, in the logical tradition. For example, p. 167, l.13- 14 refers blithely to ‘theoretical interests’ without regard to the overriding question, which (sub)areas of data processing - of problems (data) and of processors - lend themselves to any theory remotely of the kind envisaged? P. 168 (ii) and (iii) neglect the known facts that strong normalization is not sufficient for efficient computation in parallel (as in (B) in the review of [LL]), resp. that proof-theoretic strength entails algorithmic weakness, key reminder: closure under Markov’s rule. More generally, the principal lesson of experience with logical foundation (l.f.) of all of mathematics, (from which internal debates about, say, classical and intuitionistic logic distract, and) which applies also to l.f. for the narrower domain of programming, seems to be neglected: the most demanding job is to discover areas \((=\) markets) for which logical theory is rewarding at all.
Reviewer: G.Kreisel

03F05 Cut-elimination and normal-form theorems
68Q65 Abstract data types; algebraic specification