arXiv subjects

Alessandro Di Giorgio

Publications and source records attributed to Alessandro Di Giorgio.

16 recordsLinked to original sources

arXiv2026

The calculus of neo-Peircean relations

The calculus of relations was introduced by De Morgan and Peirce during the second half of the 19th century, as an extension of Boole's algebra of classes. Later developments on quantification theory by Frege and Peirce himself, paved the way to what is known today as first-order logic, causing the calculus of relations to be long forgotten. This was until 1941, when Tarski raised the question on the existence of a complete axiomatisation for it. This question found only negative answers: there is no finite axiomatisation for the calculus of relations and many of its fragments, as shown later by several no-go theorems. In this paper we show that -- by moving from traditional syntax (cartesian) to a diagrammatic one (monoidal) -- it is possible to have complete axiomatisations for the full calculus. The no-go theorems are circumvented by the fact that our calculus, named the calculus of neo-Peircean relations, is more expressive than the calculus of relations and, actually, as expressive as first-order logic. The axioms are obtained by combining two well known categorical structures: cartesian and linear bicategories.

cs.LO↗

arXiv2026

A Diagrammatic Basis for Computer Programming

Tape diagrams provide a convenient graphical notation for arrows of rig categories, i.e., categories equipped with two monoidal products, $\oplus$ and $\otimes$. In this work, we introduce Kleene-Cartesian rig categories, namely rig categories where $\otimes$ provides a Cartesian bicategory, while $\oplus$ a Kleene bicategory. We show that the associated tape diagrams can conveniently deal with imperative programs and various program logic.

cs.LO↗

arXiv2025

String Diagrams for Closed Symmetric Monoidal Categories

We introduce a graphical language for closed symmetric monoidal categories based on an extension of string diagrams with special bracket wires representing internal homs. These bracket wires make the structure of the internal hom functor explicit, allowing standard morphism wires to interact with them through a well-defined set of graphical rules. We establish the soundness and completeness of the diagrammatic calculus, and illustrate its expressiveness through examples drawn from category theory, logic and programming language semantics.

cs.LO↗

arXiv2025

Parametric Iteration in Resource Theories

Many algorithms are specified with respect to a fixed but unspecified parameter. Examples of this are especially common in cryptography, where protocols often feature a security parameter such as the bit length of a secret key. Our aim is to capture this phenomenon in a more abstract setting. We focus on resource theories -- general calculi of processes with a string diagrammatic syntax -- introducing a general parametric iteration construction. By instantiating this construction within the Markov category of probabilistic Boolean circuits and equipping it with a suitable metric, we are able to capture the notion of negligibility via asymptotic equivalence, in a compositional way. This allows us to use diagrammatic reasoning to prove simple cryptographic theorems -- for instance, proving that guessing a randomly generated key has negligible success.

cs.LO↗

arXiv2025

Tape Diagrams for Monoidal Monads

Tape diagrams provide a graphical representation for arrows of rig categories, namely categories equipped with two monoidal structures, $\oplus$ and $\otimes$, where $\otimes$ distributes over $\oplus$. However, their applicability is limited to categories where $\oplus$ is a biproduct, i.e., both a categorical product and a coproduct. In this work, we extend tape diagrams to deal with Kleisli categories of symmetric monoidal monads, presented by algebraic theories.

cs.LO↗

arXiv2024

A Diagrammatic Algebra for Program Logics

Tape diagrams provide a convenient notation for arrows of rig categories, i.e., categories equipped with two monoidal products, $\oplus$ and $\otimes$, where $\otimes$ distributes over $\oplus $. In this work, we extend tape diagrams with traces over $\oplus$ in order to deal with iteration in imperative programming languages. More precisely, we introduce Kleene-Cartesian bicategories, namely rig categories where the monoidal structure provided by $\otimes$ is a cartesian bicategory, while the one provided by $\oplus$ is what we name a Kleene bicategory. We show that the associated language of tape diagrams is expressive enough to deal with imperative programs and the corresponding laws provide a proof system that is at least as powerful as the one of Hoare logic.

cs.LO↗

arXiv2024

When Lawvere meets Peirce: an equational presentation of boolean hyperdoctrines

Fo-bicategories are a categorification of Peirce's calculus of relations. Notably, their laws provide a proof system for first-order logic that is both purely equational and complete. This paper illustrates a correspondence between fo-bicategories and Lawvere's hyperdoctrines. To streamline our proof, we introduce peircean bicategories, which offer a more succinct characterization of fo-bicategories.

math.CT↗

arXiv2024

Diagrammatic Algebra of First Order Logic

We introduce the calculus of neo-Peircean relations, a string diagrammatic extension of the calculus of binary relations that has the same expressivity as first order logic and comes with a complete axiomatisation. The axioms are obtained by combining two well known categorical structures: cartesian and linear bicategories.

cs.LO↗

arXiv2022

Deconstructing the Calculus of Relations with Tape Diagrams

Rig categories with finite biproducts are categories with two monoidal products, where one is a biproduct and the other distributes over it. In this work we present tape diagrams, a sound and complete diagrammatic language for these categories, that can be intuitively thought as string diagrams of string diagrams. We test the effectiveness of our approach against the positive fragment of Tarski's calculus of relations.

