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

Stabilization and expansion of simple dynamic random graph models for Bitcoin-like unstructured P2P networks

Speaker:
Francesco Pasquale
Quando:
03/07/2020 - 15:00
Dove:
videoconferenza online
Abstract

Venerdì 3 luglio 2020 alle ore 15:00, il prof. Francesco Pasquale dell'Università Tor Vergata, terrà il seminario dal titolo "Stabilization and expansion of simple dynamic random graph models for Bitcoin-like unstructured P2P networks".

Abstract

The Bitcoin P2P network is formed by thousands of nodes running the Bitcoin protocol. While the nodes participating in the network are mostly known, the peer discovery process in the protocol is explicitly designed to hide the global network structure. In this talk, we present a simple dynamic random graph model inspired by the peer discovery process in the Bitcoin protocol and we analyze its robustness with respect to stabilization and expansion: We show that the network dynamics quickly converges to a stable random graph that turns out to be a good expander, with high probability.

The talk is based on joint work with Luca Becchetti, Andrea Clementi, Emanuele Natale, and Luca Trevisan.

Per partecipare al seminario cliccare sul seguente link Teams meeting


Clique is hard on average for regular resolution

Speaker:
Massimo Lauria
Quando:
19/06/2020 - 11:30
Dove:
videoconferenza online
Abstract

Venerdì 19 giugno 2020 alle ore 11:30, il prof. Massimo Lauria dell'Università di Roma La Sapienza, presenterà il seminario di Logica e Informatica Teorica dal titolo "Clique is hard on average for regular resolution".

Abstract

The obvious running time to check whether a graph of n vertices has a clique of size k is roughly n^k. In this work we prove unconditionally that a large variety of state-of-the-art algorithms, even some that are widely used in practice, require running time n^Omega(k). More precisely we prove that for k ≤ n^0.25 regular resolution proofs (i.e. read-once branching programs) have to be of size n^Omega(k) to establish that an Erdos-Rényi graph with appropriately chosen edge density does not contain a k-clique. We remark that these lower bounds do not depend on unproved assumptions like P vs NP, and apply to whatever algorithm that, on k-clique free graphs, produces a regular resolution proofs of such fact. The talk is based on a joint work appeared at STOC 2018, with: Albert Atserias, Ilario Bonacina, Susanna F. de Rezende, Jakob Nordström and Alexander A. Razborov.

Per partecipare al seminario, richiedere il link all’indirizzo email vitomichele.abrusci@uniroma3.it o cliccare sul seguente link Teams meeting


Compositional theories for embedded programming

Speaker:
Margherita Zorzi
Quando:
26/06/2020 - 15:00
Dove:
videoconferenza online
Abstract

Venerdì 26 giugno 2020 alle ore 15:00, la prof.ssa Margherita Zorzi dell'Università di Verona, presenterà il seminario di Logica e Informatica Teorica dal titolo "Compositional theories for embedded programming".

Abstract:

Embedded programming style allows to split the syntax in two parts, representing respectively a host language H and a core language C embedded in H. This formally models several situations in which a user writes code in a main language and delegates some tasks to an ad hoc domain specific language. Moreover, as showed in recent years, a particular case of the host-core approach allows a flexible management of data linearity, which is particularly useful in non-classical computational paradigms such as quantum computing. The definition of a systematised type theory to capture and standardize common properties of embedded languages is partially unexplored. We present a flexible fragment of such a type theory, together with its semantics in terms of enriched categories. We introduce the calculus HC0 and we use the notion of internal language of a category to relate the language to the class of its models, showing the equivalence between the category of models and the one of theories. This provides a stronger result w.r.t. standard soundness and completeness since it involves not only the models but also morphisms between models. We observe that the definition of the morphisms between models highlights further advantages of the embedded languages and we discuss some concrete instances, extensions and specializations of the syntax and the semantics.

