Gruppo di Logica e Geometria della Cognizione

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

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

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

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

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.

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.

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.

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.

A cornerstone of the theory of lambda-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.