We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Deductive Systems and Coherence for Skew Prounital Closed Categories

Abstract: In this paper, we develop the proof theory of skew prounital closed categories. These are variants of the skew closed categories of Street where the unit is not represented. Skew closed categories in turn are a weakening of the closed categories of Eilenberg and Kelly where no structural law is required to be invertible. The presence of a monoidal structure in these categories is not required. We construct several equivalent presentations of the free skew prounital closed category on a given set of generating objects: a categorical calculus (Hilbert-style system), a cut-free sequent calculus and a natural deduction system corresponding to a variant of planar (= non-commutative linear) typed lambda-calculus. We solve the coherence problem for skew prounital closed categories by showing that the sequent calculus admits focusing and presenting two reduction-free normalization procedures for the natural deduction calculus: normalization by evaluation and hereditary substitutions. Normal natural deduction derivations (beta-eta-long forms) are in one-to-one correspondence with derivations in the focused sequent calculus. Unexpectedly, the free skew prounital closed category on a set satisfies a left-normality condition which makes it lose its skew aspect. This pitfall can be avoided by considering the free skew prounital closed category on a skew multicategory instead. The latter has a presentation as a cut-free sequent calculus for which it is easy to see that the left-normality condition generally fails.
The whole development has been fully formalized in the dependently typed programming language Agda.
Comments: In Proceedings LFMTP 2020, arXiv:2101.02835
Subjects: Logic in Computer Science (cs.LO); Category Theory (math.CT)
Journal reference: EPTCS 332, 2021, pp. 35-53
DOI: 10.4204/EPTCS.332.3
Cite as: arXiv:2101.03809 [cs.LO]
  (or arXiv:2101.03809v1 [cs.LO] for this version)

Submission history

From: EPTCS [view email]
[v1] Mon, 11 Jan 2021 10:51:49 GMT (36kb,D)

Link back to: arXiv, form interface, contact.