Modello A - Anno 2004 - prot. 2004011194

PARTE I
1.1 Programma di Ricerca di tipo
Interuniversitario


Area scientifico disciplinare Scienze matematiche e informatiche (100%) 
 
 


1.2 Titolo del Programma di Ricerca


Testo italiano

Fondazioni Logiche di Linguaggi Astratti di Programmazione


Testo inglese
Logical foundations of abstract programming languages


1.3 Abstract del Programma di Ricerca


Testo italiano

Il progetto si propone come continuazione del progetto cofinanziato MIUR2002
”PROTOCOLLO” (from PROofs TO COmputation through Linear LOgic),
rispetto al quale si pone con un duplice obiettivo. Da un lato, vuole proseguire
lo sviluppo di promettenti filoni di ricerca fondazionale e applicativa di informatica
teorica, scaturiti dall’introduzione della Logica Lineare (LL). Dall’altra, a
partire dai risultati teorici, vuole sviluppare metodologie per il disegno, l’analisi
e la verifica di linguaggi paradigmatici di programmazione, orientati al contesto
di computazioni mobili con risorse limitate.
Le sedi partecipanti al progetto raccolgono, oltre a tutti i ricercatori che hanno
fatto parte del progetto PROTOCOLLO, alcuni “nuovi ingressi” con competenze
soprattutto nell’ambito del Lambda Calcolo e della Ludica. L’esperienza
di collaborazione maturata nell’ambito del progetto PROTOCOLLO e’ stata
molto fruttuosa, come si puo’ vedere dalle numerose pubblicazioni prodotte,
molte delle quali scritte congiuntamente da ricercatori di unita’ diverse (sito del
progetto http://protocollo.di.unito.it). Abbiamo indagato sulla Logica Lineare,
e in particolare sulle sue possibili applicazioni a specifici problemi dell’Informatica.
Ci aspettiamo ora di incrementare la sinergia gia’ esistente, per procedere ad
un ulteriore e piu’ profonda indagine teorica, e per applicare i risultati ottenuti,
insieme alla nostra esperienza nel campo del Lambda Calcolo, per sviluppare
specifiche metodologie per disegno, l’analisi e la verifica di linguaggi di programmazione.
La problematica reale della computazione mobile con risorse limitate,
la cui importanza e’ testimoniata dal progetto Global Mobile Resource Garantees
(MRG) (http://groups.inf.ed.ac.uk/mrg/), ci sara’ di ispirazione e riscontro.
Infatti crediamo che molti dei risultati da noi gia’ ottenuti nell’ambito delle
logiche leggere possano essere applicati fruttuosamente in tale contesto.


Testo inglese
This project is proposed like a continuation of MIUR-2002 ”PROTOCOLLO”
project (from PROofs TO COmputation through Linear LOgic), and it is placed,
regarding the previous one, with a twofold objective. On one side, it will
continue the promising development of foundational and applicative research,
within Theoretical Computer Science, that followed the introduction of Linear
Logic (LL). On the other side, starting from the theoretical results, it will develop
methodologies for the design, the analysis and the verification of paradigmatic
programming languages oriented to applications in the context of mobile
computations with resource guarantees.
The proposal under review have been developed thanks to the collaboration
of all the researchers involved in PROTOCOLLO, and of new ones, particularly
competent about Lambda calculus and Ludics.
PROTOCOLLO has been fruitful in terms of collaboration between its
participants. Collaboration led to numerous publications (project web site
http://protocollo.di.unito.it) concerning investigations about Linear logic and
its possible applications to specific problems inherent to Computer science.
We expect to further increment synergies among researchers to deepen theoretical
investigation, the goal being to apply both the consequences of the
obtained results, and our experience about Lambda calculus to develop specific
methodologies to support design, verification and analysis of paradigmatic
programming languages.
We shall use real issues both to solicit ideas, and, as verification tools,
with respect to the result we shall obtain. Mobile computations in presence
of resource limitations will be our favorite context of reference, which, we notice,
is subject of the European project Mobile Resource Guarantees (MRG)
(http://groups.inf.ed.ac.uk/mrg/) making it evident its relevance. We are con-
fident that our old and new results in the field of implicit computational complexity,
through sub-recursive sub-systems of Linear logic can have fruitful applications
in such a context.


1.4 Durata del Programma di Ricerca    24 Mesi  

1.5 Settori scientifico-disciplinari interessati dal Programma di Ricerca

 

INF/01 - Informatica 
MAT/01 - Logica matematica 


1.6 Parole chiave


Testo italiano

LOGICA LINEARE ; LOGICHE LEGGERE ; LINGUAGGI PARADIGMATICI ; LAMBDA CALCOLO ; COMPLESSITA' COMPUTAZIONALE ; TEORIA DELLA DIMOSTRAZIONE ; RIDUZIONE OTTIMALE ; INTERAZIONE ; MODELLI INTENSIONALI ED ESTENSIONALI


Testo inglese
LINEAR LOGIC ; LIGHT LOGICS ; PARADIGMATIC LANGUAGES ; LAMBDA CALCULUS ; COMPUTATIONAL COMPLEXITY ; PROOF THEORY ; OPTIMAL REDUCTION ; INTERACTION ; INTENSIONAL AND EXTENSIONAL MODELS


1.7 Coordinatore Scientifico del Programma di Ricerca

RONCHI DELLA ROCCA  SIMONETTA 
Professore Ordinario  20/11/1946  RNCSNT46S60B111P 
INF/01 - Informatica 
Università degli Studi di TORINO 
Facoltà di SCIENZE MATEMATICHE FISICHE e NATURALI  
Dipartimento di INFORMATICA  
011/6706734
(Prefisso e telefono)
 
011/751603
(Numero fax)
 
ronchi@di.unito.it
(Email)
 


1.8 Curriculum scientifico


Testo italiano

Simonetta Ronchi Della Rocca dal 1987 e’ professore ordinario di “Fondamenti dell’Informatica” presso l’Universita’ di Torino, Dipartimento di Informatica.
E’ membro del collegio docenti del dottorato in Informatica dell’Universita’ di Torino. In questo contesto e’ stata relatore della tesi di dottorato di Luca Roversi (professore associato presso l’Universita’ di Torino), Luigi Liquori (ricercatore presso l’INRIA a Sophia Antipolis), Alberto Pravato (amministratore delegato della PROSA e professore a contratto presso l’Universita’ di Venezia).
E’ membro dell’Accademia delle Scienze di Torino.

E’ stata membro del Comitato organizzatore del LICS, dal 1992 al 2003.
E’ stata membro del direttivo nazionale del capitolo Italiano dell’EATCS.
E’ stata membro di Comitati di Programma o relatore invitato in alcune conferenze internazionali; tra le piu’ recenti: LICS 92, Logic Colloquium 94, Logic
Colloquium 95, TLCA 99, TLCA 01, ICTCS01.
E’ stata conference co-chair del FLOC99.
E’ editore della rivista "ACM Transactions on Computational Logic".

E’ stata responsabile della sede di Torino in alcuni progetti di ricerca europei (HCM “Typed lambda calculus”, TMR “Linear Logic”) e progetti MIUR (“Sistemi Formali per verifica, sintesi e analisi di programmi”,1997, “Logica Lineare e oltre”, 2000).
E’ attualmente coordinatore nazionale del progetto MIUR “Dalla Prova alla Computazione con la Logica Lineare” (PROTOCOLLO), 2002.

I suoi interessi di ricerca sono nel campo dell’Informatica Teorica, in particolare si occupa di semantica formale di linguaggi di programmazione, logica della programmazione e teorie dei tipi. Si e’ occupata di problemi di inferenza di tipi per tipi intersezione e tipi polimorfi, di semantica operazionale e denotazionale di vari lambda calcoli, di fondazione logica dei tipi intersezione.


Testo inglese
Simonetta Ronchi Della Rocca is full Professor since 1987, teaching "Foundations of Computer Science" at the University of Torino, Departement of Computer Science.

She is in the teaching board of the Computer Science PhD Program of Turin University. In this context, she has been PhD advisor of Luca Roversi (associated professor, University of Turin), Luigi Liquori (INRIA researcher, Sophia Antipolis) and Alberto Pravato (administrator of the factory PROSA and lecturer at the University of Venice).

She is member of the Academy of Science of Turin.

She was member of LICS Organizing Committee, from 1992 until 2003.
She has been member of the national direction of the Italian Council of EATCS.
She has been member of Program Committees and invited speaker for some international conferences, the more recent being : LICS 92, Logic Colloquium 94, Logic
Colloquium 95, TLCA 99, TLCA 01, ICTCS01.
Moreover she has been conference co-chair for LICS 99.
She is editor of the journal "ACM Transactions on Computational Logic".

She has been site leader for UE research Projects (HCM “Typed lambda calculus”, TMR “Linear Logic”) and of MIUR projects (“Formal methods for program verification, synthesis and analysis”, 1997, “Linear Logic and Behind” 2000).
Moreover she is the national coordinator of the MIUR project
“From Proofs to Computation Through Linear Logic” (PROTOCOLLO).

Her research interests are in the field of Theoretical Computer Science, in particular Formal Semantics of Programming Languages, Program Logics and Type Theories. She studied type inference problems both for intersection types and polimorphic types, denotational and operational semantics of various kinds of lambda calculi in different settings, logical foundations of intersection types.


1.9 Pubblicazioni scientifiche più significative del Coordinatore del Programma di Ricerca

1. PAOLINI L.; RONCHI DELLA ROCCA S. (2004). Parametric Parameter Passing Lambda Calculus INFORMATION AND COMPUTATION. (vol. 186 pp. 87-106)  
2. COPPOLA P.; RONCHI DELLA ROCCA S. (2004). Principal Typing for Lambda Calculus in Elementary Affine Logic FUNDAMENTA INFORMATICAE. to appear.  
3. RONCHI DELLA ROCCA S. (2002). Intersection Typed Lambda-Calculus ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE. (vol. 70.1)  
4. RONCHI DELLA ROCCA S.; ROVERSI L. (2001). Intersection Logic LNCS. (vol. 2142 pp. 414-429)  
5. PAOLINI L.; RONCHI DELLA ROCCA S. (1999). Call-by-value Solvability THEORETICAL INFORMATICS AND APPLICATIONS. (vol. 33 pp. 507 -- 534)  


1.10 Elenco delle Unità di Ricerca

Responsabile Scientifico Qualifica Settore Disc. Università Dipartimento Mesi Uomo
1. ABRUSCI VITO MICHELE  Professore Ordinario  M-FIL/02  ROMA TRE  FILOSOFIA  17 
2. MARTINI SIMONE  Professore Ordinario  INF/01  BOLOGNA  SCIENZE DELL'INFORMAZIONE  15 
3. MASINI ANDREA  Professore Ordinario  INF/01  VERONA  INFORMATICA  19 
4. RONCHI DELLA ROCCA SIMONETTA  Professore Ordinario  INF/01  TORINO  INFORMATICA  16 

1.11 Mesi uomo complessivi dedicati al programma


Testo italiano
Numero Mesi uomo
1° anno
Mesi uomo
2° anno
Totale mesi uomo
Personale universitario dell'Università sede dell'Unità di Ricerca  9  94  53  147 
Personale universitario di altre Università  9  91  57  148 
Titolari di assegni di ricerca  1  11  0  11 
Titolari di borse  Dottorato  2  21  12  33 
Post-dottorato  0       
Scuola di Specializzazione  0       
Personale a contratto  Assegnisti  1  0  11  11 
Borsisti  2  5  16  21 
Dottorandi  0       
Altre tipologie  0       
Personale extrauniversitario  1  11  6  17 
TOTALE     25  233  155  388 

Testo inglese
Numero Mesi uomo
1° anno
Mesi uomo
2° anno
Totale mesi uomo
University Personnel  9  94  53  147 
Other University Personnel  9  91  57  148 
Work contract (research grants, free lance contracts)  1  11  0  11 
PHD Fellows & PHD Students  PHD Students  2  21  12  33 
Post-Doctoral Fellows  0       
Specialization School  0       
Personnel to be hired  Work contract  1  0  11  11 
PHD Fellows & PHD Students  2  5  16  21 
PHD Students  0       
Other tipologies  0       
No cost Non University Personnel  1  11  6  17 
TOTALE     25  233  155  388 


PARTE II


2.1 Obiettivo del Programma di Ricerca


Testo italiano

Il progetto si propone come continuazione del progetto cofinanziato MIUR2002
”PROTOCOLLO” (from PROofs TO COmputation through Linear LOgic),
rispetto al quale si pone con un duplice obiettivo. Da un lato, proseguira’ lo
sviluppo di promettenti filoni di ricerca fondazionale e applicativa di informatica
teorica, scaturiti dall’introduzione della Logica Lineare (LL). Dall’altra, a
partire dai risultati teorici, sviluppera’ metodologie per il disegno, l’analisi e la
verifica di linguaggi paradigmatici di programmazione, orientati al contesto di
computazioni mobili con risorse limitate.
Il progetto sara’ organizzato secondo una griglia, strutturata su tre livelli
concettuali.
A livello speculativo si focalizzera’ su ricerche di base per i livelli successivi.
La ricerca sara’ nell’ambito della teoria strutturale della dimostrazione,
dello studio di modelli intensionali ed estensionali di linguaggi paradigmatici di
programmazione, dell’utilizzo della Logica come modello di computazione.
Un secondo livello sviluppera’ metodologie basate sulla logica per studiare
proprieta’ di linguaggi di programmazione. Da un lato, la ricerca al primo
livello su teoria strutturale della dimostrazione e modelli di linguaggi supportera’
metodologie guidate dall’analogia ”proofs-as-programs”; dall’altro la ricerca
speculativa su modelli e logica come modello computazionale mirera’ a metodologie
di studio e sviluppo di linguaggi con cui esprimere proprieta’ tipiche della
teoria della complessita’.
Un terzo livello, di ispirazione e riscontro, ci leghera’ a problematiche reali
usate come sorgente di sollecitazioni e come verifica dei risultati, privilegiando
il contesto delle computazioni mobili con risorse limitate.
La ricerca sara’ organizzata fluidamente attraverso i vari livelli:
(i) dalla base al riscontro (bottom-up): esistono significativi contributi dei
proponenti a livello di base e metodologico. Tuttavia, permangono rilevanti
problemi aperti. Riteniamo che la soluzione di tali problemi, suggerira’
risultati applicabili a livello di riscontro, specie nel contesto di
computazioni mobili menzionato.
(ii) dal riscontro alla base (top-down): la programmazione in presenza di
risorse spazio/tempo limitate e’ fonte di ispirazione. In questo ambito
piu’ che caratterizzazioni di classi di complessita’ o risultati di rappresentabilita’,
interessano specifici linguaggi, ragionevolmente semplici, utilizzabili
come linguaggi di specifica intermedi per la programmazione o la
verifica di sistemi con ristrettezza di risorse. Questi problemi richiedono
nuovi risultati di base e metodologici.
Segue il dettaglio degli obiettivi del progetto.
1. Livello speculativo di base.
Illustriamo tre grandi temi principali di investigazione, riuniti nei livelli
successivi:
1.1 Teoria strutturale della dimostrazione.
La Logica Lineare (LL) [26] e’ stata una delle novita’ piu’ promettenti
nella moderna teoria della dimostrazione. LL e’ una logica
costruttiva che mostra informazioni nascoste negli usuali sistemi formali.
L’esempio tipico e’ la decomposizione dell’implicazione intuizionista
A->B in !A-oB, cioe’ in una implicazione lineare e un operatore
modale ! responsabile delle operazioni di contrazione e indebolimento,
che, computazionalmente, corrispondono a duplicazione
e cancellazione. LL descrive una funzione calcolabile come una sequenza
di duplicazioni/cancellazioni, seguite da una funzione lineare.
Questa visione, grazie al ”morfismo di Curry-Howard”, che relaziona
dimostrazioni logiche e linguaggi funzionali, che ne evidenzano gli aspetti
dinamici, permette di modellare linguaggi di programmazione
con controllo esplicito delle risorse, alla base di risultati anche applicativi
[32].
L’obiettivo di questo livello e’ rispondere a problemi di carattere fondazionale,
partendo dai risultati e dall’esperienza maturata nell’uso
delle tecniche derivate da LL. Da una lato interessano logiche derivate
da LL: (i) quelle ”leggere”, frammenti di LL, con complessita’ di
eliminazione del taglio intrinsecamente limitata; (ii) quella non commutativa;
(iii) logiche disegnate per modellare specifiche proprieta’
dinamiche. Dall’altro vogliamo indagare su nuove tecniche di teoria
della dimostrazione ricavate dalla Ludica [31], un ambiente astratto
per la teoria della dimostrazione, costruito sulla nozione di interazione.
Essa sviluppa idee presenti sia in geometria dell’interazione,
sia nella semantica dei giochi e potrebbe essere applicata allo studio
di concorrenza, interazione e sincronizzazione tra processi.
1.2 Modelli intensionali ed estensionali di linguaggi paradigmatici di programmazione.
La ricerca sara’ di tipo fondazionale. Svilupperemo tecniche per la
caratterizzazione di proprieta’ estensionali/intensionali di programmi.
Nella linea degli studi sul lambda-calcolo svilupperemo tecniche di
dimostrazione su linguaggi paradigmatici, interessandoci, particolarmente,
allo studio di modelli semantici e alla definizione di modelli
”fully abstract”. Gli strumenti che useremo sono basati essenzialmente
sulla logica (semantica dei giochi, filtri modelli disegnati a
partire da assegnazioni di tipo intersezione).
1.3 La logica come modello di computazione.
Le logiche ”leggere” caratterizzano classi di complessita’ modulo una
codifica dei dati scelta. In particolare, siamo esperti di Light Affine
Logic (LAL) [10] ed Elementary Affine Logic (EAL) [8, 20, 21] , che
caratterizzano rispettivamente le computazioni polinomiali e le computazioni
elementari. Intendiamo procedere secondo due linee. Da un
lato studieremo sia l’espressivita’ delle logiche leggere al variare delle
classi di codifica dei dati sia la relazione tra i sottosistemi subricorsivi
di LL e i sistemi subricorsivi disegnati a partire da altri principi,
come, ad esempio, la teoria della ricursione. Dall’altro, in vista delle
possibili applicazioni, siamo interessati a sistemi di assegnazione di
tipo decidibili e automatizzabili per linguaggi paradigmatici; i tipi
saranno formule di logiche leggere, che garantiscono una complessita’
computazionale limitata.
2. Livello metodologico
L’interesse per i problemi fondazionali affrontati al livello 1 segue l’ottica
di sviluppare metodologie di programmazione suddividibili in due classi:
2.1 Metodologie ”Proofs as Programs”.
Tali metodologie si svilupperanno dai risultati dei punti 1.1 e 1.2.
Svilupperemo linguaggi paradigmatici che ereditino le proprieta’ dinamiche
delle logiche sviluppate, usando la tecnica della decorazione
”proofs-as-programs”. Arricchiremo, quindi, tali linguaggi per produrre
linguaggi prototipali, di cui studiare l’implementazione.
2.2 Metodologie specifiche per linguaggi con complessita’ predefinita.
Tali metodologie si svilupperanno dai risultati dei punti 1.2 e 1.3.
A causa della loro peculiarita’, le proprieta’ dinamiche delle logiche
”leggere” vanno sfruttate con tecniche specifiche. L’obiettivo e’ disegnare
linguaggi ”amichevoli” per una programmazione che garantisca
un limite superiore alla complessita’ dei programmi. Una linea di
ricerca alternativa e complementare consiste nel controllare la complessita’
tramite sistemi di assegnazione di tipo, estendendo i risultati
del punto 1.3.
3. Livello di riscontro.
La diffusione della computazione mobile ha introdotto nuovi problemi,
tra i quali la necessita’ di garantire un limite quantitativo alle risorse
di calcolo necessarie per l’esecuzione. L’importanza di tale problema
e’ testimoniata dal progetto Global Mobile Resource Garantees (MRG)
(http://groups.inf.ed.ac.uk/mrg/). Finora i risultati ottenuti in quest’ambito
si basano su risultati fondazionali, ottenuti nell’area della teoria della ricorsione,
usata per caratterizzare classi di complessita’. Al contrario, non
risultano proposte esplicitamente ispirate alle logiche ”leggere”. Questa e’
un’ulteriore ragione, pratica, per indagare in questa direzione.


Testo inglese
This project is proposed like a continuation of MIUR2002 PROTOCOLLO
project (from PROofs TO COmputation through Linear LOgic), and it is placed,
regarding the previous one, with a twofold objective. On one side, it will
continue the promising development of foundational and applicative research,
within Theoretical Computer Science, that followed the introduction of Linear
Logic (LL). On the other side, starting from the theoretical results, it will develop
methodologies for the design, the analysis and the verification of paradigmatic
programming languages oriented to applications in the context of mobile
computations with resource guarantees.
Our project is structured in three conceptual levels.
A foundational level will focus on basic research from which developing other
levels. We shall work on structural proof theory, on the study of intensional and
extensional models of paradigmatic programming languages, and on the logic
as a computational model.
A methodological level will develop specific methodologies, based on logic, to
study properties of programming languages. A speculative research about both
structural proof theory and models of languages will support methodologies of
study, guided from the analogy ”proofs-as-programs”. A speculative research
on both models and logic as computational model will aim for methodologies
of study and development of languages that, implicitly, express concepts of
complexity theory.
An applicative level will be both an inspiration and testing bed. It will link
us to real issues soliciting ideas and playing as a verification tool of the obtained
results. To such aim, our favorite reference will be mobile computations with
resource limitations.
The research will fluidly develop through the above levels: from the speculative
toward the testing one (bottom-up), and viceversa (top-down). Specifically:
(i) bottom-up flow: our group already contributed significantly to the speculative
and methodological levels where open problems still exist. We think
that basic and methodological investigation, finalized to solving them will
suggest results applicable to case studies at the application level, in mentioned
application context;
(ii) top-down flow: a source of real computational problems is programming
with limited resources, typically time and space. Neither characterizations
of complexity classes, nor results about representation power, are of great
interest in this case. Rather, the quest is about specific and friendly
languages, usable for the verification of systems with resource constraints.
These requirements inspire and demand new basic and methodological
results.
Next, we structure our goals in accordance with the pattern we already gave.
1. Level: foundations.
1.1 Structural proof theory.
LL [26] is one of the main promising novelties since the
introduction of modern proof theory. LL is a constructive logic that
shows information normally hidden inside usual formal systems. The
standard example of this is the decomposition of intuitionistic implication
A->B as !A-oB: one linear implication and a modal operator
! responsible of contracting or weakening assumptions. By applying
”Curry-Howard morphism”, relating logical deductions and programming
languages, a computable function is a composition of one
duplication/erasing operation followed by a linear transformation.
This new vision over logical operators allows to model programming
languages with an explicit control over the resources. Moreover, the
proof nets, a graphical representation of LL deductions [26],
put in evidence the dynamic, or computational, aspect of logic, and
are the base of important results like, for example, [32], which has
an applicative flavor.
Our objective here is to answer open foundational questions, starting
from known results and using the experience matured in the use of
the techniques derived from LL. We want to study logical systems
derived from LL: on one side ”light” ones, obtained as fragments
of LL whose cut elimination cost is intrinsically limited, and, to the
other side, Non Commutative Linear Logic. Moreover, we want to
use tools defined after the introduction of LL to study new logical
systems, to model specific dynamic properties. We aim also to investigate
on new proof theoretical techniques Ludics [31] suggests.
It abstractly reformulates proof theoretical principles in terms of the
notion of interaction. It develops ideas already known in geometry of
the interaction, in game semantics and could be applied to the study
of concurrency, interaction and synchronization between processes.
1.2 Intensional and extensional models of paradigmatic programming
languages.
Also in this topic, we aim at foundational goals. We mean to develop
abstract techniques for the characterization of extensional and
intensional properties of programs. In particular, we want to define
paradigmatic languages for developing proof techniques on lambda
calculus tradition. Our main interests are about the relation between
extensional and intensional properties, the study of semantic models
and the identification of those which are ”fully abstract”. The tools
we want to use are based on topology and logic, like games semantics
and filter models, designed from intersection types.
1.3 Logic as a computational model.
”Light” logics characterize complexity classes modulo a given data
representation. We are particularly expert about Light Affine Logic
(LAL) [10] and Elementary Affine Logic (EAL) [8, 20, 21] characterizing
polynomial and elementary computations, respectively. The
foundational problems that we want to study develop essentially after
two lines. One is about both the expressivity of ”light” logic,
as a function of the chosen data representation, and the relation between
the subrecursive subsystems of LL and subrecursive systems
designed after other traditions, like, as an example, recursion theory.
The other line, somewhat more applicative oriented, is about decidable
type assignment systems for paradigmatic languages, where the
types are formulas of some ”light” logic, implicitly guaranteeing a
limited computational complexity.
2. Level: methodology .
The interest about the foundational problems faced by level 1 aims to
develop programming methodologies that can be subdivided in two classes:
2.1 Methodologies ”Proofs as Programs”.
Such methodologies will be developed starting from the results of
points 1.1 and 1.2. The dynamic properties of interesting logical systems
will allow to look for the definition of paradigmatic languages
that inherit such properties, using the standard technique of decorating
derivations with suitable terms. Later on, such languages can
be enriched, so as to produce prototypes of which implementations
can be studied.
2.2 Specific methodologies for languages with predefined complexity.
Such methodologies will be developed starting from the results obtained
at points 1.2 and 1.3. Because of their peculiarity, the dynamic
properties inherent to ”light” logics, require to be exploited by specific
techniques. The objective is to design programming languages
which must be more ”friendly” than those currently available to program
algorithms that guarantees to preserve a given computational
limit. An alternative and complementary research line is to control
complexity through type inference, and we would want here to extend
results obtained at point 1.3.
3. Level: application.
A relevant problem about mobile computations is to predict and guarantee
the necessary resources to execute them. Mobile Resource Guarantees
(MRG) (http://groups.inf.ed.ac.uk/mrg/) is a European project
completely dedicated to such a problem, making it evident its relevance.
Up to now results obtained on the subject are based on foundational results
rooted in the area of the recursion theory. On the contrary, we are
not aware of results stemmed out of ”light” logics. This is a further,
practical, reason to start investigating in this direction.


2.2 Base di partenza scientifica nazionale o internazionale


Testo italiano

Il progetto, come e’ gia’ chiaro dal punto Obiettivo , si pone nel solco di
una doppia tradizione scientifica:
(1) da una parte il lambda-calcolo, con e senza tipi, come strumento paradigmatico
per lo studio ed il progetto di linguaggi di programmazione;
(2) dall’altra LL e logiche derivate da LL, come strumento privilegiato per
l’indagine delle caratteristiche computazionali dei linguaggi di programmazione,
incluso il lambda-calcolo stesso.
Nel seguito presenteremo le nostre basi di partenza scientifiche secondo lo
schema gia’ utilizzato nel punto Obiettivo, suddividendo ogni tema in sottotemi
per chiarezza di esposizione. Abbiamo ridotto all’essenziale le referenze,
per problemi di spazio; referenze piu’ dettagliate possono essere consultate nei
progetti delle varie unita’ del progetto.
1. Livello speculativo di base
1.1 Teoria strutturale della dimostrazione.
– Logica Classica
Lo studio della Logica Lineare ha influenzato il modo di considerare
altre logiche, come ad esempio la Logica Affine [14],
le Logiche con MIX [13] e la Logica Classica, ponendo particolare
enfasi sugli aspetti computazionali [28, 25]. Un approccio
importante alla logica classica (con enfasi sul cosiddetto “continuation
passing style”) e’ quello del lambda-mu-calcolo [54],
un’estensione della formulazione usuale della logica classica ottenuta
tramite un sistema di deduzione naturale etichettato a
conclusioni multiple. Un esempio di uso delle reti di prova per
studiare gli aspetti dinamici della Logica Classica e’ in [59].
– Moduli
Oltre che per la loro natura geometrica, le reti di prova sono un
formalismo interessante per la costruzione di sistemi dimostrativi
modulari. Le prime caratterizzazioni locali dei moduli sono
state date in [27]. Queste definizioni sono basate rispettivamente
sulle permutazioni e le partizioni delle formule del bordo. Maieli
e Puite [50] hanno recentemente definito un algoritmo per calcolare
il tipo di un modulo. Questi risultati non sono stati ancora
estesi al frammento moltiplicativo e additivo di LL (MALL) e
alla logica non commutativa NL (cfr. sotto). Nel caso di MALL,
il problema principale e’ l’assenza di criteri di correttezza semplici
e soddisfacenti per i proof-nets [29]. I lavori sulla logica
polarizzata e il nuovo criterio di correttezza per MALL in [38]
rendono possibile un nuovo approccio al problema della modularit.
L’estensione a NL sembra piu’ problematica. In questo
caso, degli aiuti potrebbero arrivare dai recenti risultati sulla
relazione tra ”focalizzazione” e costruzione di proof-nets [6].
– Logica non commutativa
La logica non commutativa NL [3] e’ una estensione conservativa
di entrambe le logiche lineare e ciclica [67, 2], quest’ultima
e’ una estensione classica del calcolo di Lambek. Il frammento
piu’ interessante di NL e’ quello moltiplicativo MNL, in cui abbiamo
sia la versione commutativa che non commutativa dei due
connettivi moltiplicativi par e tensore.
– Tipi Intersezione
La tradizione metodologica della teoria della dimostrazione ha recentemente
permesso di dare qualche risposta al problema di dare
una fondazione logica ai tipi intersezione. In [62], si e’ definito un
connettivo logico con la stessa semantica della congiunzione dei
tipi intersezione, che si colloca tra la usuale congiunzione intuizionista
e la congiunzione tensoriale di LL. La proposta di [62] e'
alternativa a [19] in cui, con lo stesso scopo “proof-teoretico”, si
e' introdotta un’opportuna logica, basata su stringhe di formule
di LJ. [62] si ispira infatti alla metodologia della teoria della
dimostrazione, scaturita da LL, con lo scopo di cercare il signi-
ficato del tipo intersezione, attraverso una scomposizione della
congiunzione intuizionista, ritenuta primitiva in [19].
– Ludica
La ludica [31] e’ un ambiente astratto per teoria della dimostrazione
costruito sulla nozione di interazione;
sviluppa idee presenti sia nella geometria dell’interazione che
nella semantica dei giochi [40]. Il ruolo centrale che hanno i
nomi (invece che le formule) e i metodi interattivi avvicinano
la teoria alla concorrenza. Tuttavia, in [31] il calcolo e’ ancora
strettamente sequenziale.
– Sistemi polarizzati
I sistemi polarizzati sono un ponte tra la logica classica e quella
lineare [28, 46], in particolare tra le reti di prova e il lambdamu
calcolo [54]. Una dettagliata analisi nella teoria della dimostrazione
della corrispondenza tra logica classica ed LL era
gia’ stata data in [25] : il lavoro sui sistemi polarizzati getta pero’
nuova luce sull’interpretazione computazionale di tale corrispondenza
e, da un punto di vista semantico, sulle sue connessioni
con la semantica dei giochi.
1.2 Modelli intensionali ed estensionali di linguaggi paradigmatici di programmazione.
– Disegno di linguaggi paradigmatici
[53] introduce una visione del lambda calcolo, basata sulla parametrizzazione
del concetto di valore di ingresso. Il lambda calcolo
classico e quello con chiamata per valore di Plotkin sono istanze
del calcolo parametrico menzionato. Esso permette di dimostrare
uniformemente alcune proprieta’ sintattiche, di definire
uno schema di macchina operazionale parametrica che sussume
tutte le piu’ note semantiche operazionali del lambda calcolo non
tipato, di definire modelli estensionali parametrici.
– Modelli denotazionali
La costruzione di raffinati modelli matematici di linguaggi di
programmazione funzionale, e del lambda-calcolo in particolare,
costituisce un’area di ricerca di lunga data. Due sono le linee di
indagine a cui siamo interessati. La prima si pone il problema
della costruzione di modelli estensionali che riflettano esatta-
mente il comportamento operazionale del linguaggio (cioe’ modelli
“fully abstract”) ; risultati parziali nel campo del lambda
calcolo e di PCF sono in [1, 39, 17, 52]. Particolare interesse
ha la nozione di filtro-modello, basato sui tipi-intersezione, che
sono un potente strumento per ragionare in modo finitario sulla
semantica dei linguaggi di programmazione in diversi contesti
matematici. La flessibilita’ di tali tipi ha permesso di modellare
diverse proprieta’ intensionali dei lambda-temini (terminazione
debole e forte, easiness, ... ). Si vedano, in particolare, [4] [37].
La seconda linea di ricerca indaga sulle proprieta’ del modello
stesso, e in particolare sull’esistenza di un linguaggio che le ri-
fletta esattamente. Sono stati analizzati modelli basati su diverse
costruzioni funzionali [49, 58]. Un problema collegato e’ quello
della completezza dei modelli rispetto alle lambda teorie. Salibra
in [63] ha recentemente introdotto una nuova tecnica per
dimostrare in modo uniforme l’incompletezza di tutte le semantiche
denotazionali proposte fino ad ora per il lambda calcolo.
In [18] sono state caratterizzate le lambda teorie che non sono
indotte da un qualche modello di semantiche del lambda calcolo
dato in termini di modello di grafi.
– Controllo delle Risorse nel lambda-calcolo
Tecniche basate su logiche leggere saranno prese in considerazione
nel punto 1.3. Ci sono pero’ tecniche usate nel lambdacalcolo
per controllare le risorse che non sono state completamente
sfruttate nell’ambito di LL. L’eta-regola del lambda calcolo
puo’ essere considerata come un mezzo per controllare l’allocazione
(essenzialmente statica) delle risorse computazionali. Una tale
interpretazione ha portato alla definizione di un calcolo sensibile
alle risorse [57]. Inoltre, puo’ essere utilizzata un’opportuna
nozione di forma eta-espansa, come in [KP00], per ottenere un’analisi
precisa della beta-riduzione in termini di interazione tra funzione
e argomento, in un modo che ha interessanti analogie con la semantica
dei giochi.
1.3 La Logica come modello di computazione.
La decomposizione dell’implicazione intuizionista che abbiamo citato
nel punto Obiettivo mette a disposizione un potente strumento di
analisi delle computazioni, a vari livelli di dettaglio. Sottolineiamo
qui due aspetti che tale strumento rende possibili – relativi soprattutto
all’analisi delle nozioni di duplicazione e di sostituzione: (i)
un’analisi locale di tali nozioni; (ii) un’analisi sub-ricorsiva della complessita’
di tali operazioni. Il primo aspetto citato e’ quello che ha
interpretato la riduzione ottimale alla Levy come un procedimento
di normalizzazione della logica lineare[7, 33] e che ha permesso di ottenere
importanti risultati di caratterizzazione della complessita’ intrinseca
di tale tecnica [9, 8]. Il secondo aspetto citato, invece, ha por-
tato alla definizione di diversi frammenti della LL — la logica lineare
leggera (LLL), la logica affine leggera (LAL), la logica affine/lineare
elementare (ELL, EAL), la logica ”soft” (SLL e SAL) . Tali logiche
sono state studiate in letteratura sotto vari aspetti e ne conosciamo
oggi molte caratteristiche. In particolare: (i) sono state indagate
varie varianti sintattiche di presentazione, tra cui [30, 10, 44]; (ii)
ne sono state studiate diverse semantiche matematiche, dimostrando
come sottoprodotto la decidibilita’ delle versioni affini [41, 23] (iii) e’
stata studiata in dettaglio la normalizzazione, dimostrando in particolare
la normalizzazione forte di alcune di esse [64]; (iv) sono state
studiate le proprieta’ di rappresentazione di tali logiche, qualche volta
ottenendo dei risultati apparentemente sorprendenti; in particolare
[51] mostra come LAL, senza restrizioni sulla nozione di “rappresentazione”,
e’ completa per p-space. Ma, nonostante gli sforzi effettuati,
non si e’ trovata ancora una diretta relazione tra i sottosistemi
ricorsivi di LL, come quelli sopra menzionati, e sistemi subricorsivi
disegnati a partire da altri principi, come, ad esempio, la teoria della
ricursione [12, 34, 35]. In [24] e' stato fatto un passo avanti in questa
direzione, con l’introduzione di HOLRR— un lambda-calcolo lineare,
esteso con costanti e un ricursore R, in cui si pu`o immergere
direttamente la ricursione ramificata di Leivant [48].
2. Livello metodologico
2.1 Metodologie “Proofs-as-Programs”
Il morfismo di Curry-Howard pone formalmente le basi della corrispondenza
tra dimostrazioni logiche e linguaggi funzionali, basata
sull’uso delle formule logiche come tipi per linguaggi funzionali, e
definisce quindi una nuova metodologia di disegno di linguaggi. Nell’ambito
di LL e logiche correlate, citiamo tra gli altri il linguaggio disegnato
in [15] a partire dal frammento moltiplicativo di LL e quello in [61]
che codifica anche il frammento additivo. Inoltre una interessante
applicazione di tale metodologia e’ in [60], che ha ottenuto un linguaggio
tipato con i tipi intersezione come decorazione della logica
IL [62].
2.2 Metodologie per linguaggi con complessita’ limitata
Le tecniche logico formali che abbiamo discusso sub (1.3) forniscono
ottimi strumenti metodologici per l’analisi ed il progetto di linguaggi
con complessita’ limitata. Ricordiamo qui le tecniche che piu’ ci interessano.
(i) In primo luogo, il sistema formale EAL gode della
seguente proprieta’: ogni lambda-termine che abbia un tipo in EAL
puo’ essere ridotto secondo la riduzione ottimale di Levy in un modo
particolarmente semplice (“senza l’oracolo”) ed efficiente. Ne segue
che e’ particolarmente interessante avere delle tecniche automatich
per inferire un tipo EAL per programmi funzionali, un tema studiato
in [20] e [21]. (ii) Il controllo delle duplicazioni che si ottiene
con LLL/LAL non e’ l’unica soluzione; e’ possibile usare tecniche
classiche alla Leivant/Bellantoni-Cook ([48, 47, 12] ) per ottenere
sistemi formali con una base di lambda-calcolo e varie estensioni, in
specie con ricorsione, che costituiscono una base paradigmatica per
linguaggi di programmazione [34, 24].
3. Livello di riscontro
La letteratura presenta esempi interessanti di lavori in cui concetti scaturiti
dalla speculazione di base sono stati adattati e trasportati in ambiti
piu’ applicativi nei quali e’ possibile sia valutarne l’impatto effettivo, sia
trarne ulteriore stimolo per possibili approfondimenti dei concetti di base.
[65, 43, 36] sono solo alcuni esempi, cui vorremo ispirarci, specialmente per
quanto riguarda le metodologie ivi utilizzate. Essi sono focalizzati sullo
studio delle corrispondenze tra concetti base della LL e nozioni ormai standard
nell’ambito della costruzione di interpreti/compilatori efficienti per
linguaggi funzionali, quali l’update-in-place, la deallocazione della memoria
per evitare la garbage-collection, l’in-line optimization.” In particolare,
gli studi sulla connessione tra riduzione ottimale e la geometria delle Interazioni
hanno gia’ portato a due implementazioni: BOHM (Bologna Optimal
Higer-order Machine) [9], una implementazione diretta delle riduzioni
”sharing graph” del lambda calcolo introdotte in [45, 32], e PELCR (Parallel
Enviroment for the Optimal Lambda Calculus Reduction)[55], una
implementazione delle riduzioni ottimali basate su di un mix di diverse
tecniche classiche usate nei calcoli paralleli e distribuiti.


Testo inglese
The project, as it should be clear from the point “Obiettivo”, stems
from two well established scientific traditions: (1) on one side we have the
lambda-calculus, with and without types, as a paradigmatic tool for the study
and design of programming languages; (2) on the other we have several logics
derived from LL, as privileged tool for the study of the computational properties
of programming languages, including the lambda-calculus itself.
The results in the literature on which our research project is based will be
presented according to the general scheme already used in the point “Obiettivo”,
and each research theme will be further divided in different topics, for clarity.
1. Level: foundations
1.1 Structural proof theory.
– Classical Logic.
The study of Linear Logic has affected the way of looking at
other logics such as Affine Logic [14], Logics with MIX [13] and
Classical Logic, providing a particular emphasis on the computational
aspects. For instance, Bierman and Urban find a term
assignment for classical sequent calculus which yields strong normalization
for a non-deterministic notion of computation. The
main goal in [66] was to capture those dynamical aspects of computations
that are distinctive of classical logic [28, 25]. An important
approach to classical logic (with emphasis on the so called
“continuation passing style”) is given by lambda-mu-calculus, an
extension of the usual formulation of classical logic by means of
a labeled multi-conclusion natural deduction system. Examples
of the use of proof-nets for studying classical logic are in [59].
– Modules..
Apart for their appealing geometrical nature, proof nets are an
interesting formalism for the construction of modular proof systems.
The first local characterization of modules were given in
[27]. These definitions were based on permutations and partitions
over the border (formulas), respectively. Maieli and Puit
[50] have recently given an algorithm for computing the type of
a module. However, such results have not been extended yet to
the multiplicative and additive fragment of LL (MALL) and to
non-commutative logic NL (see below). In the case of MALL, the
main problem was the absence of simple and satisfying correctness
criteria for MALL proof-nets [29]. The works on polarized
logic and the new definition of a correctness criterion for MALL
proof nets [38] make possible a new approach to the general problem
of modularity. The extension to NL seems more problematic.
In this case, some help should arrive from the recent results on
the relations between ”focusing” and proof net construction [6].
– Not commutative Logic.
Non commutative logic NL [3] is a conservative extension of both
Linear and Cyclic Logic [67, 2]. The most interesting fragment
of NL is the multiplicative one MNL, in which there are both a
commutative and a non-commutative version of the two multiplicative
connectives par and tensor.
– Intersection Types.
The methodological tradition of structural proof-theory recently
allowed to start giving some answers to the problem of giving
logical foundation to the Intersection types (IT), a very expressive
tool to investigate semantics of programming languages, in
heterogeneous mathematical settings. [62] defines a logical connective,
semantically equivalent to the conjunction of IT, which
sits in between both standard conjunction and tensor of LL, and
which is obtained by a decomposition of the standard conjunction.
[62] is alternative to [19] that gives an analogous result
by using sequences of formulae of Intuitionistic logic (LJ), while
keeping the notion of standard conjunction primitive.
– Ludics.
Ludics [31] is an abstract setting for proof-theory built on the
notion of interaction [40]. It develops ideas from both Geometry
of Interaction and Games Semantics. The central role of names
(rather than formulas) and the interactive methods open a bridge
with concurrency theory. However, computation in [31] is still
sequential.
– Polarized Systems.
Polarized systems are a bridge between linear and classical logic
[28, 46], in particular between proof nets and lambda-mu-calculus
[54]. A proof theoretic detailed analysis of the correspondences
between classical logic and LL were already given in [25], but
the work on polarized systems add relevant insights on the computational
interpretation of that correspondences and, from the
semantical point view, on the connections with games semantics.
1.2 Intensional and extensional models of paradigmatic languages.
– Paradigmatic languages design.
[53] introduces a new lambda calculus parameterized with respect
to a set of input values. The idea is that a calculus can
be defined by modeling the application of a function to its argument
using a rewriting rule that fires only when the argument
belongs to the chosen values. Standard lambda calculus and its
call-by-value version can be viewed this way. Moreover, parametric
lambda calculus is a framework to prove uniformly syntactic
properties, like confluence and standardization, of its instances.
Also, it implies a parametric definition of operational semantics
that subsumes all known instances of those kind of semantics
for untyped lambda calculus. As expected, also the definition of
extensional models can be made parametric.
– Denotational models.
The construction of sophisticated mathematical models of functional
programming languages, and of lambda-calculus in particular,
is a well established research area. In the last ten years,
there has been much work on the use of such semantical techniques
for the the study of non-trivial properties of programs
(for general results in [37].) In this field we are interested to two
specific topics. The first is the problem of building extensional
models who mimic exactly the operational behavior of the language
(i.e., “fully abstract” models): partial results in the field
of lambda calculus and of PCF are in [1, 39, 17, 52]. Particularly
interesting has the notion of “filter model”, based on intersection
types, which are a powerful tool for reasoning in a finitary way on
the programming languages semantics in different mathematical
settings. Thanks to the flexibility of intersection types interesting
intensional properties of lambda terms have been proved
(strong and weak normalization, easiness,...) [4]. The second
field is the investigation on the properties of the models themselves,
and in particular on the existence of a language reflecting
exactly the properties of a given model. Different models have
been studied from this point of view, based on different functional
constructions [49, 58]. A related problem is the completeness of
models with respect to lambda theories. Salibra, in [63] has recently
introduced a new technique for proving in a uniform way
the incompleteness of all the proposed denotational semantics
for lambda calculus. In [18] the lambda theories not induced by
graph models have been characterized. Moreover, the innovative
approach, as introduced by Ludics [31, 26], for specifying
infinitary deductive systems, where intensional and extensional
notions coexist, is adapted to models of parametric lambda cal-
culus.
– Resources control in lambda calculus
Techniques based on light logics will be taken into account in the
point 1,3. However, there are some techniques used in lambdacalculus
for controlling resources that have not been completely
exploited in the LL setting. For instance, the eta-rule of lambdacalculus
can be considered as a device for controlling the (substantially
static) allocation of computational resources. Such an
interpretation has led to the definition of resource-aware calculi
[57]. Moreover, the use of the eta-rule in its expansive version
has been used to prove properties of type assignment systems
in a polymorphic setting and to prove normalization results in a
purely syntactical way. Indeed, a suitable notion of eta-long form
can be used, as in [42], to provide a fine analysis of beta-reduction
in terms of the interaction between function and argument, in a
way which has interesting similarities with game semantics.
1,3 Logic as computational model
The decomposition of intuitionistic implication we have mentioned in
the point “Obiettivo” is a powerful tool in the analysis of computations,
at several levels of details. We stress here two issues - related
to the notions of duplication and erasing - which can be dealt with:
(i) a local analysis of these notions. Erasing and duplication are usually
understood as global, meta-level notions. The availability in the
terms (proof-nets) of fine information on the border of regions to be
duplicated/erased allow for a local analysis and accountability of the
involved resources;
(ii) a sub-recursive analysis of the complexity of these operations,
with the goal to suggest and study formal systems in which the complexity
of normalization is bounded (for instance by an elementary,
or a polynomial, function). As for (i), the optimal reduction la Le’vy
has been understood as the normalization process of linear logic. This
interpretation has given several important results characterizing the
intrinsic complexity of the optimal reduction technique (see[7, 33] for
several local interpretations of LL normalization; and [9, 8] for complexity
results.) The research direction mentioned in (ii) has lead to
the definition of several fragments of LL – Light linear and affine
logics (LLLand LAL), Elementary linear and affine logics (ELLand
EAL), Soft logics (SLL and SAL). These logics has been studied
in the literature under several aspects and we nowadays know them
quite well. In particular:
(i) several syntactic variants have been investigated[30, 10, 44];
(ii) several semantics have been studied, obtaining – as a byproduct
– the decidability of their affine versions[41, 23];
(iii) normalization has been studied in detail, proving, in particular,
strong normalization properties for some of them[64];
(iv) the representation properties of these logics have been studied,
with the aim to understand some subtle issues in the coding techniques
(see[51, 22]; in particular[51] shows that LAL, without restrictions
on the coding, can simulate doubly exponential time).
Moreover, despite many efforts, no satisfactory direct relation exists
between sub-recursive sub-subsystem of LL, as those mentioned
above, and any sub-recursive system designed after other principles,
like, for example, recursion theory [12, 34, 35]. [24] makes a step
forward in this direction, introducing HOLRR— a purely linear
lambda-calculus, extended with constants and a higher-order recursor
R, where Leivant’s Ramified recursion [48] embeds directly.
2. Level: methodology
2.1 Methodologies “Proofs-as-Programs”.
The ”Curry-Howard morphism”, relating logical proofs and functional
languages, constitutes a methodology of reference to design
paradigmatic programming languages. In the LL and related logics
setting, we recall just [15] coding the multiplicative fragment of LL,
and [61] which deals also with the additive fragment. Moreover an
interesting application of this methodology is in [60], where a language
typed with intersection types has been obtained as decoration
of the logic IL [62].
2.2 Specific methodologies for languages with predefined complexity.
The formal techniques we discussed under (1.3) give us powerful tools
for the analysis and design of languages with bounded complexity.
We will recall the techniques we are interested in. (i) The formal
system EAL enjoys the following property: Any lambda-term with a
type in EAL can be reduced under the Le’vy’s optimal reduction in
a particularly simple and efficient way (without the “oracle”). As a
consequence, it is very interesting to have automatic techniques for
the inference of EAL types for functional programs, see[20] and[21].
(ii) The control of duplication we obtain with LLL/LAL is not the
only possible solution to control execution time. One could use classical
techniques la Leivant/Bellantoni-Cook ([48, 47, 12] ) to obtain
formal systems based on lambda-calculi extended with recursion.
These systems can be seen as a paradigmatic basis for programming
languages [34, 24].
3. Level: application There are interesting examples in the literature of theoretical
notions that have been transferred in more applicative settings,
where it has been possible both to test their usability and to have back
further foundational problems. [65, 43, 36] are just some examples. They
explored the correspondence between basic notion of LL and standard
notions at the basis of the compiler/interpreter construction for functional
languages, as the update in place, the memory deallocation to avoid
garbage collection, the optimization in line. In particular, the studies on
the relation between optimal reduction and Geometry of Interactions gave
rise to two implementations: BOHM (Bologna Optimal Higer-order Machine)
[9], a direct implementation of the “sharing graph” reductions of
lambda-calculus introduced in [45, 32], and PELCR (Parallel Environment
for the Optimal Lambda Calculus Reduction)[55], an implementation of
the optimal reduction based on a mix of different techniques used in distributed
and parallel calculi.


2.2.a Riferimenti bibliografici

[1] S. Abramsky, P. Malacaria, and R. Jagadeesan. Full abstraction for PCF.
IC, 163:409–470, 2000.
[2] V.M. Abrusci. Noncommutative proof nets. In Adv. in lin. logic (222).
Cambridge Univ. Press, 1995.
[3] V.M. Abrusci and P. Ruet. Non-commutative logic. I. The multiplicative
fragment. Ann. Pure Appl. Logic, 101:29–64, 2000.
[4] F. Alessi, M. Dezani-Ciancaglini, and F. Honsell. Filter models and easy
terms. In ICTCS, LNCS(2202:17-37), 2001.
[5] J.M. Andreoli. Focussing and proof construction. Ann. Pure Appl. Logic,
107:131–163, 2001.
[6] J.M. Andreoli, R. Maieli, and P. Ruet. Constraint-based proof construction
in non commutative logic. TCS, 2004. To appear.
[7] A. Asperti. Linear logic, comonads and optimal reduction. Fund. Inform.,
22:3–22, 1995.
[8] A. Asperti, P. Coppola, and S. Martini. (Optimal) duplication is not elementary
recursive. In 27th SIGPLAN-SIGACT, pages 96–107. ACM, 2000.
[9] A. Asperti and S. Guerrini. The optimal Implementation of Functional
Programming Languages. Cambridge Tracts in TCS, 45. Cambridge Univ.
Press, 1998.
[10] A. Asperti and L. Roversi. Intuitionistic light affine logic. ACM Trans. on
Comp. Logic, 3:1–39, 2002.
[11] P. Baillot. Type inference for polynomial time complexity via constraints
on words. TCS, 2004. To appear.
[12] S. Bellantoni and S. Cook. A new recursion-theoretic characterization of
the polytime functions. Comp. Compl., 2:97–110, 1992.
[13] G. Bellin. Subnets of proof-nets in multiplicative linear logic with MIX.
MSCS, 7:663–699, 1997.
[14] G. Bellin. Two paradigms of logical computation in affine logic? In Logic
for Concurrency and Synchronisation, 18:115-150. Kluwer Academic, 2003.
[15] N. Benton, G. Bierman, V. de Paiva, and M. Hyland. A term calculus for
intuitionistic linear logic. In TLCA. LNCS, 664:75-90, 1993.
[16] A. Berarducci and B. Intrigila. Church-rosser -theories, infinite -terms
and consistency problems. In Logic Colloquium ’93. Oxford Univ. Press,
1996.
[17] A. Bucciarelli and T. Ehrhard. Sequentiality in an extensional framework.
IC, 110:265–296, 1994.
[18] A. Bucciarelli and A. Salibra. The minimal graph model of lambda calculus.
In 28th Inter. Symp. on Math. Found. of CS, LNCS, 2747:300-307, 2003.
[19] B. Capitani, M. Loreti, and B. Venneri. Hyperformulae, parallel deductions
and intersection types. ENTCS, 50, 2001.
[20] P. Coppola and S. Martini. Typing lambda terms in elementary logic with
linear constraints. In 5th TLCA, LNCS, 2044:76-90, 2001.
[21] P. Coppola and S. Ronchi della Rocca. Principal Typing in Elementary
Affine Logic. In 7th TLCA, LNCS, 2701:90-104, 2003.
[22] U. Dal Lago. On the expressive power of light affine logic. In 8th ICTCS,
LNCS, 2841:216-227, 2003.
[23] U. Dal Lago and S. Martini. Phase semantics and decidability of elementary
affine logic. TCS, 2004. To appear.
[24] U. Dal Lago, S. Martini, and L. Roversi. Higher-order linear ramified
recurrence. In 3th Types for Proofs and Programs, LNCS, 2004. to appear.
[25] V. Danos, J.B. Joinet, and H. Schellinx. A new deconstructive logic: classical
logic. JSL, 62:755–807, 1997.
[26] J.Y. Girard. Linear logic. TCS, 50:1–102, 1987.
[27] J.Y. Girard. Multiplicatives. Rend. Sem. Mat. Univ. Politec. Torino, pages
11–33, 1987. Conf. on Logic and CS: New Trends and Appl.
[28] J.Y. Girard. A new constructive logic : Classical logic. MSCS, 1:255–296,
1991.
[29] J.Y. Girard. Proof-nets: the parallel syntax for proof-theory. In Logic and
algebra, Lect. Notes in Pure and Appl. Math. 180:97-124, 1996.
[30] J.Y. Girard. Light linear logic. IC, 143:175–204, 1998.
[31] J.Y. Girard. Locus solum: from the rules of logics to the logics of rules.
MSCS, 11:301–506, 2001.
[32] G. Gonthier, M. Abadi, and J.J. L`evy. The geometry of optimal lambda
reduction. In 9th SIGPLAN-SIGACT, pages 15–26, 1992.
[33] S. Guerrini, S. Martini, and A. Masini. Proof nets, garbage, and computations.
TCS, 253:185–237, 2001.
[34] M. Hofmann. A mixed modal/linear lambda calculus with applications to
bellantoni-cook safe recursion. In 11th CSL, pages 275–294, 1997.
[35] M. Hofmann. Safe recursion with higher types and BCK-algebra. Ann.
Pure Appl. Logic, 104:113–166, 2000.
[36] M. Hofmann. A type system for bounded space and functional inplaceupdate–
extended abstract. LNCS, 1782, 2000.
[37] F. Honsell and S. Ronchi Della Rocca. An approximation theorem for
topological lambda models and the topological incompleteness of lambda
calculus. J. Comp. and System Sciences, 45:49–75, 1992.
[38] D. Huges and R. Van Glabbeek. Proof nets for unit-free multiplicativeadditive
linear logic. In LICS. IEEE, 2003.
[39] M. Hyland and L.C.H. Ong. On full abstraction for pcf. IC, 163:285–408,
2000.
[40] M. Hyland and A. Schalk. Games on graph and sequentially realizable
functionals. In LICS’02, pages 257–264. IEEE, 2002.
[41] M. Kanovich, M. Okada, and A. Scedrov. Phase semantics for light linear
logic. TCS, 294:525–549, 2003.
[42] Z. Khasidashvili and A. Piperno. A syntactical analysis of normalization.
JLC, 10:381–410, 2000. Type theory and term rewriting.
[43] N. Kobayashi. Quasi-linear types. In 26th SIGPLAN-SIGACT, pages 29–
42, 1999.
[44] Y. Lafont. Soft linear logic and polynomial time. To appear inTCS, 2001.
[45] J. Lamping. An algorithm for optimal lambda calculus reduction. In
Popl’90, pages 16–30, 1990.
[46] O. Laurent. Polarized proof-nets: proof-nets for LC. In TLCA.
LNCS1581:213-227, 1999.
[47] D. Leivant. Stratified functional programs and computational complexity.
In 20th ACM Symp. on Prin. of Prog. Lang., pages 325–333, 1993.
[48] D. Leivant. Ramified recurrence and computational complexity III: Higher
type recurrence and elementary complexity. Ann. Pure Appl. Logic, 96:209–
229, 1999.
[49] J. Longley. The sequentially realizable functionals. Ann. Pure Appl. Logic,
117:1–93, 2002.
[50] R. Maieli and Q. Puite. Modularity of proof-nets: generating the type of a
module. Arch. Math. Logic, 2004. To appear.
[51] P. Neergaard and H. Mairson. LAL is square: Representation and expressiveness
in light affine logic. In 4th ICC, 2002.
[52] L. Paolini and S. Ronchi Della Rocca. Lazy logical semantics. In Cometa’03.
ENTCS, 2003.
[53] L. Paolini and S. Ronchi Della Rocca. Parametric parameter passing
lambda-calculus. IC, 189:87–106, 2004.
[54] M. Parigot. µ-calculus: an algorithmic interpretation of classical natural
deduction. In Logic programming and automated reasoning. LNCS, 624:190-
201, 1992.
[55] M. Pedicini and F. Quaglia. A parallel implementation for optimal lambdacalculus
reduction. In Ppdp 2000, pages 3–14, 2000.
[56] M. Pedicini and F. Quaglia. Scheduling vs communication in pelcr. In
Euro-par 2002, pages 648–655, 2002.
[57] A. Piperno. Normalization and extensionality. In LICS, pages 300–310.
IEEE, 1995.
[58] G. Plotkin. LCF considered as a programming language. TCS, 5:225–255,
1977.
[59] E. Robinson. Proof nets for classical logic. JLC, 13:777–797, 2003.
[60] S. Ronchi Della Rocca. Typed intersection lambda calculus. ENTCS, 70,
2002.
[61] S. Ronchi Della Rocca and L. Roversi. Lambda calculus and intuitionistic
linear logic. Studia Logica, 59:417–448, 1997.
[62] Simona Ronchi Della Rocca and Luca Roversi. Intersection Logic. In CSL.
LNCS, 2412:414-428, 2001.
[63] A. Salibra. Topological incompleteness and order incompleteness of the
lambda calculus. ACM Trans. on Comp. Logic, 4:379–401, 2003. 16th
LICS.
[64] K. Terui. Light affine calculus and polytime strong normalization. In 16th
LICS, pages 209–220. IEEE, 2001.
[65] D. Turner and P. Wadler. Operational interpretations of linear logic. TCS,
227:231–248, 1999.
[66] C. Urban and G.M. Bierman. Strong normalization of cut-elimination in
classical logic. Fund. Inform., 20:1–32, 2000.
[67] D. N. Yetter. Quantales and (noncommutative) linear logic. JSL, 55:41–64,
1990.


2.3 Numero di fasi del Programma di Ricerca:    2

2.4 Descrizione del Programma di Ricerca

Fase 1
Durata e costo previsto
Durata   Mesi  15  Costo previsto   Euro  100.000 


Descrizione

Testo italiano
Il progetto, come gia’ specificato nella parte “Obiettivo”, e’ organizzato in
vari livelli, che vanno da un livello speculativo di base a un livello di studio
e definizione di metodologie, ad un livello di riscontro e verifica su problematiche
reali. La comunicazione tra questi livelli sara’ sia in senso “bottom up”
che in senso “top down”. Infatti riteniamo che la soluzione di problemi aperti
a livello di base potra’ suggerire applicazioni a casi reali a livello di riscontro,
mentre problemi reali nell’ambito dell’applicazione che vogliamo tenere in considerazione
programmazione in ristrettezza di risorse ) possono ispirare nuove
ricerche di tipo metodologico. Di conseguenza e’ estremamente difficile articolare
il progetto in una rigida struttura sequenziale. A grandi linee pero’ possiamo
definire una prima fase di studio di 18 mesi, seguita da una fase di verifica dei
risultati e di implementazione prototipale di 9 mesi. La fase di studio sara’
dedicata a raffinare i risultati gia’ ottenuti al livello speculativo di base e al
livello metodologico, e allo studio di problemi aperti sempre a questi due livelli,
La suddivisione in livelli e temi di ricerca gia’ descritta si potra’ articolare,
all’interno di uno specifico tema, in una ulteriore suddivisione in task specifici.
Ci sembra qui importante evidenziare due fatti. Innanzitutto tutte le sedi coinvolte
nel progetto sono impegnate nei livelli 1 e 3, e tre di esse nel livello 2, a
dimostrazione di una effettiva collaborazione. Inoltre, sia i livelli che i temi di
ricerca in cui essi sono suddivisi non sono indipendenti. In particolare i temi 1.1
(Teoria strutturale della dimostrazione) e 1.3 (La logica come modello di computazione),
cosi’ come 2.1 (Metodologie Proof-as-Programs) e 2.2 (Metodologie
per Linguaggi con Complessita’ limitata) presentano problematiche comuni. In
effetti i problemi possono essere studiati da piu’ punti di vista, e proprio da
questa ottica multipla ci aspettiamo risultati interessanti. Ogni tema sara’ seguito
da un coordinatore, che avra’ il compito di monitorare il lavoro svolto,
e stimolare incontri, discussioni e cooperazioni sui vari problemi. Lo schema
generale del progetto di ricerca e’ il seguente:
1. Livello speculativo di base
1.1 Teoria strutturale della dimostrazione
– Logica Classica e Ludica
– Moduli
– Logica non commutativa
– Fondazione logica dei tipi intersezione
1.2 Modelli intensionali ed estensionali di linguaggi paradigmatici di programmazione.
– Modelli “fully abstract” per linguaggi funzionali
– Studio di lambda teorie
– Separabilita’
– L’eta-espansione come strumento per il controllo delle risorse.
– Approccio algebrico al lambda calcolo
1.3 La Logica come modello di computazione
– Studio delle Logiche Leggere
– Nuovi modelli per computazioni con complessita’ limitata
– Computazioni di numeri reali
2. Livello metodologico
2.1 Metodologie “Proofs-as-Programs”
2.2 Metodologie per linguaggi con complessita’ limitata
3. Livello di riscontro


Testo inglese
The project, defined in ”Obiettivo”, is organized in three levels, a foundational
one, a methodological one, and an applications one. The investigation
will fluidly move up and downward between levels, under the view that solving
foundational problems can suggest applications to real cases, and open problems
in a particular application field like, for example, programming with resources
limitations, can suggest new methodological studies. This is why our project
cannot a strictly sequentialized. We individuate a first phase, lasting about
15 months, dedicated to foundational and methodological studies and a second
phase, lasting about 9 months, dedicated both to verify the obtained results and
to try to use them a a base of prototypical implementations. In the first phase
we will work at the foundational and methodological level, to refine obtained
results and to study new open problems. The level constituting the project,
already defined, require a further splitting in specific research topics, for shake
of clarity.
We want to stress two important points. First of all, all the research unities
are involved at the levels 1 and 3, and three of the them at the level 2, so realizing
a true collaboration. Moreover, the levels are not at all independent. In
particular, both at levels 1.1 (Structural proof theory) and 1.3 (Logic as a computational
model), and at levels 2.2 (Proofs-as-Programs methodologies) and
2.3 (Methodologies for languages with predefined complexity) there are common
problems. Indeed, problems can be studied from different point of view,
and we expect to obtain interesting results exactly by crossing views. Every
level will have a coordinator, responsible of organizing meetings, and stimulating
both discussions and cooperation. Here it is the general structure of the
project:
1. Level: foundations
1.1 Structural proof theory
– Classical logic and Ludics
10
– Modules
– Non commutative logic
– Logical foundation of intersection types
1.2 Intensional and extensional models of paradigmatic programming
languages.
– “Fully abstract” models for functional languages
– lambda theories
– Separability
– Eta-expansion as toll for resources control
– Algebraic approach to lambda calculus
1.3 Logic as computational model
– Light logics
– New models for computation with limited complexity
– Computing real numbers
2. Level: methodology
2.1 Methodologies“Proofs-as-Programs”
2.2 Methodologies for languages with predefined complexity.
3. Level: Applications


Risultati parziali attesi

Testo italiano
1. Livello speculativo di base.
1.1 Teoria strutturale della dimostrazione (unita’ interessate: 1,3,4)
– Logica Classica e Ludica
Vogliamo sviluppare la teoria della dimostrazione per la logica
classica e la Ludica. Ci concentreremo sulla cosiddetta regola
MIX e sulla sua interazione con l’indebolimento. Questa linea
risale alla preistoria della Logica Lineare, a un lavoro di Ketonen
e Weyhrauch sulle procedure di decisione per frammenti sottostrutturali
del calcolo dei predicati. Un raffinamento di tale lavoro
ha condotto all’identificazione di una nozione di correttezza
per le reti di prova per la Logica Affine, una caratterizzazione
della dinamica delle prove nella Logica Affine con Mix ed un
algoritmo di separazione che restituisce una famiglia di reti di
prova in Logica Affine data una rete di prova in Logica Affine
con Mix. Lo ”status” del MIX e dell’Indebolimento rimane un
problema aperto per la semantica categoriale della Logica Classica
che intendiamo affrontare in questo progetto. Vogliamo inoltre
studiare la Logica Classica con un approccio proprio della
teoria dei tipi. Lo scopo e’ quello di ottenere un ambiente unificante
per studiare le proprieta’ computazionali del paradigma
funzionale ponendo l’enfasi sul cosiddetto ”Continuation Passing
Style”. Speriamo di ottenere un trattamento puramente logico
delle chiamate per valore e per nome. Riteniamo sia possibile
estendere la nozione di interazione (nel contesto della Ludica)
alla nozione di interazione concorrente o asincrona. Le strutture
astratte corrispondenti alle dimostrazioni (o ai programmi)
dovrebbero essere grafi (reti di prova astratte) e le interazioni
ordini parziali. In questo ci ispireremo alle intuizioni e alle tecniche
provenienti dalla teoria delle reti di prova, delle strutture
di eventi di Winskel, della multi-focalizzazione di Andreoli e dei
bi-grafi di Milner. Inoltre, visto che nella Ludica la sintassi e’
costruita su una relazione di equivalenza di dimostrazioni (ovvero
programmi, processi), ci si chiede se non possa offrire un ambiente
generale per lo studio dell’interazione e dell’equivalenza a
livello fondazionale.
– Moduli
Un modulo e’ una struttura (un pezzo di rete) con un bordo fatto
da ipotesi e da alcune conclusioni della rete stessa. Le principali
soluzioni al problema della codifica del comportamento di un
modulo come funzione del solo bordo sono quelle di Girard e di
Danos-Regnier basate su permutazioni e partizioni delle formule
del bordo. In [50], Maieli e Puite hanno fornito un algoritmo
per il calcolo del tipo di un modulo. Tale algoritmo itera alcuni
passi elementari di riscrittura corrispondenti alla associativita’,
commutativita’ e distributivita’ debole (o lineare) dei connettivi
di MLL. Un problema aperto e’ come estendere questo metodo
ai moduli di NL.
Si vuole studiare l’uso dei moduli nell’interpretazione delle reti
di MLL come circuiti booleani. Infatti, i circuiti booleani possono
essere costruiti su diverse basi, cioe’, partendo da differenti
circuiti di base; analogamente, si vuole analizzare la costruzione
delle reti di MLL che corrispondono alle reti di prova booleane
a partire da diversi moduli base. La questione della modularita’
rimane ancora aperta se si considera l’intera logica lineare. Qui
la difficolta’ era dovuta in passato all’assenza di criteri semplici
e soddisfacenti per i proof-net di MALL. I lavori sulla logica
polarizzata e la nuova definizione di un criterio di correttezza
per le reti di MALL [38] rende possibile un nuovo approccio
al problema generale della modularita’. La nostra prospettiva
e’ ”lo studio del processo della costruzione di una rete mediante
un sistema di calcolo basato su moduli di LL”. Al fine di
ridurre l’inevitabile non-determinismo implicito in questo processo,
miriamo a sfruttare una proprita’ di normalizzazione delle
dimostrazioni lineari, conosciuta come ”focalizzazione” [5, 6].
– Logica non commutativa
Il frammento piu’ interessante della logica non commutativa NL
e’ quello moltiplicativo MNL, cioe’ il frammento di NL nel quale
sono presenti solo i connettivi moltiplicativi, in entrambe le loro
versioni (commutativa e non commutativa). Nelle dimostrazioni
di MNL, la regola strutturale di scambio puo’ essere controllata
tramite una particolare classe di ordini ciclici: le varieta’
d’ordine. Ad ogni sequente di una dimostrazione di MNL viene
associata una particolare varieta’ che si modifica attraverso le
regole di introduzione dei connettivi e che rimane inalterata o
si restringe passando attraverso le regole strutturali.Il risultato
che si intende perseguire e’ quello di legare la nozione puramente
estensionale di varieta’ d’ordine, alla nozione piu’ geometrica di
”genere di un grafo”. Stabilire tale legame funzionale sarebbe un
risultato interessante almeno su due fronti: il fronte della ricerca
delle prove e quello della linguistica computazionale.
Ci aspettiamo risultati specifici in tre campi. Ci aspettiamo di
trovare una procedura per associare ad una qualsiasi varieta’ un
certo grado k che ne indichi la parzialita’. Una volta stabilita
questa misura, come secondo punto, sara’ possibile introdurre la
nozione di logica k-ciclica nel seguente modo: una dimostrazione
di MNL e’ anche una dimostrazione nella logica k-ciclica se e solo
se le varieta’ associate ai sequenti della dimostrazione hanno un
grado di parzialita’ al massimo pari a k. E finalmente si potra’
generalizzare questo risultato, mostrando che ogni dimostrazione
in una generica logica k-ciclica puo’ essere tradotta in un proofnet
di genere, al massimo, pari a f(k), per una certa funzione f
da rintracciare.
– Fondazione logica dei tipi intersezione
Si vuole raffinare il risultato ottenuto in [62], definendo una logica
che modelli tutte le prove del frammento implicativo e congiuntivo
di LJ(Logica Intuizionista), in modo da isolare il sottoinsieme
delle prove che corrispondono, in modo strutturale,
a derivazioni di tipo intersezione. Ci si aspetta di trovare una
scomposizione della congiunzione intuizionista in due connettivi,
che internalizzano propriet`a delle dimostrazioni a livello metateoretico.
Una logica di tal genere sarebbe interessante non solo
da un punto di vista squisitamente “proof-teoretico”, ma anche
nell’ambito dello studio di proprieta’ denotazionali di linguaggi
di programmazione. Infatti tale logica potrebbe fornire una connessione
tra l’approccio topologico, basato sui tipi intersezione,
ed un approccio basato sulla teoria della dimostrazione.
1.2 Modelli intensionali ed estensionali di linguaggi paradigmatici di programmazione
(unita’ interessate 1,2,3,4)
– Modelli “fully abstract” per linguaggi funzionali
Ricordiamo che un modello e’ detto “fully-abstract” quando l’equivalenza
da esso indotta sul linguaggio coincide con l’equivalenza operazionale,
o osservazionale. Intendiamo studiare tecniche di ”raf-
finamento” di filtri-modelli (basati su sistemi di assegnazione di
tipo intersezione), intese a costruire modelli che restringano la
classe delle funzioni rappresentabili nel modello. La motivazione
e’ che problemi di mancata fully-abstraction sono spesso legati
alla sovrabbondanza delle funzioni rappresentabili nel modello
rispetto alle funzioni rappresentabili mediante programmi. Un
primo risultato in questa linea e’ quello ottenuto in [52], che
sfrutta la nozione di lambda calcolo parametrico. Si vuole estendere
questo risultato, e quindi definire una metodogia generale
basata sui tipi intersezione per costruire modelli “fully-abstract”
per diversi lambda-calcoli. Un altro approccio e’ partire dalla
macchina operazionale parametrica [53], che suggerisce un particolare
tipo di modello sintattico (anch’esso parametrico). Questo
modello si basa sulla nozione di ortogonalita’ simile a quelle che
si possono trovare in numerose teorie legate alla logica lineare,
come la semantica delle fasi o la ludica. L’ortogonalita’, contrapponendo
insiemi di termini e contesti, origina una struttura
matematica “fully abstract” rispetto alla semantica operazionale
soggiacente, di cui si vogliono studiare da un lato le caratteristiche
estensionali e dall’altro quelle intensionali di specifiche
istanze operazionali. Intendiamo poi studiare la possibilita’ di
costruire modelli “fully abstract” anche utilizzando una nuova
semantica dei giochi per il lambda calcolo a partire dalla nozione
di gioco introdotta da Hirsch e Hodkinson per le algebre relazion-
ali.
Nella stessa linea di indagine, ci si propone di estendere e completare
il risultato fondamentale ottenuto da Plotkin nell’ambito
dei domini alla Scott e delle funzioni continue [58]. Cioe’ si vuole,
a partire da un modello denotazionale di PCF, non fully abstract,
trovare la minima estensione del linguaggio per cui il modello
goda di tale proprieta’. In primo luogo quindi si vuole studiare
quale estensione di PCF `e necessaria per descrivere tutte
e sole le funzioni stabili sugli spazi coerenti. Successivamente si
vuole affrontare il problema nell’ambito degli spazi iper-coerenti
e delle funzioni iperstabili di Bucciarelli ed Herhard [17].
– Studio di lambda teorie
Intendiamo studiare problemi di consistenza nel lambda calcolo
(vedi ad esempio [16]) affrontati con metodologie semantiche. Infatti
esistono molti problemi aperti, collegati con questa linea
di ricerca, di grande interesse. Due esempi importanti sono:
scelta della classe di termini piu’ opportuna da associare alla
nozione di ”indefinito” nel lambda calcolo, definizione della classe
di lambda termini che puo’ essere consistentemente uguagliata
con l’operatore che rappresenta la ricorsione, ossia l’operatore di
MINIMO punto fisso. Un ulteriore problema aperto e’ la caratterizzazione
categoriale, al momento assente, dei modelli costruiti
in [4] e lavori simili. Tali modelli sono al momento l’unico strumento
semantico che abbia consentito prove di easiness per classi
sufficientemente generali di lambda termini. Un inquadramento
categoriale della costruzione dovrebbe consentire una flessibile e
proficua generalizzazione della classica costruzione di Scott.
– Separabilita’
Nello studio delle equivalenze tra programmi, termini o dimostrazioni,
e in particolare per le dimostrazioni di full-abstraction, le proprieta’
di “separabilita”’ tra termini sono un importante strumento.
Nel lambda-calcolo queste proprieta’ sono state ampiamente studiate.
La mancanza di risultati in un contesto logico piu’ generale
e’ dovuto all’assenza di un ”modo canonico” per rappresentare le
dimostrazioni (come nel calcolo dei sequenti di Gentzen). Le cose
sono cambiate radicalmente con l’introduzione delle reti di prova,
e piu’ recentemente con lo studio delle reti di prova polarizzate
della LL polarizzata (LLpol). Vogliamo studiare la separabilita’
in un contesto polarizzato, basandoci su alcuni risultati parziali
che fanno congetturare la separabilita’ interna di LLpol.
– L’eta-espansione come strumento per il controllo delle risorse.
L’eta-regola del lambda calcolo puo’ essere considerata come un
mezzo per controllare la allocazione (essenzialmente statica) di
risorse computazionali. Una tale computazione ha portato alla
definizione di un calcolo sensibile alle risorse [57]. Un’opportuna
nozione di forma eta-espansa puo’ essere usata, come in [42],
per fornire un’analisi precisa della beta-riduzione come interazione
tra funzione e argomento, in un modo che ha interessanti
analogie con la semantica dei giochi. Ci proponiamo di
estendere i risultati sopra menzionati al caso dinamico, permettendo
cioe’ l’allocazione di risorse durante la computazione, e
applicare le tecniche proposte alla separabilita’ in un contesto
sensibile all’utilizzo di risorse.
– Approccio algebrico al lambda calcolo
Un problema interessante (legato al problema della incompletezza
d’ordine del lambda calcolo e all’esistenza di una algebra combinatoria
assolutamente non ordinabile) e’ se il reticolo delle
lambda teorie soddisfa identita’ di reticolo non banali. Intendiamo
inoltre estendere la nozione di linearita’ per le algebre
combinatorie introdotte da Abramsky alla varieta’ di algebre per
la lambda astrazione che e’ la diretta controparte algebrica del
lambda calcolo.
1.3 La logica come modello di computazione (unita’ interessate 1,2,3,4)
– Modelli di computazione con complessita’ predeterminata
Intendiamo procedere secondo diverse direttrici.
In una prima direzione, vogliamo analizzare l’ espressivita’ delle
logiche leggere in funzione della rappresentazione dei dati in ingresso.
Infatti, in dipendenza dai vincoli imposti sui tipi dei
termini delle codifiche, cambiano (e di molto) i risultati di rappresentabilita’
(p.e. se il secondo ordine non e’ opportunamente
ristretto, il calcolo non e’ piu’ corretto per polytime: [51] , [22] ).
C’e’ bisogno di risultati generali che scalino tra le diverse logiche,
in funzione della classe di complessita’ considerata. Vogliamo
porre l’enfasi sulla ricerca dell’uniformita’: la questione da risolvere
e’ se sia possibile definire parametricamente un calcolo
logico in modo tale che differenti classi di complessita’ si possano
definire con un’opportuna scelta dei parametri. L’idea e’ quella
di trovare un’adeguata nozione generale di ”esponenziale” cosicche’
differenti calcoli per classi di complessita’ possano essere
ottenuti senza cambiare le regole che governano gli esponenziali,
ma solo le regole strutturali.
Vogliamo indagare sulle strategie di riduzione indotte dai tipi
delle logiche leggere. I tipi EAL e LAL forzano sui lambda termini
delle strategie di riduzione ben determinate. E’ ben noto,
tuttavia, che tali strategie normalizzano “meno” del lambdacalcolo
(per esempio: esistono lambda-termini con tipo in LAL
che normalizzano in tempo polinomiale come termini LAL, ma
che normalizzano in tempo polinomiale come lambda-termini
puri). Terui e Baillot hanno recentemente proposto un sistema
(DLAL) che seleziona solo lambda-termini puri per i quali ogni
strategia e’ polinomiale. Ma e’ interessante anche andare nella
direzione opposta, ovvero cercare sistemi di tipi che tipizzano
famiglie piu’ ampie di termini e che danno indicazione sulla
strategia di riduzione per rimanere confinati entro una data classe
di complessita’.
In una seconda direzione, vogliamo determinare esattamente cosa
significhi caratterizzare classi di complessita’ per mezzo della teoria
strutturale della dimostrazione. Noi investigheremo almeno
le seguenti restrizioni di LL. Partendo dal frammento proposizionale
delle logiche leggere, cercheremo le estensioni “minimali”
necessarie per rappresentare, ad esempio, tutte le funzioni
polinomiali.
Studieremo il frammento lineare del secondo ordine, senza additivi.
Oltre a una bassa complessita’ computazionale, questa
restrizione sembra indurre un’algebra di polinomi direttamente
sulle formule logiche. Infine un’ulteriore restrizione che vogliamo
considerare e’ quella della funzione di contrazione A-o(A tensor
A) al caso in cui una delle due formule A contratte sia ottenuta
per mezzo di una (debole) forma di “dereliction”. Il sistema
risultante sembra essere corretto e completo rispetto a PTime
e nello stesso tempo puo’ suggerire una decomposizione naturale
della modalita’ “!”. L’idea che anche il ! possa essere decomposto
appare gia’ nella Ludica [31]. La Ludica ha infatti precisato
la doppia funzione degli esponenziali: da un lato portano
un’informazione strutturale, cioe’ la possibilita’ di cancellazioni
e duplicazioni; dall’altro permettono il cambio di polarita’ della
sottoformula esponenziata. Questa osservazione porta in modo
naturale a decomporre gli esponenziali in due modalita’, una
per ciascuna delle precedenti funzioni. Noi vogliamo studiare il
significato (se esiste) di tale decomposizione nei sistemi leggeri.
Questa analisi sarebbe anche un ponte verso la semantica dei
giochi, dove tale decomposizione e’ presente.
In una terza direzione, vogliamo studiare la correlazione tra sistemi
sub-ricorsivi di LL che caratterizzano PTime ed altri sistemi,
disegnati, ad esempio, seguendo principi della teoria della
ricursione. Vogliamo fare questo seguendo due linee. In primo
luogo vogliamo rendere esplicita la struttura logica nascosta in
HOLRR [24], in cui il comportamento computazionale del ricursore
R e’ definito in modo da limitare il numero di duplicazione
possibili. R potrebbe essere scomposto in operatori piu’ primitivi,
e questo potrebbe mettere in correlazione la ramificazione
di HOLRR e la stratificazione di LAL. Vogliamo poi provare a
rilassare il piu’ possibile i principi che rendono LAL corretto e
completo rispetto a PTime per identificare la corretta strategia
di eliminazione del taglio. Sospettiamo che il sistema risultante
possa non essere piu’ fortemente normalizzabile.
Intendiamo inoltre sviluppare un nuovo calcolo logico per le classi
di complessita’. In un primo stadio vogliamo estendere l’approccio
iniziato da Girard con LLL al fine di introdurre operatori modali
adeguati al trattamento del non determinismo. L’obiettivo e’
quello di caratterizzare in modo puramente logico le classi di
complessita’ ”non deterministiche” (ad esempio NP).
– Complessita’ computazionale implicita di computazioni su numeri
reali.
Il modello BSS (Blum-Shub-Smale) e’ un’estensione delle macchine
di Turing che cattura le classi di complessita’ computazionali
generate fissando un insieme arbitrario di operazioni atomiche.
Questo approccio puo’ essere esteso ulteriormente in un
contesto piu’ ampio utilizzando la teoria algebrica della complessita’.
Da un punto di vista macroscopico, lo si puo’ estendere
considerando una macchina computazionale ideale che moltiplica
in un passo elementi di un anello arbitrario R e memorizza i
risultati in modo che l’accesso ad essi abbia costo unitario. Nel
modello BSS, operazioni lineari come l’addizione, la sottrazione
o la moltiplicazione scalare sono libere, mentre la moltiplicazione
non scalare e la divisione hanno costo uno. Questo approccio alla
complessita’ e’ importante soprattutto per valutare l’efficenza
degli algoritmi numerici, dove non e’ presa in considerazione la
reale complessita’ computazionale delle operazioni aritmetiche.
Studieremo l’uso di LLL e ELL per caratterizzare le classi di complessita’
BSS; questo approccio permette una definizione delle
classi di complessita’ per le computazioni sopra numeri reali
basato sulle classi di complessita’ implicita che hanno una caratterizzazione
logica. BSS-PTIME potrebbe presumibilmente essere
ottenuto da un risultato di rappresentazione per i programmi
BSS in un’estensione di LLL, che preservi il limite di complessita’
controllando le regole strutturali. Per ottenere questo tipo di
risultati, studieremo la codifica delle macchine BSS in un lambda
calcolo tipato da formule di LLL (piu’ precisamente di LAL [10])
e con un tipo atomico per i numeri reali.
2 Livello metodologico
2.1 Metodologie “Proofs.as-Programs” (unita’ interessate 1,4)
Risultati parziali gia’ ottenuti nell’indagine sulla fondazione logica
dei tipi intersezione rivelano aperture interessanti in questa
direzione. Una volta disegnata la logica che modelli tutte le
prove del frammento implicativo e congiuntivo di LJ(Logica Intuizionista),
in modo da isolare il sottoinsieme delle prove che
corrispondono, in modo strutturale, a derivazioni di tipo inter-
sezione, si vuole indagare sul linguaggio che si otterra’ tramite
la sua decorazione. Ci si aspetta un linguaggio di processi, che
formalizzi in modo rigoroso la nozione di sincronizzazione. Ulteriori
sviluppi potranno ottenersi raffinando le formule logiche,
come suggerito dalle logiche leggere, per il controllo delle risorse
di calcolo.
2.2 Metodologie per linguaggi con complessita’ limitata (unita’ interessate
1,2,4)
Affronteremo essenzialmente due problemi: (i) L’uso di tipi interserzione
per la caratterizzazione di classi di termini delle logiche
leggere con proprieta’ di normalizzazione specifiche. Infatti l’uso
dei tipi intersezione (e dei filtro-modelli) per la caratterizzazione
delle proprieta’ di normalizzazione dei lambda-termini puri e’
una delle applicazioni piu’ notevoli di questi sistemi di tipo e ha
dato risultati di eccezionale importanza (caratterizzazione dei
solvable, dei fortemente normalizzabili, ecc.). Sembra ragionevole
applicare le competenze (molto forti) dell’unita’ operativa (e
del progetto nel suo complesso) allo studio di quali proprieta’
di normalizzazione possano ottenersi aggiungendo tecniche di
tipo “intersezione” ai tipi delle logiche leggere. (ii) L’estensione
degli algoritmi di inferenza di tipo sviluppati in letteratura per
le logiche leggere [20, 21, 11] ai sistemi piu’ evoluti sviluppati
al punto 1.3, in particolare per sistemi di tipi con ricorsione esplicita,
per esempio nello stile di [24] La disponibilita’ di strumenti
automatici di inferenza e’importante in quanto permette di
liberare il programmatore dall’annotazione dei box, tipica delle
logiche leggere. Inoltre, si osserva che i riduttori ottimali di
lambda-termini secondo Levy-Lamping sfruttano implicitamente
le strategie di riduzione imposte dai tipi (nel caso di LAL e EAL).
Comprendere quale sia il sistema di tipo “piu’ flessibile” per cui
questo continua ad avvenire sembra essere un problema interessante
(e difficile).


Testo inglese
1. Level: foundations.
1.1 Structural proof theory (unities: 1,3,4)
– Classical logic and Ludics
We aim at studying and developing proof theory for classical
logic and Ludics. We will focus on the role of the so called MIX
rule and on its interactions with Weakening. The issue goes back
to the pre-history of linear logic, more precisely to Ketonen and
Weyhrauch’s work on decision procedures for sub-structural fragments
of the predicate calculus. A refinement of such a work has
led to identify correctness conditions for proof-nets for Affine
Logic, a proof-net characterization of the dynamics of Affine
Logic with Mix, and a separation algorithm which yield a family
of Affine proof-nets once a proof-net for Affine Logic with Mix
is given. The status of Mix and of Weakening remains an open
problem for categorical semantics of classical logic and we should
start to addressed it in the period of this project. We would also
investigate classical logic under a ”type theoretical” approach.
The aim is to obtain a unifying framework in order to study computational
properties of the functional paradigm with emphasis
on the so called Continuation Passing Style. We hope to be able
to give a pure logical treatment of ”call by value” and ”call by
name”. We think it is possible to extend the notion of interaction
(in the framework of Ludics) to an asynchronous or concurrent
notion of interaction. The abstract structures corresponding to
proofs/programs should be graphs (abstract proof nets) and the
interactions partial orders. We will be led from intuitions and
methods coming from the theory of proof-nets, Winskel’s event
structures, Andreoli multi-focalization, and Milner’s bi-graphs.
Moreover, as Ludics build the syntax on the equivalence relation
among proofs (programs/processes), rather then the opposite, we
wonder whether it can offer a general setting in which to study
interaction and equivalence at a foundational level.
– Modules
A module is a structure (a piece of a proof-net) with a specified
border consisting of all of the hypotheses and some of the conclusions
(of the proof-net). The most important solutions to the
problem of encoding the behavior of a module as a function on
the border only are those given by Girard and Danos-Regnier,
based, respectively, on permutations and partitions over the border
(formulas). In [50], Maieli and Puite have given an algorithm
for computing the type of a module. This algorithm simply iterates
some elementary graph rewriting steps corresponding to the
associativity, commutativity and weak (or linear) distributivity
of the connectives of MLL. An open problem is how to extend
this method to the modules of non-commutative logic NL.
On the complexity side, recently, has been shown by Terui a correspondence
betweenMLL proof nets with n-ary fan-in par/tensor
and boolean circuits. N-ary par/tensors were introduced by
Danos and Regnier in and can be seen as a particular case of
modules. We want to investigate the use of modules in the interpretation
of MLL proof-nets as boolean circuit. In fact, boolean
circuits can be built on different basis, that is, starting from
different basic boolean circuits; correspondingly, we would like
to analyze the construction of MLL proof nets corresponding to
boolean proof nets starting from different basic modules.
Although the question of modularity w.r.t. the MLL case can be
considered settled, it remains still open w.r.t. the full fragment
of linear logic. Here the difficulty was due, in the past, to the absence
of simple and satisfying correctness criteria for proof-nets
of MALL. The works on polarized logic and the new definition of
a correctness criterion for MALL proof nets [38] make possible a
new approach to the general problem of modularity.
Our perspective is the ”study of the process of proof-net construction
by means of a system calculus based on modules of
LL”. In oder to reduce the inevitable non-determinism implied
in this process, we aim at exploiting a normalization property of
linear proofs known as ”focusing” [5, 6].
– Non-commutative logic
The most interesting fragment of non-commutative logic NL is
the multiplicative one, MNL, i.e., the fragment of NL where are
only admitted the multiplicative connectives in their double version,
the commutative and the non commutative ones.
In MNL proofs, the exchange rule can be easily checked by a
special subset of cyclic orders: the order varieties. To every sequent
in a MNL proof, we can associate a particular order variety
that changes through the introduction rules, but that remains
the same or becomes smaller through the structural rules. The
result that we want to obtain for NL can be viewed as a link
between the purely extensional notion of order varieties and the
more geometrical notion of gender in graph theory. We believe
that this kind of functional link would be an interesting result in
the proof construction field and in the computational linguistic
field.
We expect to obtain specific results in three topics. We We want
to find a procedure that allows to associate to every order variety
a certain k that denotes its ”degree of partiality” (when an order
variety is total, i.e. a cycle, then k=0). So, it will be possible, at
the second step, to introduce the notion of k-cyclic logic in this
way: a certain MNL proof is also a proof in a k-cyclic logic if and
only if the varieties associated to the sequents occurring in the
proof have the degree of planarity at most equal to k (e.g., McyLL
will correspond to 0-cyclic logic). We also know that any McyLL
proof can be expressed by a planar proof-net; in other words we
know that the 0-cyclic logic corresponds to work with graphs of
gender 0. And finally we will generalize this result, showing that
every proof in any k-cyclic logic can be translated in a proof-net
of gender at most equal to f(k), for a certain function f (to be
defined).
– Logical foundation of intersection types
We want to deepen [61] by defining a logical system that embeds
the implicative and conjunctive fragment of Intuitionistic Logic
(LJ), in which we structurally characterize a sub-set of derivations
equivalent to Intersection Types (IT). The idea is to find
a decomposition of standard intuitionistic conjunction into two
connectives, each internalizing meta-theoretical properties of LJ
and IT. The interest would be both on the proof-theoretical side,
and on the study of denotational properties of paradigmatic programming
languages. Such a logic could connect both topological
and proof-theoretical approaches to the study and definition of
semantics of programming languages.
1.2 Intensional and extensional models of paradigmatic programming
languages.
– “Fully abstract” models for functional languages.
Let us recall that a model is “fully abstract” when the equivalence
it induces on the language coincides with the operational
(observational) equivalence. We want to study general techniques
for “refine” filter-models, with the aim to build models
with a very restricted class of representable functions. The motivation
is that the full-abstraction fails in general because there
are too many representable functions in the model with respect
to the functions which are definable by programs. We are still
missing an in-depth study of the pruning techniques for the representable
functions in the filter-models. A first result along
this line is that one obtained in [52], which uses the notion of
parametric lambda calculus. We want to extend this notion,
for defining a general methodology to build fully abstract models
for different lambda calculi. An other approach is to start
from the parametric operational semantics [53], for introducing
a syntactic model, based on a suitable notion of “orthogonal”
in analogy to the omonymous notion present in Phase semantics
and Ludics, conceived after, and as an evolution of, LL. In our
context, “orthogonal” formalizes the contra-position contexts vs.
terms of a given language, originating a fully abstract model for
the intended operational semantics. Extensional and intensional
properties of this latter will be studied.
Moreover, in the same research line, we believe we can extend
and complete [57], by Plotkin. On one side, we want to find
which extension of PCF allows to characterize Stable functions
on Coherence spaces. Then, we want to cope with the same
problem in the context of Iper-coherence spaces and Iper-stable
functions [17].
– Lambda theories.
As in [16], we want to study consistency problems for the lambdacalculus,
using semantic methodologies. One interesting example
is about the choice of the right set of lambda terms to represent
the notion of ”being undefined”. Another problem is the definition
of the set of lambda terms that can be consistently equated
to the recursion operator, which, recall, is interpreted as the
least fix point operator. A further open problem is the categorical
characterization of the models in [4], the unique semantic
tool that allowed to prove easiness for significantly general sets of
lambda-terms. A categorical characterization would constitute
a generalization of the classical model construction by Scott.
– Separability.
”Separability” is a basic tool to prove equivalences between programs,
terms and demonstrations of full-abstraction. The introduction
of proof-nets, and of their polarized version, relative to
Polarized LL(LLpol), opens the way to a general and uniform
approach to the study of lambda calculus theories. We shall
study ”separability” for lambda calculus starting from partial
results on separability internal to LLpar. We shall start from
three known results: i) Laurent’s injectivity of LLpar game semantics;
ii) Statman separability for simply typed lambda calculus,
as proved by Joly, starting from Krivine realizability; iii)
separability of a variant of lambda mu calculus, by Surin.
– Eta-expansion to control resources.
The eta-rule of lambda calculus can be used to model a static
allocation of computational resources. This pint of view led to
[56], a resource sensitive calculus. Also, the eta-rule can be used
to talk about properties of type assignments in a polymorphic
context, to prove normalization syntactically, and, once suitably
modified, it can be used to yield a game theoretic interpretation
of beta reduction [42]. We want to extend the results just recalled
in a context of dynamic allocation of resource, possibly using
separability results.
– Algebraic approach to lambda calculus.
An interesting question is to ask if the lattice of lambda theories
satisfies non trivial lambda identities, which is closely related
to a pair of problems: one concerns the lambda calculus order
incompleteness, and, the other is about the existence of an absolutely
non sortable combinatory algebra. We also want to extend
to the varieties of the lambda abstractions the notion of linearity
on combinatory algebras, given by Abramsky, the varieties of the
lambda abstractions being the algebraic counterpart of lambda
calculus.
1.3 Logic as computational model
– Computational models with predetermined complexity.
We shall investigate under different lines.
We want to analyze the expressivity of light logics as a function
of the chosen representation of input data — we already know
that the expressivity heavily depend on them. In particular we
are interested to find uniform criteria to determine expressivity,
that can scale uniformly to different logical systems and to different
complexity classes. The goal is a parametric logical system
that can ”uniformly” characterize different complexity classes by
means of different choices of the parameters. Parameters should
effect structural rules, while ”exponential” should remain unchanged.
We want investigate about the reduction strategies induced by
EAL and LAL on lambda terms, already knowing about the existence
of a sub-set of lambda terms, that can be given formulae
of LAL as types [64], and such that they normalize in polynomial
time under any strategy. We want to go, somewhat, in the
opposite direction by looking for type assignments of sufficiently
large classes of lambda terms, without escaping an initially given
reduction complexity.
We want also contribute to determine the meaning of characterizing
complexity classes by structural proof-theory. We shall
investigate about, at least, the following restrictions of LL. On
one side, starting from the propositional fragment of light logics,
we shall look for their minimal extensions that allow to represent,
for example, all the polynomial functions. On the other, we
shall explore II order linear fragment — no additives and multiplicatives
— which seems to induce an algebra of polynomials
directly on logical formulae, forcing a low computational complexity.
Also, we shall restrict the contraction map A-o(A tensor
A) of a suitable fragment of LL, so that one of the two A is
forcefully derived from a (weak form) of dereliction. The result
seems to be PTime correct and complete, simultaneously suggesting
a natural decomposition of the modality “!”. The idea
that ”!” can be decomposed also appears in Ludics [31], where
exponentials are associated both to the structural information,
like contraction and weakening, and to a change of polarity of
the involved formula. This decomposition exactly suggests a decomposition
of modalities, whose possible impact on light logics
still require investigation.
We want to relate sub-recursive sub-systems of LL characterizing
PTime with other systems, designed after recursion theoretic
principles, for example. Two leading ideas follow. One should
make it explicit the logical structures hidden in HOLRR [24],
in which the constraints, defining the computational behavior
of the recursor R, are in charge of limiting the duplication. R
should be split into more primitive operators, to make it evident,
the relation between ramification and stratification of light logics.
Another way to relate heterogeneous sub-recursive systems,
is to relax as much as possible the principles that make LAL
PTime sound and complete. This would require relaxing structural
constraints about sub-derivations that can be duplicated,
after a careful identification of the right cut-elimination strategy.
We shall try to characterize nondeterministic complexity classes
— like NP. The idea is to extend Girard’s approach that led to
LLL — non-determinism will follow from introducing suitable
modalities.
– Implicit computational complexity on real numbers.
Blum-Shub-Smale (BSS) model is an extension of Turing machines
to capture computational complexity classes, given an arbitrary
set of atomic operations. Their approach is relevant to
assess the efficiency of numerical algorithms, when actual computational
complexity of arithmetic operations is not taken into
account. Their point of view holds with costless linear operations
— addition, subtraction, and scalar multiplication — while
non-scalar multiplication and division have unary cost. We shall
investigate the definition of complexity classes that contain functions
on real numbers, in the hierarchy of BSS, by exploiting implicit
characterizations, as given by LLL and ELL. Presumably,
BSS-PTIME can be obtained by embedding BSS programs in an
extended version of LLL which preserves the complexity bound
by control on the structural rules. In order to obtain this kind of
results, we shall investigate the encoding of BSS machines in a
typed lambda calculus, whose types would be formulae of LLL,
extended with a basic type for real numbers.
2. Level: methodology
2.1 Methodologies“Proofs-as-Programs” (unities: 1,4).
Starting from known results about the logical foundation of Intersection
types, we want to design and study a language obtained by
”decorating” the sub-system of LJ whose derivations structurally
correspond to those of the Intersection types system. We expect a
process language that highlights aspects and properties of the synchronization
among processes. Then, we shall try to embed techniques,
developed on light logics to deal with processes running with
limited resources.
2.2 Methodologies for languages with predefined complexity (unities: 1,2,4).
We shall cope with essentially two issues.
We plan to apply Intersection types to the study of which normalization
properties could be obtained through their combined use with
light types. This goal is in the lines of the fruitful traditional use
of Intersection types, and of filter-models, about which the project
participants have strong competence, to characterize normalization
properties of pure lambda-terms, like solvable terms, strongly normalizable
terms, etc.
We plan to extend the type inference algorithms developed for light
logics [20, 21, 11] to more flexible systems, subject of our studies,
paying particular attention to systems with explicit recursion. Automatic
inference dispense programmers from the box annotation,
typical of light logics. Moreover, optimal reducers of lambda-terms
a’ la Le’vy-Lamping implicitly exploit the reduction strategies enforced
by the types of, at least LAL and EAL. We shall also look for
the type system such that this continues to hold.



Unità di Ricerca impegnate

Unità n. 1 
Unità n. 2 
Unità n. 3 
Unità n. 4 


Fase 2
Durata e costo previsto
Durata   Mesi  9  Costo previsto   Euro  66.300 


Descrizione

Testo italiano
Questa seconda fase del progetto sara’ soprattutto orientata alla verifica dei
risultati ottenuti nella fase 1, e alla verifica della loro applicabilita’ a problemi
reali, nell’ambito in particolare di computazioni mobili con risorse limitate.
Del resto questi problemi hanno orientato, a livello di riscontro, tutto il
nostro programma di ricerca. Intendiamo quindi dedicare questa ultima parte
del programma al disegno e allo sviluppo di linguaggi. Intendiamo in particolare
sia implementare a livello prototipale linguaggi paradigmatici, studiati ai
livelli 1 e 2, sia progettare e sviluppare loro estensioni che da una parte abbiano
le caratteristiche di usabilita’ dei linguaggi reali e dall’altra ereditino il rigore
semantico del linguaggio paradigmatico sotteso. E’ pero’ importante sottolineare
che l’effettivo lavoro di implementazione prototipale sara’ possibile solo se
il finanziamento ottenuto sara’ sufficiente a permetterci di acquisire le risorse
umane (borse e contratti) che abbiamo pensato di utilizzare soprattutto a tal
fine.


Testo inglese
In this second phase we shall orient our activities to the application of results,
obtained in phase 1, to real problems, with a particular focus on the context of
mobile computations that take place in contexts with limited resources. In particular,
we plan to implement paradigmatic programming languages, of levels 1
and 2, once extended and adapted to better fit usability requirements, typical
of everyday programming languages, while preserving the properties of those we
shall start from. We remark that the development of prototypical implementations
will, in any case, be subject to the funds we shall obtain to hire human
resources to that purpose.


Risultati parziali attesi

Testo italiano
Questa parte del progetto e’ articolata in quattro punti distinti:
i) Nel contesto della tecnologia di sviluppo dei compilatori orientata ad una
implementazione efficiente del lambda calcolo ci aspettiamo di estendere
PERCL con costrutti per la chiamata di procedure esterne. Ricordiamo
che PERCL interpreta lambda termini (estesi con costanti alla PCF) in un
ambiente multiprocessore. L’implementazione di PELCR [56] si avvale di
varie tecniche classiche dei calcoli paralleli e distribuiti, in particolare, si e’
usata una tecnica di aggregazione dei messaggi che permette una riduzione
dell’overhead di comunicazione, una politica fair della distribuzione del
carico generato dinamicamente, una tecnica ”piggyback” per minimizzare
l’informazione sul carico dei processori. L’estensione descritta comporta
alcuni problemi che devono essere considerati perche’ possa essere compatibile
con la strategia di valutazione parallela (e’ infatti molto probabile
che abbia effetti sulla granularita’ dell’applicazione).
ii) Nel contesto della realizzazione di buoni interpreti per linguaggi funzionali
vogliamo progettare e realizzare un meta-linguaggio che permetta di
specificare vari lambda-riduttori (ottimale alla Levy-Lamping, Mackie,
vanOostrom, ecc.) e di generare tali riduttori in modo automatico dalle
specifiche. Esistono infatti pochissime implementazioni di riduttori di
lambda-termini secondo le strategie indotte dalle logiche leggere. Uno
strumento parametrico di generazione permetterebbe un confronto sperimentale
circa la loro reale efficienza su benchmark significativi.
iii) Nel contesto della realizzazione di buoni interpreti per linguaggi funzionali,
vogliamo progettare e studiare sistemi di controllo della memoria basati
sulle logiche leggere. C’e’ estesa letteratura sull’applicazione della logica
lineare al problema della deallocazione esplicita di memoria. L’applicabilita’
di tali tecniche al contesto delle logiche leggere non e’ mai stata studiata,
mentre sembra estremamente promettente.
iv) Nel contesto della progettazione di nuovi linguaggi di programmazione,
Vogliamo progettare un sistema di tipi per un linguaggio concreto (con
strutture dati primitive e ricorsione) che permetta di controllare l’uso della
risorsa ”tempo” utilizzando i principi propri delle logiche elementari e
leggere. L’obiettivo e’ quello di essere in grado di ottenere informazioni
“tight” sul tempo di calcolo a partire dall’inferenza di tipo. La motivazione
per tale progetto e’ ovvia, quando si realizzi che stiamo parlando di un
linguaggio concreto e non di una variante di lambda-calcolo. L’utilizzo dei
risultati ottenuti al punto 2.2 “ Metodologie per linguaggi con complessita’
limitata” appare importante.