Per partecipare al seminario, richiedere il link all’indirizzo email vitomichele.abrusci@uniroma3.it o cliccare sul seguente link Teams meeting


Proof-nets and laws of Categorial Grammar

Speaker:
Vito Michele Abrusci
Quando:
12/06/2020 - 15:00
Dove:
videoconferenza online
Abstract

Venerdì 12 giugno 2020 alle ore 15:00, il prof. Vito Michele Abrusci dell'Università Roma Tre, presenterà il seminario di Logica dal titolo: "Proof-nets and laws of Categorial Grammar".

Abstract:

I present a geometrical analysis – i.e. by means of proof nets of the multiplicative fragment of Cyclic Linear Logic - of the principles that lay at the basis of Categorial Grammar and of the Lambek Calculus: Residuation laws, Monotonicity laws, Application laws, Expansion laws, Type-raising laws, Composition laws, Geach laws and Switching laws.
This geometrical analysis leads to better understand these laws, and to discover some laws have a common geometrical representation (the proofs of Application laws, Expansion Laws and Type-reasing laws are represented by proof-nets with two axiom links, whereas the proofs of Composition laws, Geach laws and Switching laws are represented by proof-nets with three axiom links).

The talk is based on a joint work with Claudia Casadio.

Per partecipare al seminario, richiedere il link all’indirizzo email vitomichele.abrusci@uniroma3.it o cliccare sul seguente link Teams Meeting


Automatic differentiation in PCF

Speaker:
Michele Pagani
Quando:
05/06/2020 - 15:00
Dove:
videoconferenza online
Abstract

Venerdì 5 giugno 2020 alle ore 15:00, il prof. Michele Pagani dell'Université Paris 7, presenterà il seminario di Logica e Informatica Teorica dal titolo: "Automatic differentiation in PCF".

Abstract:

Backpropagation is a classic automatic differentiation algorithm computing the gradient of functions specified by a certain class of simple, first-order programs, called computational graphs. It is a fundamental tool in several fields, most notably machine learning, where it is the key for efficiently training (deep) neural networks. Recent years have witnessed the quick growth of a research field called differentiable programming, the aim of which is to express computational graphs more synthetically and modularly by resorting to actual programming languages endowed with control flow operators and higher-order combinators, such as map and fold. We extend the backpropagation algorithm to a paradigmatic example of such a programming language: we define a compositional program transformation from PCF (a Turing complete simply-typed lambda-calculus) to itself augmented with a notion of linear negation, and prove that this computes almost everywhere the gradient of the source program with the same efficiency as first-order backpropagation. The transformation is completely effect-free and thus provides a purely logical understanding of the dynamics of backpropagation.

Per partecipare al seminario, richiedere il link all’indirizzo email vitomichele.abrusci@uniroma3.it o cliccare sul seguente link Teams Meeting


Logic programming with generalized multiplicative connectives

Speaker:
Matteo Acclavio (SAMOVAR - Telecom SudParis, INRIA – Saclay)
Quando:
29/05/2020 - 15:00
Dove:
in video conferenza
Abstract

Logic programming is a paradigm which makes use of mathematical logic to represent programs by means of sets of formal sentences. In this talk we recall Andreoli's logic programming paradigm, which is based on linear logic proof structures. We focus on the so called "multiplicative" fragment, that is, the one which only employs linear and context-free methods. We show how to revise this construction in order to accommodate specific generalized multiplicative connectives. This allows us to implement some non-linear and context-sensitive methods in a pure multiplicative fragment.

This talk is based on a joint work with Roberto Maieli

Per partecipare al seminario:

chiedere il link all’indirizzo email vitomichele.abrusci@uniroma3.it
o cliccare sul seguente link Microsoft Teams


LA LOGIQUE DÉCONFINÉE

