A categorical construction for the computational definition of vector spaces

DOI10.1007/S10485-020-09598-7zbMATH Open1461.03016arXiv1905.01305OpenAlexW3100233597MaRDI QIDQ2024925FDOQ2024925

Octavio Malherbe, Alejandro Díaz-Caro

Publication date: 4 May 2021

Published in: Applied Categorical Structures (Search for Journal in Brave)

Abstract: Lambda-S is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi. One is to forbid duplication of variables, while the other is to consider all lambda-terms as algebraic linear functions. The type system of Lambda-S has a constructor S such that a type A is considered as the base of a vector space while S(A) is its span. Lambda-S can also be seen as a language for the computational manipulation of vector spaces: The vector spaces axioms are given as a rewrite system, describing the computational steps to be performed. In this paper we give an abstract categorical semantics of Lambda-S* (a fragment of Lambda-S), showing that S can be interpreted as the composition of two functors in an adjunction relation between a Cartesian category and an additive symmetric monoidal category. The right adjoint is a forgetful functor U, which is hidden in the language, and plays a central role in the computational reasoning.

Full work available at URL: https://arxiv.org/abs/1905.01305

zbMATH Keywords

categorical semanticsquantum computingalgebraic lambda-calculus

Mathematics Subject Classification ID

Quantum computation (81P68) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40) Categorical semantics of formal languages (18C50) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Monoidal categories, symmetric monoidal categories (18M05)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Linear logic
• Confluence in probabilistic rewriting
• Families parametrized by coalgebras
• The differential lambda-calculus
• Intensional interpretations of functionals of finite type I
• Call-by-value, call-by-name and the vectorial behaviour of the algebraic \lambda-calculus
• The algebraic lambda calculus
• Typing Quantum Superpositions and Measurement
• A concrete categorical semantics of lambda-\(\mathcal{S}\)

Cited In (4)

• A concrete model for a typed linear algebraic lambda calculus
• A new connective in natural deduction, and its application to quantum computing
• A quick overview on the quantum control approach to the lambda calculus
• Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model

Uses Software

• QML

Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• A computational definition of the notion of vectorial space 👍 👎
• Vectorspace categories immersed in directed components 👍 👎
• On a family of vector space categories. 👍 👎
• A category of geometric spaces: Some computational aspects 👍 👎
• Non-linear combinatorial vectorspace categories 👍 👎
• Categorical Vector Space Semantics for Lambek Calculus with a Relevant Modality 👍 👎

This page was built for publication: A categorical construction for the computational definition of vector spaces

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2024925)