zbMATH — the first resource for mathematics

Geometry of interaction. I: Interpretation of system F. (English) Zbl 0686.03030
Logic colloq. ’88, Proc. Colloq., Padova/Italy 1988, Stud. Logic Found. Math. 127, 221-260 (1989).
[For the entire collection see Zbl 0673.00007.]
The author provides an explicit formula for cut elimination from Gentzen- type derivations. To each derivation \(\Pi\) in second order linear logic, two matrices u, \(\sigma\) are assigned, and the proof of the following fact is sketched. The normal form of \(\Pi\) under the standard cut elimination procedure is given by the matrix \(EX(u,\sigma)=(1-\sigma^ 2)u(1-\sigma u)^{-1}(1-\sigma^ 2)\) provided the final sequent of \(\Pi\) does not contain the connectives ?, \(\exists\). Coefficients of the matrix u are bounded operators in Hilbert space, and coefficients of \(\sigma\) are 0, 1, describing in a straightforward way cuts present in the proof \(\Pi\). Intuitionistic and classical logic probably can be treated via the author’s embedding in linear logic [Theor. Comput. Sci. 50, 1-102 (1987; Zbl 0625.03037)]. A specific \(C^*\)-algebra \(\Lambda^*\) is introduced to model linear logic. The author makes a lot of optimistic comments concerning possible future applications of functional analysis to the study of linear logic, and of linear logic to the study of interactive computations.
Reviewer: G.Mints

03F05 Cut-elimination and normal-form theorems
03B70 Logic in computer science