Benvenuto
Gruppo di Logica e Geometria della Cognizione
coordinatore: V. Michele Abrusci

 

Dipartimento di Matematica e Fisica
Università Roma Tre
Largo San Leonardo Murialdo 1
00144 Roma -Italia

 

Il fondamento scientifico della costituzione del gruppo risiede nell'interesse che tutti i suoi componenti portano alla moderna teoria della dimostrazione. Questo settore della logica matematica ha conosciuto recentemente una vera e propria "rinascita", dovuta al suo incontro con l'informatica: la corrispondenza di Curry-Howard stabilisce una corrispondenza tra dimostrazioni e programmi e tra esecuzione dei programmi ed eliminazione del taglio (un procedimento di trasformazione delle dimostrazioni ben noto ai logici). La scoperta di questa semplice e fondamentale corrispondenza è il punto di partenza per un nuovo approccio alla nozione di costruttività in logica ed alla programmazione in informatica.

In quest'ambito si colloca l'apparizione della logica lineare, che unisce gli aspetti "costruttivi" della logica intuizionista alle simmetrie della logica classica. La logica lineare nasce da un'analisi matematica molto fine della semantica delle dimostrazioni della logica intuizionista. Dalla sua apparizione nel 1986, essa si è imposta come strumento usato in vari settori di ricerca, dalla teoria della dimostrazione al lambda-calcolo, dalle macchine astratte al calcolo distribuito, dalla teoria della complessità alla programmazione logica.


News

Seminari di J.-Y. Girard a Roma Tre

Speaker:
Jean-Yves Girard, Université d'Aix-Marseille
Quando:
18/11/2016 - 11:30
Dove:
Aula Verra, Università Roma Tre, via Ostiense 234, Roma
Abstract

Le Fantôme de la transparence
Un ripensamento dei fondamenti filosofici della logica e della teoria dei proof-net

Seminari di J.-Y. Girard a Roma Tre

18 Novembre, 25 Novembre, 2 Dicembre, 9 Dicembre 2016
ore 11.30-13.30
Aula Verra, Università Roma Tre, via Ostiense 234, Roma

Jean-Yves Girard (professore emerito presso l'Université d'Aix-Marseille), ospite nei mesi di novembre e dicembre presso il Dipartimento di Matematica e Fisica dell'Università Roma Tre, terrà quattro seminari con il seguente calendario:

Venerdì 18 Novembre: Qu'est-ce qu'une réponse ?
Venerdì 25 Novembre: Qu'est-ce qu'une question ?
Venerdì 2 Dicembre: D'où vient la certitude ?
Venerdì 9 Dicembre: La foutue réalité

I seminari si terranno dalle ore 11:30 alle ore 13:30 presso l'Aula Verra del Dipartimento di Filosofia, Comunicazione e Spettacolo, Università Roma Tre, via Ostiense 234, Roma.

I seminari, in lingua francese, tratteranno ciascuno una parte del volume Le Fantôme de la transparence (Editions Allia, Paris, 2016). In questo testo Girard propone un ripensamento dei fondamenti filosofici della logica, a partire dalla consapevolezza, maturata attraversi i risultati limitativi della logica del XX secolo e il più recente incontro della logica matematica con il mondo dell'informatica teorica, del fallimento della pretesa trasparentista. In un precedente articolo che ha ispirato il volume, Girard scriveva:

Le fantasme (ou fantôme) de la transparence est l’idée qu’au-delà de la perception immédiate, existerait un monde, un niveau de lecture, complétement intelligible, i.e., explicite et immédiat. Cette transparence nous dévoilerait ainsi un envers unidimensionnel de l’univers. Ce qui part d’une prémisse correcte, dépasser les apparences ; mais, pour ce faire, on imagine un autre côté du miroir aux contours nets, précis et sans la moindre ambiguïté. Le monde devient un rébus dont il suffit de trouver la clef : tout serait tellement immédiat, lisible, qu’il n’y aurait même plus besoin de poser de questions, i.e., de penser. (Girard, Le Fantôme de la transparence, 2014)

