Next Formal Methods Seminar (D2 seminar) will take place on January 7th at 1pm in room A008.

Alejandro Díaz Caro (Mocqua) Will give a presentation entitled Sup, Sum, and Scalars: In Linear Logic and in Non-Linear Logic.

Abstract:
In [1], we introduced a new connective, called “sup”, to intuitionistic
propositional logic to model information erasure, non-reversibility, and
non-determinism, as observed in quantum measurement, among other
contexts. This connective features the introduction rule of conjunction
and the elimination rule of disjunction, resulting in a
non-deterministic cut-elimination process. To enrich its proof terms, we
added a sum operator, which allows for recovering the determinism of the
connective. Additionally, since one of our goals was to express quantum
programs, we introduced a scalar product. These rules may occupy the
space between the introduction and elimination of a given connective,
forcing us to include commuting cuts to establish a proper introduction
theorem.
The next step toward transforming this calculus into a quantum calculus
was to adopt a linear logic framework. Thus, in [2], we considered the
full intuitionistic multiplicative-additive linear logic (IMALL). We
proved that, when removing the sup connective, the system–augmented
with sums and scalar multiplication–is linear in the algebraic sense.
Specifically, any term t applied to a linear combination a⋅r+b⋅s is
observationally equivalent to a⋅(tr)+b⋅(ts).
In [3], we provided an abstract characterization of the sup connective
in IMALL, showing that any symmetric monoidal closed category with
biproducts and a monomorphism from the semiring of scalars to the
semiring Hom(I,I) is a suitable model. By leveraging the binary
biproducts, we defined a weighted codiagonal map, which serves as the
core of the sup connective.
Finally, in [4], we considered two non-linear systems: first, with the
sum operator alone as a parallel operator, and second, with the
combination of the sum and scalar operators as an algebraic lambda
calculus. We proposed two categorical models for these calculi. In
particular, we explored the role of disjunction within the calculus,
which has rarely been studied in conjunction with the parallel (or sum)
construct. For the parallel lambda calculus, we employed the category
MagSet, whose objects are magmas and whose morphisms are functions from
the category Set. For the algebraic lambda calculus, we used the
category AMagSSet, whose objects are action magmas, with morphisms
similarly drawn from Set. Our approach diverges from conventional
interpretations, which typically handle disjunctions via coproducts.
Instead, we proposed handling them through a combination of disjoint
unions and Cartesian products.