DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2026.34

Stabilized Profunctors and Matrix Representation

Authors: Takeshi Tsukada, Kazuyuki Asada, and Kengo Hirata

Published in: LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)

Abstract

The (bi)category of profunctors on groupoids is a categorification of the relational model of linear logic. Its objects are not just sets but rather sets whose elements are equipped with groups encoding their symmetries, and its morphisms carry actions by these symmetries. While detailed information on such symmetries helps with, e.g., adequacy proofs of profunctorial models, it makes operations such as composition more difficult to compute. A way to ease the computation is to transform a profunctor into a matrix. Although the matrix representation is not functorial in general, it is known to behave well for certain subclasses, such as the class of profunctors definable by λ-terms. The mathematical reason behind this phenomenon, however, was not understood. This paper shows that the key is stability. Stability is a classical concept in domain theory, and has been extended to profunctors in Taylor’s work and further developed by Fiore et al. All λ-definable profunctors are known to be stabilized, and we show that the matrix representation behaves well for stabilized profunctors. We prove that the matrix representation defines a functor from stabilized profunctors to matrices that preserves the linear logic structures.

Cite as

Takeshi Tsukada, Kazuyuki Asada, and Kengo Hirata. Stabilized Profunctors and Matrix Representation. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 34:1-34:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{tsukada_et_al:LIPIcs.FSCD.2026.34,
  author =	{Tsukada, Takeshi and Asada, Kazuyuki and Hirata, Kengo},
  title =	{{Stabilized Profunctors and Matrix Representation}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{34:1--34:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-433-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{378},
  editor =	{Pfenning, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.34},
  URN =		{urn:nbn:de:0030-drops-263847},
  doi =		{10.4230/LIPIcs.FSCD.2026.34},
  annote =	{Keywords: Profunctor, weighted relational model, stability}
}

Document

DOI: 10.4230/LIPIcs.LICS.2026.57

Causality in Pure Quantum Computation with Quantum Control

Authors: Kengo Hirata and Takeshi Tsukada

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract

Indefinite causal order is a characteristic phenomenon in quantum computation, with examples including the quantum SWITCH and the OCB process. Not all such processes are believed to be physically realizable: while some implementations of the quantum SWITCH have been proposed, the OCB process is suspected to be unrealizable. This difference in realizability is commonly attributed to constraints imposed by physical causality. This paper studies such a causality issue in a higher-order setting, proposing a typed lambda calculus with quantum control and its categorical semantics. Our calculus extends pure quantum computation with higher-order functions and quantum conditional branching, and it is equipped with a type system based on intuitionistic BV logic to enforce causality. We also present a novel model that is closely related to the Caus construction, by which we prove that some physically-unrealizable processes are not definable in our language.

Cite as

Kengo Hirata and Takeshi Tsukada. Causality in Pure Quantum Computation with Quantum Control. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 57:1-57:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{hirata_et_al:LIPIcs.LICS.2026.57,
  author =	{Hirata, Kengo and Tsukada, Takeshi},
  title =	{{Causality in Pure Quantum Computation with Quantum Control}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{57:1--57:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.57},
  URN =		{urn:nbn:de:0030-drops-268445},
  doi =		{10.4230/LIPIcs.LICS.2026.57},
  annote =	{Keywords: Quantum computing, supermap, categorical model, linear logic, BV logic, programming language, type system}
}

Search Results

Documents authored by Hirata, Kengo

Stabilized Profunctors and Matrix Representation

Abstract

Cite as

Causality in Pure Quantum Computation with Quantum Control

Abstract

Cite as

Thanks for your feedback!

Could not send message