Università degli Studi di Padova

“Graded Doctrines and Linear Equality”

Tuesday 18th May, 5pm - Zoom - Fabio Pasquali (University of Genova)


Equality in First Order Logic is an equivalence relation which is substitutive. A formula of the form t=t’ expresses to which extent the term t is equal to the term t’ or also, with an eye on computer science, to which extent the program t is equivalent to the program t’. Recent studies on equivalences between programs pointed out that it is preferable to compare programs using distances rather than equivalence relations. One might guess that a syntactic calculus behind this point of view can be achieved rephrasing the rules of equality from First Order Logic to Linear Logic, i.e. endowing predicate Linear Logic by a binary relation with rules that force it to be a substitutive distance. But this calculus has the undesirable consequence that equality collapse to an equivalence relation, i.e. equality can be duplicated an arbitrary number of times.

In this talk we introduce a calculus for equality in predicate Linear Logic enriched by graded modalities. The use of graded modalities allows us to have equality as a truly linear predicate.

The language that we employ is the categorical one of Lawvere doctrines. We introduce graded linear doctrines as the basic mathematical tool with which we develop the study of linear equality. We also describe a universal construction that generates models of linear equality starting from any graded linear doctrine (the construction is a generalisation of the one presented in [1]).

This is a join work with Francesco Dagnino (Genova).

[1] Elementary quotient completion. M.E. Maietti, G. Rosolini. Theory and Application of Categories 27(17):445–463, 2013