Linear logic (Q579249)

The paper contains, in reverse order, (A) a substantial contribution to proof theory, and (B) speculations on using proofs as parts of programs, interspersed by (C) diverse relations to the (logical) literature. Here are a few samples from this, at least, for the reviewer, very readable paper. - (A) Building on extensive experience the author develops a smooth cut elimination theory (for proof `nets') with new logical operators, which achieve, demonstrably more efficiently, goals of traditional proof theory. A suitable selection leads to genuinely decidable subsystems, related to contraction-free rules studied by Herbrand, Wang, Ketonen and others, but neglected (overshadowed by foundational preoccupation with completeness, proof-theoretic strength, and similar flashy ideals, to which the author occasionally reverts, too; c.f. the end of 5.5 on p. 92 about conservation). (B) Viewed against the background of all mathematics, let alone all data processing, proofs are rarely (used in) programs, and programs rarely contain specifications of the problems they are meant for, let alone, proofs that they solve them. (P.7.III (ii) on `isolation' is to be understood in this sense). A proper focus is the - admittedly, \(\forall \exists\) small - speciality of extracting bounds from prima facie non-constructive proofs in mathematics, and synthesizing programs mechanically from suitable fragments of formal proofs. The author envisages (but does not state explicitly) a master program \(\Pi\) for his normalization procedure, with formal derivations \(\pi\) of his system as inputs, and their (unique) normal form \({\bar \pi}\) as output. The assumption is that \({\bar \pi}\) provides information that has (market) value but is not read off easily from \(\pi\), let alone, from the fact that the end formula F of \(\pi\) is true; on p. 17 there is a garbled reference to this in terms of different `interpretations' of: F is true. A colourful description of \(\pi\) in Chapter 2 suggests that \(\Pi\) lends itself to parallel processing; tacitly, without long waiting times (because of an `intrinsic' order). But this is not checked, nor even compared to familiar algebraic `normalization' procedures, for example, of rational expressions to fractions. - (C) One theme of the author's observations is the distrust, shared by contemporary (French) mathematicians, of the master assumption behind the logical tradition: general, and therefore coarse notions, like arbitrary or general recursive functions, are the first order of business (instead of: reculer pour mieux sauter). Thus he replaces the `big' spaces in Scott's theory of domains by more structured, coherent spaces, associating to programs \(\Pi\) corresponding functions \(\alpha_{\Pi}\) (on the spaces considered). A less publicized defect of the logical tradition of generality is that it does not even try to exploit specifics, such as the special properties, mentioned in (B), of programs that happen to include proofs. Without exaggeration, the - often, admittedly, clumsy - objections of engineers on p. 7.III to airy-fairy theory apply to the logical ideal of theory above; certainly, not to be theories used for developing semiconductors and superconductors that have made computer hardware one of the wonders of the modern world.