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

Numeration 2017

Organizzatori:
Vilmos Komornik
Marco Pedicini
Inizio:
05/06/2017
Fine:
09/06/2017
Dove:
Università Roma Tre -- Argiletum Via Madonna dei Monti 40 Sala Urbano VIII
Descrizione

The goal of this workshop is to bring together researchers interested in interactions between numeration systems, ergodic theory, number theory and combinatorics.


Le teorie del ragionamento nella prospettiva dei due processi: la distinzione tra processi inferenziali intuitivi e riflessivi

Speaker:
Massimo Marraffa
Quando:
12/05/2017 - 11:30
Dove:
Dipartimento di Matematica e Fisica, Aula 311, pal. C, l.go S. Leonardo Murialdo 1
Abstract

Secondo le teorie ‘dei due sistemi’, il sistema cognitivo umano sarebbe composto da almeno due sottosistemi. Il Sistema 1 opera in modo inconscio e rapido, producendo risposte intuitivamente cogenti a problemi di apprendimento e ragionamento. Il Sistema 2 opera invece in modo cosciente e lento, entrando in azione solo quando il soggetto è indotto a svolgere un compito inferenziale in modo riflessivo.
Nel mio intervento solleverò due obiezioni a questa famiglia di teorie. 
(1) L’immagine di due sistemi neurocognitivi che esistono l’uno accanto all’altro e competono per il controllo del comportamento dell’agente ha scarsa plausibilità evoluzionistica: perché mai l’evoluzione invece di modificare, estendere o integrare l’architettura del preesistente S1, avrebbe ricominciato tutto da capo con S2? Più plausibile è allora l'ipotesi che i processi di S2 siano realizzati in quelli di S1 . Ossia non vi sono due sistemi distinti, bensì due livelli o strati di processi cognitivi, l’uno dipendente dalle operazioni dell’altro. In quest’ottica, non occorre supporre che l’evoluzione abbia fortemente arricchito l’architettura di S1 per far nascere S2; basta immaginare che i sottosistemi di S1 siano stati orchestrati e utilizzati in modi nuovi.
(2) Ammettiamo la realtà della distinzione fra processi di ragionamento intuitivi e riflessivi; e accogliamo la congettura che il ragionamento riflessivo sia in larga misura realizzato dalle operazioni cicliche di processi intuitivi inconsci (fra cui i sottosistemi normalmente assegnati a S1). Ciò non equivale però a una conferma dell’ipotesi dei due sistemi; e questo perché -- è stato sostenuto -- la distinzione fra S1 e S2 non coincide con la distinzione fra ragionamento intuitivo e ragionamento riflessivo.


Laver tables

Speaker:
Patrick Dehornoy (Université Caen-Normandie)
Quando:
17/02/2017 - 11:30
Dove:
Dipartimento di Matematica e Fisica, Aula 311 Largo San Leonardo Murialdo, 1
Abstract

Discovered (or invented?) by Richard Laver in the 1990s, the tables that are now known as Laver tables are finite structures obeying the self-distributivity law x(yz)=(xy)(xz). Although their construction is totally explicit, some of their combinatorial properties are (so far) established only using unprovable set theoretical axioms, a quite unusual and paradoxical situation. We shall explain the construction of Laver tables, their connection with set theory, and their potential applications in low-dimensional topology via the recent computation of some associated cocycles.


Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics

Speaker:
Matteo Acclavio (Université de Caen)
Quando:
10/02/2017 - 11:30
Dove:
Aula 311 (Palazzina C, Dipartimento di Matematica e Fisica, l.go S. Leonardo Murialdo 1)
Abstract

Le reti di prova sono una sintassi per le prove della logica lineare con una rappresentazione geometrica intuitiva che permette di definire una relazione di equivalenza tra derivazioni meno fine rispetto alla pura equivalenza sintattica.
In questo incontro daremo una sintassi bidimensionale alternativa per le derivazioni della logica lineare moltiplicativa. Nel nostro caso, la sintassi dei diagrammi di corde permette la definizione di un formalismo in cui verificare se un diagramma corrisponde ad una prova può essere verificato in tempo lineare.
Inoltre mostreremo come questa sintassi possa essere utilizzata per definire una semantica denotazionale per la logica lineare moltiplicativa con unità tramite classi di equivalenza di diagrammi (generata da una riscrittura terminante).


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.


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.


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