Testo inglese
In the context of the compiler technology oriented to efficient implementation
of lambda calculus, we expect to extend PELCR to allow external procedures
calls. Recall that PELCR interprets lambda terms, extended with constants a’ la
PCF, in a multiprocessor environment. Communication overhead is reduced by
aggregating messages. The load on processors is dynamically balanced by means
of a fair policy, while the ”Piggyback” technique allow to decrease the amount
of processors loads information. The extension we aim for raises compatibility
issues, still unresolved, related to the parallel evaluation strategy.
In the context of good interpreters for functional languages, we expect to
find a meta-language that embeds, parametrically, known efficient lambda reducers,
like, for example, those by Le’vy-Lamping, Mackie, van Oostrom, etc..
The idea is that the meta-language should allow to automatically generate such
interpreters, starting from their formal specification. Light logics should help
designing the meta-language and to comparatively assessing the various interpreters,
by means of uniform benchmarks.
Again in the context of interpreters for functional languages, we expect to
adapt to the languages designed after light logics the known good memory management
techniques that take advantage of information about resource usage,
statically given by formulae of LL, once used as types.
Finally, in the context of the programming languages design, we expect to
develop a type checking for a concrete programming language, endowed with,
for example, primitive basic data types and recursion, which allow to program
functions whose resource consumption is certified by their types. The starting
point will be our studies at level 1.3 about Light logics. Concreteness of the
language is the main issue, whose solution should be supported by results of
point 2.2 ”Methodologies for languages with predefined complexity”.