Speaker:
Jean-Yves Girard (CNRS, Directeur de recherche émérite)
Quando:
29/05/2020 - 10:30
Dove:
videoconferenza online al link: https://us02web.zoom.us/j/89571804741?pwd=NWJubDlKdHYyTUVHWEx1SllwQ0Uxdz09
Abstract

Seminario di Logica

Venerdì 29 maggio 2020, ore 10h30

Jean-Yves Girard (CNRS, Directeur de recherche émérite)

LA LOGIQUE DÉCONFINÉE
Resumé

Nul besoin de système pour raisonner, il suffit d’utiliser des tests.

Jusqu’à une date récente, je pensais que cette approche d’usine achoppait
sur des problèmes de finitude. Mais si l’on considère des tests suffisants (pas nécessaires
donc), les batteries de tests peuvent rester finies.

L’opposition traditionnelle entre Curry et Church se retrouve sous la forme usage/usine.
L’usage (BHK) définit les signifiants logiques implicitement : le type comme comportement.
L’usine (Herbrand) définit les signifiants logiques explicitement : le type comme critère de correction.

Ces deux approches sont reliées par un résultat d’adéquation, élimination des coupures si
l’on veut : les tests suffisent à garantir l’usage.

La trinité réaliste axiomatique syntaxe/sémantique/méta est ainsi remplacée par une trinité
déréaliste usine/usage/adéquation.

Il seminario sarà tenuto in lingua francese.
________________________________________________________________________________
Join Zoom Meeting


Logic Beyond Formulas: the multiplicative case

Speaker:
Matteo Acclavio (SAMOVAR - Telecom SudParis, INRIA - Saclay, LIX - Ecole Polytechnique)
Quando:
21/02/2020 - 11:30
Dove:
Dipartimento di Matematica e Fisica, Aula 311, Palazzina C
Abstract

There is a well-known correspondence between formulas and cographs, which are unoriented graphs containing no chordless paths of length 3. The aim of this talk is to shape a proof system operating on general graphs instead of formulas. In such a proof system, we lose the tree structure of formulas corresponding to cographs. As a consequence, we can no longer use the standard proof theoretical methods relying on the tree structure of formulas: for instance, we are not able to identify the main connective of a formula.

Thanks to graphs modular decomposition and some techniques from deep inference, we are able to define a proof system with admissible cut rule and which is a conservative extension of MLL with mix.

This talk is based on a joint work with Ross Horne and Lutz Strassburger.


Multiplicatives

Speaker:
Roberto Maieli (Università Roma Tre)
Quando:
20/12/2019 - 11:30
Dove:
Aula 311, Palazzina C, Dipartimento di Matematica e Fisica, L.go San Leonardo Murialdo 1
Abstract

We investigate the notion of generalized link (module) of the pure multiplicative fragment of Linear Logic (MLL). We then present a computation paradigm based on a concurrent and incremental construction of graphical modular proofs of MLL.


Proof nets through the lens of graph theory

Speaker:
Nguyên Lê Thành Dung (LIPN, Université Paris 13)
Quando:
17/05/2019 - 11:30
Dove:
Aula 311, Palazzina C, L.go S. Leonardo Murialdo 1
Abstract

One of the main innovations introduced by linear logic at its birth is a representation of proofs as graph-like structures called "proof nets", instead of trees as in natural deductions. However, there have been very few attempts to connect these proof nets with mainstream graph theory. In this talk, we will discuss the benefits of such connections:
- Using a relationship between unique perfect matchings and MLL+Mix proof nets first noticed by Retoré, we obtain the best known algorithms for MLL+Mix correctness and sequentialization, and discover some purely graph-theoretical results inspired by linear logic. (Reference for this part: https://arxiv.org/abs/1901.10247 )
- The notion of combinatorial map (already applied to the combinatorics of the lambda-calculus by Bodini-Gardy-Jacquot, Zeilberger-Giorgetti...) allows us to recast Girard's "long trip" criterion in terms of topology of surfaces, and also induces some clarifications in the theory of cyclic linear logic.