giovedì 20/10/1994, ore 17, aula G

Corrado Böhm

Parallelismo nella pura programmazione funzionale

Abstract
Descriviamo un sistema di programmazione funzionale in cui ogni funzione ed ogni dato espresso come elemento di un'algebra di termini possiede una interpretazione nel lambda-calcolo puro. Ci restringeremo a sistemi ricorsivi di equazioni che definiscono funzioni da un'unione di algebre di termini ad algebre di termini (quindi polimorfe ma non eterogenee), senza tuttavia escludere funzioni di ordine più elevato, aventi per esempio funzioni come argomenti. Verranno forniti esempi significativi di programmazione senza effetti collaterali. In virtù delle premesse, il sistema di riscrittura corrispondente alle equazioni ammette una computazione parallela di cui si mostrerà la correttezza.

giovedì 3/11/1994, ore 17, aula G

Piero Pagliani

La comunicazione in sistemi di informazioni parziali come fondamento semantico di alcune logiche non-classiche: dalla teoria alle applicazioni

Abstract
Le semantiche che si basano su metafore suggerite dall'idea di "informazione che varia" costituiscono alcuni degli strumenti di analisi più utilizzati in logica: esempi paradigmatici sono la semantica relazionale di Kripke per la Logica Intuizionista, basata sulla nozione di "incremento delle informazioni" e la semantica relazionale di Routley e Mayer per il sistema R di Logica della Rilevanza, basata sulla nozione di "combinazione di informazioni".
In questo seminario verrà illustrato un nuovo modello intuitivo basato invece sulla nozione di "richiesta e comunicazione di informazioni" in sistemi concreti di dati del tipo <Oggetto, Attributo, Valore>. Si proverà che la Logica di Kleene, la Logica di Nelson non costruttiva, la Logica a tre valori di Lukasiewicz e la Logica di Post di ordine tre, sono modellizzate in modo naturale dal nuovo paradigma interpretativo. Questo risultato permette di definire le operazioni algebriche per calcolare le dipendenze funzionali contingenti, necessarie, impossibili e possibili in sistemi dove la funzione di informazione è solo parzialmente definita.

giovedì 17/11/1994, ore 17, aula G

Ugo Berni Canani

Distribuzioni di parole

Abstract
1) Distribuzioni di frequenze.
2) Analisi fattoriale delle associaziuoni fra parole, applicazioni (rilevazione di polisemie, rappresentazioni sintetiche di testi).
3) Indice di associazione tra parole: assunzioni implicite, distribuzione in testi reali e testi generati aleatoriamente.
4) Aspetti di ordine nelle configurazioni di parole. Rilevazione di sinonimie.
5) Modelli di relazioni lessicali.

giovedì 1/12/1994, ore 17, aula G

Adolfo Piperno

Normalizzazione ed estensionalità

Abstract
Il lambda-calcolo viene in genere equipaggiato con due regole di tipo diverso: la beta-regola, che costituisce il vero e proprio meccanismo di calcolo, e la eta-regola, che consente di ragionare su proprietà di termini.
Verrà descritto un approccio diverso alla riduzione nel lambda-calcolo, in cui la beta-regola continua a costituire il vero meccanismo di calcolo, ma è sempre terminante, mentre la eta-regola stabilisce le risorse.

giovedì 15/12/1994, ore 17, aula G

Marco Pedicini

Riduzione delle dimostrazioni: modelli algebrici

Abstract
Gli sviluppi recenti della teoria della dimostrazione riguardano lo studio di “modelli” della riduzione di dimostrazioni (“Geometry of interactions”, J.Y.Girard).
Verranno presentate recenti proposte di modelli algebrici della riduzione.

giovedì 12/1/1995, ore 17, aula G

Giuseppe Jacopini

Una caratterizzazione della classe degli automi cellulari invertibili
(in collaborazione con G.Sontacchi)

Abstract
Viene introdotta la classe degli automi cellulari fortemente invertibili e vengono date motivazioni per questa scelta.
Si dimostra che ogni automa cellulare invertibile è o un automa fortemente invertibile o una potenza di un automa fortemente invertibile.

giovedì 26/1/1995, ore 17, aula G

Flavio Corradini

Bisimulations and models for nondeterministic systems

Abstract
Various equivalences relating concurrent systems with respect to their behaviour have been defined in the literature, having the aim to capture different aspects of nondeterministic computation.
Many of them are based on the notion of bisimulation: firstly, the best known ones will be presented (strong and weak bisimulation equivalences and branching bisimulation equivalence).
Then a new and more concrete one will be discussed: it takes into account not only the actions a process can perform but also the number of the different possibilities, and it has the advantage - compared to the other ones - to be fully abstract with respect to a denotational model based on a family of trees.
The last part of the talk relies on a work jointly written with Rocco De Nicola and Anna Labella.

giovedì 9/2/1995, ore 17, aula G

Claudio Bernardi

Funzioni che ammettono “catene decrescenti infinite”

Abstract
Sia f una funzione da un insieme in sé. Per "catena decrescente infinita" si intende una successione (a_n) tale che f(a_n+1)=a_n. E’ ovvio che una funzione che ammette punto fisso ammette anche catene decrescenti infinite. D’altra parte, in opportuni contesti topologici e logici, l’esistenza di catene decrescenti infinite si dimostra in condizioni più generali di quelle che garantiscono l’esistenza di punti fissi.
Mentre un teorema di punto fisso permette, in un certo senso, definizioni autoreferenti, l’esistenza di catene decrescenti infinite corrisponde a definizioni “infondate”.
Verranno presentati alcuni risultati, alcuni controesempi e molte congetture.

giovedì 23/2/1995, ore 17, aula G

Claudio Cerrato

Sistemi deduttivi per logiche modali

