Linear lambda-terms and natural deduction (Q1577345)

In the paper the !-free fragment, with \(\otimes\), \(\&\), \(I\) and linear implication, of intuitionistic propositional linear logic is studied. The main issue is the unique normal form for natural deduction in this fragment. The approach uses the system of typed \(\lambda\)-terms with two sorts of pairing and projection corresponding to \(\otimes\) and \(\&\). It is much closer to the framework of standard \(\lambda\)-calculus than the approaches based on let-construction. In the paper's notation let would correspond to the introduction of ``frozen'' substitution for the components of a tensor term. The paper avoids this, working in the standard language of \(\lambda\)-terms and defining substitution in a standard way. The uniqueness of normal form in the case without \(I\) is achieved by pushing all \(\otimes\)-eliminations downward and grouping ``parallel'' \(\otimes\)-eliminations together. The proof of uniqueness uses an interpretation of \(\otimes\)-substitution as a multiplication operation on \(\lambda\)-terms. After that the extension to the language with \(I\) (in case of \(\beta\)-conversion) is obtained. Future development of this approach, according to the author, will probably permit to avoid ``boxing'' devices used in the approaches based on proof-nets.