2
$\begingroup$

It's well known that the simply-typed lambda calculus corresponds to a cartesian closed category. How would substructural type systems be characterized in category theory?

For example, linear type systems correspond to closed symmetric monoidal categories. But what category-theoretic constructions correspond to affine type systems, ordered type systems, and relevant type systems?

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ Affine type systems correspond to what some would call semicartesian closed monoidal categories. The categorical structure associated with relevant type systems probably has no standard name. I suppose it is a symmetric monoidal closed category with suitable natural transformations implementing duplication. For what concerns "ordered" type systems, I don't know exactly, are you talking about subtyping? $\endgroup$
    – Damiano Mazza
    Jun 6, 2017 at 16:16
  • 2
    $\begingroup$ I don't understand what answer we're suposed to give. An entire research overfiew of various variants of the Curry-Howard correspondence for substructural type theory? That's a bit much. Perhaps this should instead be tagged as a reference-request. $\endgroup$
    – Andrej Bauer
    Jun 7, 2017 at 7:04
  • $\begingroup$ @AndrejBauer Just tagged this as a reference-request. Variants of the Curry-Howard correspondence for substructural type systems are exactly what I'm looking for. Thank you $\endgroup$
    – C. Bednarz
    Jun 7, 2017 at 7:09
  • $\begingroup$ Relevance type systems correspond to relevance monoidal categories. $\endgroup$
    – Mike Shulman
    Jun 9, 2017 at 8:22

1 Answer 1

Reset to default
0
$\begingroup$

Dan Licata, Mitchell Riley, and Mike Shulman have recently proposed a rather general answer to this, in A Fibrational Framework for Substructural and Modal Logics (extended preprint).

This probably isn’t the main answer you want, for several reasons — it’s long and fairly dense, and more significantly, the logics and categorical structures it gives are not the ones you might first hope for, since they (a) must be presented in the style of the general framework, and (b) the categorical structure will directly and ‘naïvely’ mirror the structural rules of the logic, rather than being repackaged into some neater equivalent form.

However, the references cited in that article form an excellent entry point to the literature on categorical semantics of substructural logics, and should help to find the more direct answers you really want.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ Looking through the references now and it seems like they're just what I need. Thank you! $\endgroup$
    – C. Bednarz
    Jun 7, 2017 at 7:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.