Graded Adjoint Logic

Harley Eades III

Augusta University




Abstract: There are two new complementary forms of controlling the structural rules in substructural logics: graded types and adjoint logic. The former annotate types (or formulas) with a usage annotation called grades that control how the structural rules of weakening and contraction are allowed to be used. These annotations are often the elements of a partially-ordered semiring where a weakened formula is annotated with the additive identity of the semiring and the addition is used to combine usage annotations during contraction. Thus, in graded types the structural rules are always present, but controlled via grades. Compare this to adjoint logic which annotates formulas with modes that indicate which structural are allowed to be used. For example, one mode may allow weakening but not contraction, and another mode may allow both. Thus, instead of controlling how the structural rules are used modes control which structural rules are present. An interesting question is how can we combine these two views together? That is, we want a type system that allows us to control which structural rules are present and how we are allowed to use them.

In this talk I will introduce Graded Adjoint Logic both syntactically and semantically. First, I will show how Benton's LNL Logic/Model can be generalized to the graded setting. Then a notion of graded mode is introduced and used to define the final system of Graded Adjoint Logic. I will also discuss the semantics of the logic which is based on a new categorical model in Grade-Indexed Multicategories.

Joint work with Tori Vollmer and Dominic Orchard.