Graded Adjoint Logic
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.