The mix rule is an inference rule that can be added to linear logic. The most common mix rule is the binary mix rule
(or ), but to be unbiased one should also consider the nullary mix rule
(or ), which together are equivalent to , and imply -ary mix rules for all .
Ordinary linear logic has semantics in polycategories, linearly distributive categories, and star-autonomous categories, depending on how many connectives are assumed. A linearly distributive category satisfies the binary mix rule if there is a morphism satisfying a certain coherence axiom. It additionally satisfies the nullary mix rule if this morphism is an isomorphism. In CS97 these are called mix categories and isomix categories respectively.
Last revised on September 8, 2018 at 23:28:10. See the history of this page for a list of all contributions to it.