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

Linear Implicative Algebras, a Brouwer-Heyting-Kolmogorov interpretation of linear logic

Speaker:
Luc Pellissier (IRIF, Université Paris 7)
Quando:
18/01/2019 - 12:00
Dove:
Aula 311, Palazzina C, Dipartimento di Matematica e Fisica, l.go S. Leonardo Murialdo 1
Abstract

Implicative Algebras were recently introduced by Alexandre Miquel as a unified framework for forcing and realisability, whose particularity is to interpret terms and formulæ uniformly. In this ongoing work, we show how linear logic fits in this picture: we present a notion of model of intuitionistic linear logic in which sits both syntactic models and a localized phase semantics ; and show how to transform such a model into an algebra allowing to interpret faithfully all the connectives of classical linear logic.


Types by Need (joint work with Beniamino Accattoli and Maico Leberle)

Speaker:
Giulio Guerrieri (University of Bath)
Quando:
18/01/2019 - 11:00
Dove:
Aula 311, Palazzina C, Dipartimento di Matematica e Fisica, l.go S. Leonardo Murialdo 1
Abstract

A cornerstone of the theory of ?-calculus is that intersection types characterise termination properties. They are a flexible tool that can be adapted to various notions of termination, and that also induces adequate denotational models.
Since the seminal work of de Carvalho in 2007, it is known that multi types (i.e. non-idempotent intersection types) refine intersection types with quantitative information and a strong connection to linear logic. Typically, type derivations provide bounds for evaluation lengths, and minimal type derivations provide exact bounds.
De Carvalho studied call-by-name evaluation, and Kesner used his system to show the termination equivalence of call-by-need and call-by-name. De Carvalho’s system, however, cannot provide exact bounds on call-by-need evaluation lengths.
In this paper we develop a new multi type system for call-by-need. Our system produces exact bounds and induces a denotational model of call-by-need, providing the first tight quantitative semantics of call-by-need.


Coends and proof equivalence in second order multiplicative linear logic

Speaker:
Paolo Pistone (Università di Tubinga)
Quando:
21/12/2018 - 16:00
Dove:
Aula 311, Dipartimento di Matematica e Fisica, l.go S. Leonardo Murialdo 1, Palazzina C
Abstract

Proof nets for multiplicative linear logic (MLL) provide canonical representations of proofs: they are permutation-independent, separable and are injectively interpreted in the relational and coherent semantics. None of these properties scales to second order multiplicative linear logic (MLL2): proof nets for MLL2 are not invariant with respect to all valid permutations, are not separable and are not injectively interpreted in either the relational or coherent semantics. This problem is related to the interpretation of the existential quantifier. In categorical terms this should correspond to a coend, whereas the usual proof net representation violates the diagrams defining a coend. Starting from this intuition, we investigate the problem of defining canonical proof nets for MLL2 as a coherence problem for coends over a compact-closed category and we show some results concerning some fragments of MLL2.


La teoria della realizzabilità classica e l'assioma dell'ultrafiltro.