Da riflessione teorica sui fondamenti, la proposta di Girard, il cui nome è legato all'invenzione della logica lineare, si estende a una ricostruzione tecnica delle basi della logica: la messa in discussione dei presupposti trasparentisti della conoscenza si traduce in un profondo ripensamento della teoria dei proof-net, da lui stesso elaborata a partire dal 1987 per una presentazione geometrica delle dimostrazioni.

Per i loro contenuti e ambizioni, i seminari si indirizzano tanto a chi si interessa ai problemi della logica da un punto di vista filosofico e non tecnico, quanto a chi, da informatico o da matematico, è abituato a operare nella “sala macchine” dei linguaggi logici.

Chi fosse interessato a partecipare è pregato di segnalare il proprio nome all'indirizzo: paolo.pistone@uniroma3.it.

I seminari saranno trasmessi in diretta streaming sul canale youtube
https://www.youtube.com/channel/UCSS_Jzga01PmGKghCJzh2Vw.

Le slides dei seminari sono disponibili qui.


Il !-calcolo: una variante del lambda-calcolo che generalizza la chiamata per nome e la chiamata per valore

Speaker:
Giulio Guerrieri (Università Roma Tre - Université d'Aix-Marseille)
Quando:
28/10/2016 - 11:30
Dove:
Aula 311 della Sezione di Matematica del Dipartimento di Matematica e Fisica Largo San Leonardi Murialdo 1, Roma – Palazzina C, III piano
Abstract

Introdurremo e studieremo il !-calcolo, un calcolo funzionale non tipato in cui l'operatore di promozione della Logica Lineare fa esplicitamente parte della sintassi e l'applicazione è bilineare.
Questo calcolo, che può essere visto come una versione non tipata del calcolo Call-By-Push-Value di Paul Levy, sussume sia il lambda-calcolo per nome sia il lambda-calcolo per valore, in quanto consente (e internalizza) una fattorizzazione delle due traduzioni di Girard della logica intuizionista nella Logica Lineare.
Costruiremo un modello denotazionale del !-calcolo basato sulla interpretazione relazionale della Logica Lineare e dimostreremo un teorema di correttezza per tale modello ricorrendo a una versione con risorse del !-calcolo basato sulla Logica Lineare Differenziale.


Connettivi generalizzati in Logica Lineare Moltiplicativa

Speaker:
Roberto Maieli (Università Roma Tre)
Quando:
21/10/2016 - 11:30
Dove:
Aula 311 della Sezione di Matematica del Dipartimento di Matematica e Fisica Largo San Leonardi Murialdo 1, Roma – Palazzina C, III piano
Abstract

This talk addresses the following questions:
1) what is a generalized (n-ary) connective of the multiplicative fragment of linear logic (MLL)?
2) are there generalized connectives that cannot be defined by those primitive binary ones (Tensor and Par)?
3) is there a way to sequentialize proof-nets containing two orthogonal generalized non binary-definable conclusions?


Tipaggio in Ludica del frammento moltiplicativo di CCS (Calculus of Communicating Systems)

Speaker:
Stefano Del Vecchio (Università Roma Tre - LIPN, Université Paris Nord)
Quando:
07/10/2016 - 11:30
Dove:
Aula 311 della Sezione di Matematica del Dipartimento di Matematica e Fisica Largo San Leonardi Murialdo 1, Roma – Palazzina C, III piano
Abstract

