Pith. sign in

REVIEW 1 cited by

Categorical models of computation: partially traced categories and presheaf models of quantum computation

Not yet reviewed by Pith; the record is open.

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1301.5087 v1 pith:3UG67LKC submitted 2013-01-22 math.CT

classification math.CT
keywords categoriestracedpartiallycomputationquantummainbasecategory
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

This dissertation has two main parts. The first part deals with questions relating to Haghverdi and Scott's notion of partially traced categories. The main result is a representation theorem for such categories: we prove that every partially traced category can be faithfully embedded in a totally traced category. Also conversely, every monoidal subcategory of a totally traced category is partially traced, so this characterizes the partially traced categories completely. The main technique we use is based on Freyd's paracategories, along with a partial version of Joyal, Street, and Verity's Int construction. Along the way, we discuss some new examples of partially traced categories, mostly arising in the context of quantum computation. The second part deals with the construction of categorical models of higher-order quantum computation. We construct a concrete semantic model of Selinger and Valiron's quantum lambda calculus, which has been an open problem until now. We do this by considering presheaf categories over appropriate base categories arising from first-order quantum computation. The main technical ingredients are Day's convolution theory and Kelly and Freyd's notion of continuity of functors. We first give an abstract description of the properties required of the base categories for the model construction to work; then exhibit a specific example of base categories satisfying these properties.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Quantalic lambda-calculus and additive disjunction

    cs.LO 2026-08 conditional novelty 6.0 of 10

    Quantalic linear lambda-calculus gains an additive disjunction operator with sound and approximately complete equational reasoning, plus probabilistic and quantum model constructions.

Pith tools