Gruppo di Logica e Geometria della Cognizione

Via the Taylor expansion of lambda terms it is possible to provide an innovative proof of the head-normalization theorem for the relational model.
Thanks to this result we can also state in a very natural way the equivalence between the relational model and some intersection type systems.

In the talk, we present the history of Mersenne primes from the ancient Greeks to our days. We show that only strong and long-standing interactions of mathematics, computer science and computer technology made it possible to find Mersenne primes with several millions of digits. The long history divided naturally into shorter or longer epochs; before the Lucas test; the Lucas test with hand calculation; the Lucas test with early electronic computers; the epoch of supercomputers; distributed computation, the industrialisation for the search of Mersenne primes. At the end, I will speculate about the future of this game.

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.

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.

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

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.

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.

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?

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.