×

Linear logic. (English) Zbl 0625.03037

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.
Reviewer: G.Kreisel

MSC:

03F05 Cut-elimination and normal-form theorems
68N01 General topics in the theory of software
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B70 Logic in computer science
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Girard, J.-Y., Une extension de l’interprétation de Gödel à l’analyse et son application à l’elimination des coupures dans l’analyse et dans la théorie des types, (Fenstadt, J. E., Proc. 2nd Scand. Logic Symp. (1971), North-Holland: North-Holland Amsterdam), 63-92
[2] Girard, J.-Y., Interprétation fonctionelle et élimination des cupures de l’arithmétique d’ordre supérieur, (Thèse de Doctorat d’Etat (1972), UER de Mathématiques, Univ. de Paris VII)
[3] Girard, J.-Y., Three-valued logic and cut-elimination: the actual meaning of Takeuti’s conjecture, Dissertationes Math., CXXXVI (1976) · Zbl 0357.02027
[4] J.-Y. Girard, Normal functors, power series and lambda-calculus, Ann. Pure Appl. Logic; J.-Y. Girard, Normal functors, power series and lambda-calculus, Ann. Pure Appl. Logic
[5] Girard, J.-Y., The system \(F\) of variable types, Theoret. Comput. Sci., 45, 2, 159-192 (1986), fifteen years later · Zbl 0623.03013
[6] Kreisel, G.; Takeuti, G., Formally self-referential propositions for cut-free classical analysis and related systems, Dissertationes Math., CXVIII (1974) · Zbl 0336.02027
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.