Warning: Table './church/sessions' is marked as crashed and last (automatic?) repair failed query: SELECT sid FROM sessions WHERE sid = '9ah1qlloj4972a6683pm3tujm2' in /var/www/church/includes/database.mysql.inc on line 121
Gruppo di Logica e Geometria della Cognizione

 

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

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.


Periodic structure of graph dynamical systems on maxterm and minterm Boolean functions.

Speaker:
Jose C. Valverde (Università di Castiglia-La Mancia)
Quando:
07/12/2017 - 11:00
Dove:
Dipartimento di Matematica e Fisica, L.go S. Leonardo Murialdo 1, Aula 211
Abstract

The emergence of the concepts of cellular automata (CA) (Wolfram, 1983, 1984, 1986) and Boolean (BN) network (Kauffman, 1969), between the end of the 60s and early 80s, for the formalization of computational processes and genetic regulation, respectively, was a first step in the development of modeling of evolutionary phenomena using networks. This type of modeling has been useful to solve various problems in other Sciences such as Chemistry (see Kier & Seybold, 2009; Kier, Seybold & Cheng 2005; Scalise & Schulman, 2015), Physics (see Chopard & Droz, 1998), Biology (see Deutsch & Dormann, 2004, Toroczkai & Güçlü, 2007), Ecology (see Dieckman, Law & Metz, 2000; Hofbauer & Sigmund, 2003; Hogeweg, 1988), even of Social Sciences like Psychology or Sociology (see Abraham, 2015; Kempe, Kleminberg & Tardos, 2005).
This new paradigm of modeling has evolved in recent years, giving rise to the concept of graph dynamical system (GDS), which generalizes the previous ones, since it contemplates that the relationships among elements of the system can be arbitrary. That is, the graph representing the relations among elements of the system, called dependency graph, could be arbitrary. In this generalization, the smallest units of aggregation of the phenomenon are called nodes (or vertices), in relation to their membership in the graph, relieving the term of cells in a CA and entities in a BN.
In this talk, we discuss some of the advances in the study of the periodic structure of a GDS when the evolution operator is a maxterm or minterm Boolean function.


Una interpretazione di CCS nella ludica

Speaker:
Stefano Del Vecchio (Università Roma Tre - Université Paris Nord)
Quando:
24/11/2017 - 11:00
Dove:
Dipartimento di Matematica e Fisica, Palazzina C, Aula 311
Abstract

Starting from works aimed at extending the Curry-Howard correspondence to process calculi through linear logic, we give another Curry-Howard counterpart for Milner's Calculus of Communicating Systems (CCS) by taking Ludics as the target system. Indeed interaction, Ludics' dynamic, allows to fully represent both the non-determinism and non-confluence of the calculus. CCS processes are interpreted into carefully defined behaviours of Ludics using a new construction, called directed behaviour, that allows controlled interaction paths by using pruned designs. Execution of processes is characterized as interaction on behaviours, by implicitly representing the causal order and conflict relation of event structures. As a direct consequence, we are also able to interpret deadlocked processes, and identify deadlock-free ones.



Warning: Can't find file: 'watchdog' (errno: 2) query: INSERT INTO watchdog (uid, type, message, severity, link, location, referer, hostname, timestamp) VALUES (0, 'php', 'Table './church/sessions' is marked as crashed and last (automatic?) repair failed\nquery: SELECT sid FROM sessions WHERE sid = '9ah1qlloj4972a6683pm3tujm2' in /var/www/church/includes/database.mysql.inc on line 121.', 2, '', 'http://logica.uniroma3.it/node?page=2', '', '98.80.143.34', 1728494427) in /var/www/church/includes/database.mysql.inc on line 121