Meeting on Logic and Complexity    (ProToCoLLo)

Bertinoro, 15^th and 16^th October 2003

The idea is to bring together researchers involved in the italian national project “Protocollo”, one of whose research mainstreams is about implicit characterizations of computational classes, based, as much as possible, on structural proof-theroy.

It will take place just after the end of ICTCS03, on 15^th afternoon.

The programme divides essentially in three parts:

• Wednesday 15^th , in the afternoon: the most stable material and ideas, will be presented. The speakers will have slots of 40 minutes;

• Thursday 16^th , in the morning: less formalized subjects and problems will be presented. The speakers will have slots of about 50 minutes whose sharing of time, between presentation and discussion, is up to the speakers;

• Thursday 16^th , in the afternoon: free discussion, may be in separate groups, each working on one the subjects, illustrated in the morning, or something related. We shall conclude by a talk by Harry Mairson on a topic not directly related with the meeting topics, but which involves linear logic technology, so it is related to the whole Protocollo project.

Scheduling, short abstract on stable and informal talk subjects and a list of the participants follow.

Scheduling

Structured material and ideas

Martin Hoffman

A. Type systems for non-size-increasing functions.

Harry Mairson

I. The talk is about some observations on Wadler's ICFP paper "Call by value is dual to call by name": I think better results can be stated.

Katsushige Terui

B. Light Affine Logic simplified.

Ugo Dal Lago

C. Higher-Order Linear Ramified Recurrence (HOLRR) is a ptime sound and complete typed lambda caluclus. Its terms are those of a linear (affine) lambda-calculus -- every variable occurs at most once -- extended with a limited recursive scheme on a word algebra. Completeness for ptime holds by embedding Leivant's ramified recurrence on words into HOLRR. Soundness is established at all types -- and not only for first order terms. Type connectives are limited to tensor and linear implicaation. Moreover, typing rules are given as a simple deductive system.

Damiano Mazza

D. Danos e Joinet define Elementary Linear Logic {ELL} as a subsystem of Linear Logic {LL} whose derivations satisfy a couple of structural constraints. The approach is extended to characterize deterministic polynomial computations.

Works in progress and informal ideas

Ugo Dal Lago

E. The paper where Lafont introduces Soft Linear Logic, concludes with some suggestions about how to obtain an elementary version of SLL. The idea is to discuss about such seggestions.

F. Elementary and Light logics can be used as type assignments for the untyped lambda-calculus. Given an untyped lambda term M and a type derivation \pi for M, it is possible to compute (in time O(|pi|)) a bound to the number of reduction steps to the normal form of M. The discussion is about the possibility of improving the quality of such a bound.

Damiano Mazza

G. The goal of this discussion is to understand why “light logics” work. The starting point is to show examples of computations inside Linear and Classical logics which are not elementary.

H. The definition of SLL, by Lafont, is not completely under control: the goal is to clarify some points about syntax, polytime soundness and completeness.

Participants

Paolo Coppola (Udine)

Martin Hoffman (Munich)

Ugo Dal Lago (Bologna)

Harry Mairson (Boston - MA)

Simone Martini (Bologna)

Damiano Mazza (Marseille)

Simona Ronchi Della Rocca (Torino)

Luca Roversi (Torino)

Katsushige Terui (Tokio)

Lorenzo Tortora De Falco (Roma)