Abstract
Viene presentata una ricerca di approfondimento sui sistemi deduttivi per logiche modali, che ha portato all’introduzione di sequenti con segni metalinguistici (modal sequents), sequenti ad alberi di sequenti (cut-free modal sequents), sequenti ad alberi di sequenze (modal tree-sequents) e sistemi di deduzione naturale basati sull’implicazione stretta.

giovedì 9/3/1995, ore 17, aula G

Maurizio Proietti

A Language-independent Theory of Program Transformation
(joint work with A.Pettorossi)

Abstract
The program transformation methodology has been developed in the context of several programming languages: functional, logic, imperative, concurrent, etc..
We present a theory of program transformation which is parametric wrt the specific languange used to write programs. We show that the correctness of a transformation can often be proved by making very weak assumptions on the syntax and semantics of the given programming language.
We show also that known correctness results for the transformation of functional and logic programs can easily be derived within our theory.

giovedì 23/3/1995, ore 17, aula G

Aldo Ursini

Semantiche relazionali per logiche sottostrutturali e lineari

Abstract
Richiamo sulle logiche sottostrutturali (calcoli dei sequenti senza qualcuna delle regole strutturali), sul calcolo di Lambek e sulle logiche lineari (commutativa, ciclica, non commutativa). Richiamo sulle rispettive semantiche: cornici ternarie e binarie - come presentate da Dosen - e spazi delle fasi (Girard, Yetter, Abrusci). Una semantica relazionale in presenza di negazioni e di leggi di De Morgan: fasoidi, fasoidi ridotti e loro proprietà. Risultati di completezza. Rapporti con la semantica algebrica. Esempi ed applicazioni.

giovedì 6/4/1995, ore 17, aula G

Piero Pagliani

Il ruolo della semantica nella teoria e nelle applicazioni della logica

Abstract
Negli ultimi tempi l’utilizzo di tecniche logico-semantiche in diversi campi applicativi ha, in qualche misura, messo in discussione i confini convenzionali tra sintassi e semantica. In particolare, a partire dagli ultimissimi anni, sta assumendo rilievo un programma di ricerca che pone al suo centro il concetto di "sistemi di informazione come sistemi semantici", e che deriva direttamente dalla grande scuola logico-algebrica polacca. Passando in rassegna risultati chiave in campo logico si cercherà di inquadrare la filosofia di questo programma di ricerca, discutendo il ruolo ricoperto dalla semantica a partire dai classici teoremi di completezza fino ai Labelled Deductive Systems proposti proposti ultimamente da Dov Gabbay come framework unificante per un ampio ventaglio di approcci logici (logica intuizionista, logiche della rilevanza, logiche non monotoniche, logica lineare, calcolo di Lambek, logiche modali, ecc...), cercando di mettere in luce il ruolo di trait d’union che assume la semantica algebrica in connessione alle nozioni di "elementi ideali e prototipali".
Un breve excursus cercherà di dimostrare che simili elementi ricoprono un ruolo centrale anche nella logica classica indiana.

giovedì 20/4/1995, ore 17, aula G

Giambattista Amati

L'eliminazione della regola di contrazione, risoluzione e tableaux: il caso intuizionista.

Abstract
La risoluzione può essere vista come una regola che stabilisce dei "bindings" tra differenti rami di un tableau. Nel calcolo mediante tableaux, invece, non si tiene conto di quello che avviene su due rami diversi: in molti casi ciò è motivo di inefficienza. Nel caso della logica proposizionale classica, per dedurre se da P è deducibile A, è possibile utilizzare prima le regole dei tableaux sull'insieme {TP, FA}, il più possibile ma senza creare ramificazioni; successivamente scambiare F con T e, infine, applicare la risoluzione in modo da rendere "lineare" la dimostrazione [Avron JAR 94].
Per la logica intuizionista il discorso si complica per il fatto che non è possibile ridurre le formule a "forma normale". Più in generale è possibile stabilire che in casi analoghi, in un paradigma dei tableaux con i soli {T, F} senza etichette, la regola di contrazione non è in generale eliminabile a meno di riscrivere "ad hoc" alcune formule mediante alcune equivalenze tipiche della logica in considerazione [per l'intuizionismo si veda Dyckhoff JSL92].
Nel seminario si presenta un metodo uniforme di tableaux con etichette senza la regola di contrazione e si discute come combinare risoluzione e tableaux in logica intuizionista.

giovedì 4/5/1995, ore 17, aula G

Carlo Cellucci

Gli alberi con tagli analitici

Abstract
Smullyan ha sottolineato che l'importanza delle dimostrazioni senza tagli non dipende dall'eliminazione dei tagli di per sé ma piuttosto dal fatto che tali dimostrazioni soddisfano la proprietà della sottoformula. Conformemente a questo punto di vista, nel seminario si presentano gli alberi con tagli analitici, un sistema da cui i tagli non possono essere eliminati ma che soddisfano la proprietà della sottoformula.
Come i tableaux, gli alberi con tagli analitici sono un sistema di refutazione ma, a differenza dei tableaux, essi hanno un'unica regola di inferenza (una forma analitica della regola del taglio) e parecchie regole di chiusura dei rami.
Il principale vantaggio degli alberi con tagli analitici rispetto ai tableaux è l'efficienza: mentre gli alberi con tagli analitici possono simulare i tableaux con un aumento di complessità tutt'al più di un fattore costante, i tableaux non possono simulare polinomialmente gli alberi con tagli analitici.
In effetti questi ultimi, nonstante la loro estrema semplicità, sono intrinsecamente più efficienti di qualsiasi sistema senza tagli e hanno la stessa efficienza della risoluzione al livello proposizionale.

giovedì 18/5/1995, ore 17, aula G

FranK W. Lawvere

The algebra of time