Unità di Ricerca impegnate

Unità n. 1 
Unità n. 2 
Unità n. 3 
Unità n. 4 




2.5 Criteri suggeriti per la valutazione globale e delle singole fasi


Testo italiano

Proponiamo, per valutare i risultati teorici del progetto, i seguenti criteri:
- Le pubblicazioni prodotte nell’ambito del progetto dovranno essere valutate
in funzione del prestigio (impact factor) e della pertinenza della rivista, o
degli atti del convegno, su cui appariranno.
- Ad ogni workshop del progetto saranno invitati revisori esterni, a cui
saranni chiesti rapporti sulla qualita’ dell’attivita’ scientifica svolta. Tali rapporti
saranno allegati al rapporto finale.
- Gli atti del convegno finale verranno pubblicati. La forma di pubblicazione
e il successo del volume saranno un indice del prestigio del progetto.
Per quanto riguarda le implementazioni di linguaggi prototipali realizzate,
tutti i codici sviluppati nell’ambito del progetto saranno resi disponibili in rete alla
comunita’ scientifica internazionale, che potra’ sperimentarli. A tutti gli utenti
verra’ richiesto di redigere un rapporto sulla loro esperienza.


Testo inglese
We propose, for the evaluation of the theoretical results of this project, the
following criteria:
- The publications developed during the project will be evaluated with respect
to the impact factor and pertinence of either the journal or the conference
proceedings, when they will appear.
- We will invite, at every workshop of the project, external referees, which
will be asked to write reports on the quality of our scientific research. Such
reports will be attached to the final one.
- The proceedings of the final meeting will be published. The modalities of
the publication and the success of the volume will be a measure of the result of
the project.
As far as the implementations that will be realized, all the software developed
inside the project will be put in the web, for be freely used by the scientific
community. To all users a report on their experience will be asked.