On the Algebra of Structural Contexts
Résumé
We discuss a general way of defining contexts in linear logic, based on the observation that linear universal algebra can be symmetrized by assigning an additional variable to represent the output of a term. We give two approaches to this, a syntactical one based on a new, reversible notion of term, and an algebraic one based on a simple generalization of typed operads. We relate these to each other and to known examples of logical systems, and show new examples, in particular discussing the relationship between intuitionistic and classical systems. We then present a general framework for extracting deductive system from a given theory of contexts, and prove that all these systems have cut-elimination by the means of a generic argument.
Mots clés
algebraic theories
combinatorial species
cut-elimination
display logic
linear logic
multi-categories
operads
sequent calculus
structural contexts
substructural logics
élimination des coupures
logique linéaire
operades
calcul des séquents
contextes structuraux
logiques sub-structurales
algèbre universelle
universal algebra
théories algébriques
Domaines
Autre [cs.OH]
Loading...