Bounded linear logic: A modular approach to polynomial time computability. Extended abstract (Q4035310)

[For the entire collection see Zbl 0753.00018.] The article deals with typing as a way of describing the interactive behaviour of algorithms. It proposes Bounded Linear Logic (BLL) to represent successfully the dynamics of typing systems and restore the contraction rule. BLL is intermediate between second-order Rudimentary Linear Logic (RLL) and full second-order Linear Logic (LL) with respect to the representation of polynomial-time functions. It considers the bounded storage concept and the corresponding bounded exclamation mark as a new kind of typing instructions. The syntax of BLL is considered as a possible framework for a modular calculus of efficient algorithms. The paper presents brief descriptions of relevant results from RLL and LL and compares them with corresponding concepts and facts for BLL (e.g., rules for Storage, Weakening, Contraction, Dereliction). The main results are presented as sequence of theorems and lemmas with illustrating examples provided. The following conclusions are drawn: a) BLL normalizes in polynomial time. b) Every polynomial-time computable function can be typed in BLL. Topics and directions of further investigations based on BLL are outlined.