Polynomial time in untyped elementary linear logic. Unpublished note

We show how to represent polynomial time computation in an untyped version of proof-nets of elementary linear logic. Following a question of J.-Y. Girard asking whether a restriction on the types of elemen-tary linear logic (ELL [Gir98]) could represent exactly polynomial time computation (PTIME), P. Baillot [Bai11] shown that proofs of!W (!!Ba (with W = ∀α.!(α ( α) (!(α ( α) (!(α ( α) and Ba = ∀α.α ( α ( α) in second-order intuitionistic elementary affine logic en-riched with type fix-points exactly represent PTIME problems. We prove a similar result in untyped classical elementary linear logic. This stresses the standard fact that types are useless for the control of complexity in elementary linear logic. Moreover it shows that linear proofs are enough (the general weakening principle of affine logics is not required). 1 Untyped Elementary Proof-Nets 1.1 E-Nets An e-net is a directed acyclic graph with loose edges. Incoming edges of a node are called its premises and its outgoing edges are its conclusions. The loose edges are called the conclusions of the e-net. Each node has an associated kind