Speaker:
Davide Barbarossa (Università Roma Tre/Université d'Aix-Marseille)
Quando:
20/07/2018 - 11:30
Dove:
Aula 311, Palazzina C, Dipartimento di Matematica e Fisica, l.go S. Leonardo Murialdo 1
Abstract

La teoria della realizzabilità classica è stata introdotta da J.-L. Krivine negli anni 2000 a seguito di una intuizione di T. Griffin, che ha tipato l'istruzione "callcc" in Scheme (simile alla istruzione "try-catch" in Java) con la regola dell'assurdo (nella forma di legge di Pierce). Questo ha portato a generalizzare la corrispondenza di Curry-Howard a tutta la logica classica, ed anche oltre: assiomatizzando la nozione di programma (lambda-termine) e di esecuzione (programma + pila di esecuzione), grazie alle "algebre di realizzabilità", si riesce ad associare programmi a dimostrazioni (classiche) che usino assiomi supplementari - come ad esempio quelli della teoria degli insiemi. Questi programmi, chiamati "realizzatori" della formula dimostrata, ne forniscono una "giustificazione" che è una semantica intermedia tra quella Tarskiana (vero/falso) e quella data dalle dimostrazioni. In questo incontro ci concentreremo sull'assioma dell'ultrafiltro ("esiste un ultrafiltro non triviale sull'algebra di Boole delle parti di N") nel quadro della aritmetica al secondo ordine.


On the Taylor expansion of lambda-terms and the groupoid structure of their rigid approximants

Speaker:
Federico Olimpieri (Université d'Aix-Marseille)
Quando:
15/06/2018 - 11:30
Dove:
Dipartimento di Matematica e Fisica, l.go S. Leonardo Murialdo 1, palazzina C, aula 311
Abstract

We show that the normal form of the Taylor expansion of a lambda-term is isomorphic to its Böhm tree, improving Ehrhard and Regnier’s original proof along three independent directions. First, we simplify the final step of the proof by following the left reduction strategy directly in the resource calculus, avoiding to introduce an abstract machine ad-hoc. We also introduce a groupoid of permutations of copies of arguments in a rigid variant of the resource calculus, and relate the coefficients of Taylor expansion with this structure, while Ehrhard and Regnier worked with groups of permutations of occurrences of variables. Finally, we extend all the results to a non-deterministic setting: by contrast with previous attempts, we show that the uniformity property that was crucial in Ehrhard and Regnier’s approach can be preserved in this setting.


Introduction to numeration systems: number expansions in lattices

Docente:
Prof. Attila Kovacs, Eötvös Loránd University Faculty of Informatics, Dept. of Comp. Algebra
Inizio:
07/05/2018
Fine:
08/05/2018
Dove:
Aula 311, Edificio C, Dipartimento di Matematica e Fisica, Largo San Leonardo Murialdo 1
Descrizione

Aula 211, Lunedì 7 Maggio 2018, dalle ore 9 alle ore 11
Aula 211, Martedì 8 Maggio 2018, dalle ore 9 alle ore 11
Aula 211, Martedì 8 Maggio 2018, dalle ore 14 alle ore 18

1. Fundamentals of number expansions, mathematical background
2. Decision and classification problems, algorithmical complexity
3. Fast computations: expansivity, congruences
4. Discrete dynamic, attractors and periodic elements
5. Optimizing by basis transformation
6. Generalized binary number systems
7. Construction problems, open questions
8. Block diagonal systems, simultaneous systems
9. Applications

Literature:
S. Akiyama , T. Borbély , H. Brunotte , A. Pethö , J. M. Thuswaldner:
On a generalization of the radix representation -- a survey (2004) IN ”HIGH PRIMES AND MISDEMEANOURS: LECTURES IN HONOUR OF THE 60TH BIRTHDAY OF HUGH COWIE WILLIAMS”, FIELDS INSTITUTE COMMUNICATIONS

A. Kovács papers in
http://compalg.inf.elte.hu/~attila/Publications.html


Universally optimal mitigation strategies for leakage of information

Speaker:
Prof. Pasquale Malacaria, Queen Mary University of London
Quando:
18/05/2018 - 11:30
Dove:
Aula 311, Dipartimento di Matematica e Fisica, Universita’ Roma Tre, Largo San Leonardo Murialdo 1
Abstract

Software systems may leak information about confidential data.
Information theory helps in mathematically analyze and automatically quantify such leaks.

However, there is an (uncountable) infinity of leakage measures.
Hence a question arises: can we design countermeasures to information leakage
that are universally optimal, i.e. that guarantee minimal leakage no matter
which leakage measure is chosen?

We show contexts when this can be achieved, a counterexample to a general
solution and discuss potential applications of these techniques to security and privacy problems.

(This is a joint work with Arman Khouzani)


Collusions : toward an agonal ontology

Speaker:
Jean-Baptiste Joinet (Université Lyon 3 - Centre Cavaillès, ENS, Paris)
Quando:
02/05/2018 - 11:00
Dove:
Dipartimento di Matematica e Fisica, Lgo S. Leonardo Murialdo 1, palazzina C, aula 311 (terzo piano)
Abstract

In Frege and Russell’s line, the main tool to propagate ontology toward higher orders is realized by quotienting sets by equivalence relations. Indeed, this leads to produce, at the next order, separated individualities (disjoint non empty subsets covering the original set) and this in such a way that this separation is conceptually generated from a relation at the initial order.
This way to relate ontology and equivalence relations is deeply Parmenidian in inspiration : non only because it considers individualities independently of time (first point), but also because it propagates at the next order the idea of an autonomy of individualities, i.e. the idea that the individuality of individuals is independent of any relational commitment between them (second point).
"Denotational semantics of programs" (the research programme launched by Strachey and Scott around 1969) can be seen as a first step to substitute to Parmenidian ontology an Heraclitean ontology, in the sense that it faces the first point (individualities in time): in a computational universe, transformation comes first and separation phenomenas are generated by (and compatible with) these transformation.
In that talk, I will present my current work on a complementary program toward a non Parmenidian ontological point of view facing the second point (Agonal ontology) which starts by introducing a generalization of equivalence relations, collusions (total and surjective collusive relations). After having presented their main properties, notably with respect to the partitioning purpose, I will conclude about logical potential interpretations.


Dalle prove sintattiche alle combinatorial proofs

Speaker:
Matteo Acclavio (LIX - INRIA Parsifal Team)
Quando:
23/03/2018 - 14:30
Dove:
Dipartimento di Matematica e Fisica, Università degli Studi Roma Tre, largo San Leonardo Murialdo,1 - Pal.C - AULA 311
Abstract

In questo incontro studieremo come le combinatorial proofs di Hughes possono essere utilizzate per definire una nozione di equivalenza tra dimostrazioni per la logica classica. Mostreremo poi come diversi formalismi (calcolo dei sequenti, alberi di refutazione e resolution) possano essere tradotti in combinatorial proofs e quale nozione di identità viene definita da ciascuno di essi.


Negative local feedbacks in Boolean networks

Speaker:
Paul Ruet (CNRS, IRIF, Université Paris-Diderot)
Quando:
23/03/2018 - 11:00
Dove:
Dipartimento di Matematica e Fisica, Università degli Studi Roma Tre, largo San Leonardo Murialdo,1 - Pal.C - AULA 311
Abstract

We shall be interested in the asymptotic dynamical properties of Boolean networks: fixed points, attractive cycles, and more general attractors. While the properties of Boolean networks without local cycle or without local positive cycle are rather well understood, recent literature raises the following two questions about networks without local negative cycle. Do they have at least one fixed point? Should all their attractors be fixed points? We give negative answers to both questions: we show that and-nets without local negative cycle may have no fixed point, and that Boolean networks without local negative cycle may have (antipodal) attractive cycles.