In the setting of process algebras (CCS; pi-calculus; etc.), linear logic gave a substantial contribution to the extension of the Curry-Howard isomorphism to such calculi, used to model concurrent systems. The focus of this work is the multiplicative fragment of CCS, which simpli_es the problem, and thus the solutions, which can be later extended to the full calculus.
The main issue is to preserve the non-determinism of the calculus. By a direct typing in linear logic, this non determinism is lost, due to the confluent nature of cut elimination - only one of the possible outcomes can be kept. Type systems based on linear logic de_ne a correspondence between CCS terms - or executions of a term - and LL proof-nets, often imposing determinism in execution either by restricting the process to functional behaviour, or typing only a part of all the possible execution paths.
In this work we de_ne a translation of MCCS into Ludics, in order to obtain a type able to describe all the execution paths and thus the process itself. Due to the interactive nature of its objects, the designs, ludics seems the right setting to de_ne a correspondence between interaction (the equivalent of cut elimination) and execution. Behaviours, sets of designs closed by bi-orthogonality, are used to type MCCS terms. Exploiting particular noncommutative designs we impose restrictions on behaviours, in order to rule out the interactions not corresponding to possible execution on the translated MCCS term. Indeed, since some execution steps do not commute, a partial order is de_nable on execution; non commutativity in ludics is used to match this partial order, allowing in the behaviour only the designs whose interaction, with its orthogonal, do correspond to possible execution paths.
In this way we obtain a one to one correspondence between interaction and execution: for each execution path on the term there is a corresponding interaction of the behaviour with its orthogonal, and vice versa, preserving non-determinism to some extent.


Open Call-by-Value (joint work with Beniamino Accattoli)

