Linear lambda-terms and natural deduction
type: Item
instance of: scholarly article
title: Linear lambda-terms and natural deduction
zbMATH Open document ID: 0974.03051
DOI: 10.1023/A:1005016206457
published in: Studia Logica
publication date: 2001-12-07T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03F52
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 1501372
zbMATH Keywords: linear logic
zbMATH Keywords: natural deduction
zbMATH Keywords: normalization
zbMATH Keywords: \(\lambda\)-calculus
author: G. E. Mints
reviewed by: Serguei V. Solov'ev
MaRDI profile type: Publication
full work available at URL: a:1005016206457
OpenAlex ID: W1593393851
description: scientific article; zbMATH DE number 1501372