Logica e computazioni: sintassi, semantica e interazione (PRIN 2004)

Data inizio
30 novembre 2004
Durata (mesi) 
24
Dipartimenti
Informatica
Responsabili (o referenti locali)
Masini Andrea
URL
2004011194_002

L'attivita' dell'unita' di Verona seguira' tre linee di ricerca:
1) teoria della dimostrazione strutturale;
2) modelli estensionali e intensionali per linguaggi di programmazione paradigmatici. 3) sistemi deduttivi per classi di complessita' computazionale;
Le tre linee di ricerca appartengono al "livello 1: speculativo di base" del progetto nazionale (modello A).
In (1) studieremo e svilupperemo 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 sotto-strutturali del calcolo dei predicati.
Ketonen e Weyhrauch, usando la struttura dati delle "catene causali" (piu' tardi riscoperte con la condizione di aciclicita'), hanno considerato una rappresentazione statica della logica dei predicati senza contrazione; tale rappresentazione si puo' mettere in relazione con le reti di prova. 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.
Per quel che riguarda (2) intendiamo sviluppare una nuova semantica dei giochi per il lambda calcolo a partire dalla nozione di gioco introdotta da Hirsch e Hodkinson per le algebre relazionali (vedi R. Hirsch e I. Hodkinson - Relation algebras by games - Studies in Logic and the Foundations of the Mathematics, vol.147, North-Holland, 2002).
In questo modo speriamo di trovare una nuova semantica operazionale del lambda calcolo "fully abstract" secondo un'opportuna nozione di gioco. Un altra questione interessante (legata 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. Altre direzioni di ricerca riguardano l'estensione di metodi semantici basati sugli spazi coerenti e la caratterizzazione di modelli del lambda calcolo differenziale introdotto da Erhard.
In (3) intendiamo 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). Vogliamo inoltre 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 inoltre riconsiderare l'approccio di Buss (basato sull'aritmetica limitata) assumendo un punto di vista costruttivo (in accordo con il paradigma "prove come programmi" e "formule come tipi").

Enti finanziatori:

Ministero dell'Istruzione dell'Università e della Ricerca
Finanziamento: assegnato e gestito dal dipartimento
Programma: COFIN - Progetti di Ricerca di Interesse Nazionale

Partecipanti al progetto

Attività

Strutture