Speaker:
Giulio Guerrieri (Università Roma Tre - Université d'Aix-Marseille)
Quando:
11/03/2016 - 11:00
Dove:
Aula 311, Dipartimento di Matematica e Fisica, L.go San Leonardo Murialdo 1.
Abstract

The elegant theory of the call-by-value lambda-calculus relies on
weak evaluation and closed terms, that are natural hypotheses in
the study of programming languages. To model proof assistants,
however, strong evaluation and open terms are required, and it is
well known that the operational semantics of call-by-value becomes
problematic in this case, as first pointed out by Paolini and Ronchi
della Rocca. Here we study the intermediate setting—that we call
Open Call-by-Value—of weak evaluation with open terms, on top
of which Grégoire and Leroy designed the abstract machine of Coq.
Various calculi for Open Call-by-Value already exist, coming from
logical, semantical, or implementative points of view, each one with
its pros and cons. This paper presents a detailed comparative study
of their operational semantics. First, we show that all calculi are
equivalent from a termination point of view, justifying the slogan
Open Call-by-Value. Second, we compare their equational theories.
Third, we present a detailed quantitative analysis of the time cost
model. Four, we introduce a new simple abstract machine, and
prove it a reasonable implementation of Open Call-by-Value with
respect to its cost model. Along the way, there emerges a sharp
deconstruction of call-by-value evaluation and of the complexity of
its implementations.


Diagrammi di corde per le reti di prova

Speaker:
Matteo Acclavio (Institut de Mathématiques de Marseille)
Quando:
12/02/2016 - 11:00
Dove:
Dipartimento di Matematica e Fisica, L.go S. Leonardo Murialdo 1, Aula 311
Abstract

Le reti di prova in MELL necessitano di criteri di correttezza non locali o esterni alla sintassi delle reti di interazioni: connessione, aciclicita', box, salti.
Dopo aver introdotto la sintassi dei diagrammi di corde per le categorie monoidali, verra' descritto come ricostruire in questi contesti modelli di proof net con un unico criterio di correttezza locale per MLL e MELL (con o senza costanti).


New trends on linear logic proof-nets

Organizzatori:
Lorenzo Tortora de Falco (Dipartimento di Matematica e Fisica, Università Roma Tre)
Giulio Guerrieri (I2M, Université d'Aix-Marseille)
Inizio:
21/12/2015
Fine:
22/12/2015
Dove:
Università Roma Tre, Dipartimento di Matematica e Fisica (Largo San Leonardo Murialdo, 1 - 00146 Roma), Room 311 (3rd floor)
Descrizione

Program:

December 21, Monday

11:00-11:15 Ouverture
11:15-12:00 Daniel De Carvalho The relational model is injective for Multiplicative Exponential Linear Logic
12:00-12:30 Lorenzo Tortora de Falco/Luc Pellissier Some remarks about connectedness, Taylor expansion and injective relational semantics

12:30-14:00 lunch

14:00-14:45 Lionel Vaux Looking at cut elimination through the lens of Taylor expansion
14:45-15:15 Marco Solieri Taylor-expansion, cut elimination and geometry of interaction
15:15-16:00 Damiano Mazza Proof Nets in Space

16:00-16:15 coffee break

16:15-16:45 Ugo Dal Lago The Geometry of Synchronization
16:45-17:15 Anna Chiara Lai, Marco Pedicini, Silvia Rognone Quantum entanglement and the Bell Matrix: the encoding in QMLL

December 22, Tuesday

9:15-10:00 Marc Bagnol TBA

10:00-10:30 coffee break

10:30-12:30 open session Representation of nets
talks and micro-talks by Giulio Guerrieri/Lorenzo Tortora de Falco, Luc Pellissier, Thomas Ehrhard, Beniamino Accattoli, Vito Michele Abrusci.

12:30-14:30 lunch

14:30-17:00 open session Correctness criteria
talks and micro-talks by Roberto Maieli, Vito Michele Abrusci, Beniamino Accattoli, Marc Bagnol, Thomas Ehrhard.


Multi scale and multi omic approaches in systems medicine

Speaker:
Prof. Pietro Lio', Computer Laboratory, University of Cambridge, UK
Quando:
18/12/2015 - 11:30
Dove:
Dipartimento di Matematica e Fisica Universita' degli Studi Roma Tre AULA 311 (SEMINARI) Largo San L. Murialdo,1
Abstract

I will first introduce my current research on multi comics and multi scale modeling. Ductal carcinoma is one of the most common cancers among women, and the main cause of death is the formation of metastases. Through a branching process model, I describe the relation between the survival times
and the drivers mutations mainly involved in metastatic breast cancer. In particular, the model takes into account intracell to tissues dynamics in breast, blood and bone compartments and uses the gene expression profile of circulating tumour cells to predict personalised survival probability. I will end by introducing current work on logic approaches.


Algebraic Models for Systems Biology

Speaker:
Prof. Abdul Salam Jarrah
Quando:
03/12/2015 - 11:00
Dove:
Dipartimento di Matematica e Fisica Universita' degli Studi Roma Tre AULA 311 (SEMINARI) Largo San L. Murialdo,1
Abstract

Elucidating the topology and dynamics of biological networks from
experimental data is a central goal of systems biology. Recently
algebraic models have been introduced as a new framework for modeling
and analyzing biological networks as multi-states systems,
generalizing Boolean networks. Within this framework, using tools from
computational algebra and algebraic geometry, algorithmic methods that
find and present the model space have been developed, and the class of
nested canalyzing models have been characterized. Furthermore,
methods for analyzing the dynamics of monomial models have been
developed. The algebraic framework as well as some of the mentioned
methods will be presented in this talk.


Results and problems around a discrete dynamical system

Speaker:
Prof. Attila Pethö, University of Debrecen, Hungary
Quando:
13/11/2015 - 11:30
Dove:
Dipartimento di Matematica e Fisica Università degli Studi Roma Tre Aula 314, terzo piano, edificio C - Largo San Leonardo Murialdo,1
Abstract

To the real vector TeX Embedding failed! we associate the mapping TeX Embedding failed! such that TeX Embedding failed!. This is the discrete dynamical system, which is the topic of our talk. It was introduced by S. Akiyama, H. Brunotte, T. Borb\'ely, J. Thuswaldner and called shift radix system, shortly SRS. The orbits of the iterations of TeX Embedding failed! can be divergent or periodic. In the later case they can be ultimately zero or not. The distinction of these cases leads to hard algorithmic and complexity question provided TeX Embedding failed! is a rational vector. We report on topological and geometric properties of regions associated to SRS.