cs.LO↗

arXiv2021

Diagrammatic Polyhedral Algebra

We extend the theory of Interacting Hopf algebras with an order primitive, and give a sound and complete axiomatisation of the prop of polyhedral cones. Next, we axiomatise an affine extension and prove soundness and completeness for the prop of polyhedra.

cs.LO↗

arXiv2016

Lagrangian Decomposition based Multi Agent Model Predictive Control for Electric Vehicles Charging integrating Real Time Pricing

This paper presents a real time distributed control strategy for electric vehicles charging covering both drivers and grid players' needs. Computation of the charging load curve is performed by agents working at the level of each single vehicle, with the information exchanged with grid players being restricted to the chosen load curve and energy price feedback from the market, elaborated according to the charging infrastructure congestion. The distributed control mechanism is based on model predictive control methodology and Lagrangian decomposition of the optimization control problem at its basis. The simulation results show the effectiveness of the proposed distributed approach and the mutual coherence between the computed charging load curves and the resulting energy price over the time.

eess.SY↗

arXiv2016

On the Control of Energy Storage Systems for Electric Vehicles Fast Charging in Service Areas

This paper presents a real time control strategy for energy storage systems integration in electric vehicles fast charging applications combined with generation from intermittent renewable energy sources. A two steps approach taking advantage of the model predictive control methodology is designed on purpose to optimally allocate the reference charging power while managing the priority among the plugged vehicles and then control the storage for efficiently sustaining the charging process. Two different use cases are considered: in the former the charging area is disconnected from the grid, so that the objective is to minimize the deviation of electric vehicles charging power from the nominal value; in the latter the focus is on the point of connection to the grid and the need of mitigating the related power flow. In both cases the fundamental requirement for feasible control system operation is to guarantee stability of the storage's state of charge over the time. Simulation results are provided and discussed in detail, showing the effectiveness of the proposed approach.

eess.SY↗

arXiv2015

Electric Energy Storage Systems integration in Distribution Grids

This paper presents a real time control strategy for dynamically balancing electric demand and supply at local level, in a scenario characterized by a HV/MV substation with the presence of renewable energy sources in the form of photovoltaic generators and an electric energy storage system. The substation is connected to the grid and is powered by an equivalent traditional power plant playing the role of the bulk power system. A Model Predictive Control based approach is proposed, by which the active power setpoints for the traditional power plant and the storage are continually updated over the time, depending on generation costs, storage's state of charge, foreseen demand and production from renewables. The proposed approach is validated on a simulation basis, showing its effectiveness in managing fluctuations of network demand and photovoltaic generation in test and real conditions.

math.OC↗

arXiv2015

Smart Vehicle to Grid Interface Project: Electromobility Management System Architecture and Field Test Results

This paper presents and discusses the electromobility management system developed in the context of the SMARTV2G project, enabling the automatic control of plug-in electric vehicles' (PEVs') charging processes. The paper describes the architecture and the software/hardware components of the electromobility management system. The focus is put in particular on the implementation of a centralized demand side management control algorithm, which allows remote real time control of the charging stations in the field, according to preferences and constraints expressed by all the actors involved (in particular the distribution system operator and the PEV users). The results of the field tests are reported and discussed, highlighting critical issues raised from the field experience.

math.OC↗

arXiv2015

Electric Vehicles Charging Control based on Future Internet Generic Enablers

In this paper a rationale for the deployment of Future Internet based applications in the field of Electric Vehicles (EVs) smart charging is presented. The focus is on the Connected Device Interface (CDI) Generic Enabler (GE) and the Network Information and Controller (NetIC) GE, which are recognized to have a potential impact on the charging control problem and the configuration of communications networks within reconfigurable clusters of charging points. The CDI GE can be used for capturing the driver feedback in terms of Quality of Experience (QoE) in those situations where the charging power is abruptly limited as a consequence of short term grid needs, like the shedding action asked by the Transmission System Operator to the Distribution System Operator aimed at clearing networks contingencies due to the loss of a transmission line or large wind power fluctuations. The NetIC GE can be used when a master Electric Vehicle Supply Equipment (EVSE) hosts the Load Area Controller, responsible for managing simultaneous charging sessions within a given Load Area (LA); the reconfiguration of distribution grid topology results in shift of EVSEs among LAs, then reallocation of slave EVSEs is needed. Involved actors, equipment, communications and processes are identified through the standardized framework provided by the Smart Grid Architecture Model (SGAM).

cs.NI↗

arXiv2013

Optimal Fully Electric Vehicle load balancing with an ADMM algorithm in Smartgrids

In this paper we present a system architecture and a suitable control methodology for the load balancing of Fully Electric Vehicles at Charging Station (CS). Within the proposed architecture, control methodologies allow to adapt Distributed Energy Resources (DER) generation profiles and active loads to ensure economic benefits to each actor. The key aspect is the organization in two levels of control: at local level a Load Area Controller (LAC) optimally calculates the FEVs charging sessions, while at higher level a Macro Load Area Aggregator (MLAA) provides DER with energy production profiles, and LACs with energy withdrawal profiles. Proposed control methodologies involve the solution of a Walrasian market equilibrium and the design of a distributed algorithm.

eess.SY↗