RICERCA ITALIANA     

Fondazioni Logiche di Linguaggi Astratti di Programmazione

Università degli Studi di Torino

Abstract

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. <<<

Coordinatore Scientifico del Programma di Ricerca

Simonetta RONCHI DELLA ROCCA Università degli Studi di TORINO

Obiettivo del Programma di Ricerca

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. <<<

Risultati parziali attesi

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).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. <<<

Durata

24 mesi

Base di partenza scientifica nazionale o internazionale

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. <<<