A categorical construction for the computational definition of vector spaces

DOI10.1007/S10485-020-09598-7MaRDI QIDQ2024925zbMATH OpenOpenAlexFDO

Authors Alejandro Díaz-Caro, Octavio Malherbe

Publication date 4 May 2021

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

Full work available at URL https://arxiv.org/abs/1905.01305, http://hdl.handle.net/11336/141616

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)

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.

Recommendations

• A computational definition of the notion of vectorial space
• scientific article; zbMATH DE number 858448
• scientific article; zbMATH DE number 3977210
• A category of geometric spaces: Some computational aspects
• Non-linear combinatorial vectorspace categories
• scientific article; zbMATH DE number 463967
• Vectorspace categories immersed in directed components
• Categorical Vector Space Semantics for Lambek Calculus with a Relevant Modality
• scientific article; zbMATH DE number 2068347
• On a family of vector space categories.

Cites work

• scientific article; zbMATH DE number 6712184 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 3522182 (Why is no real title available?)
• scientific article; zbMATH DE number 1216133 (Why is no real title available?)
• scientific article; zbMATH DE number 2079022 (Why is no real title available?)
• scientific article; zbMATH DE number 5273418 (Why is no real title available?)
• A concrete categorical semantics of lambda-\(\mathcal{S}\)
• Call-by-value, call-by-name and the vectorial behaviour of the algebraic \(\lambda \)-calculus
• Confluence in probabilistic rewriting
• Families parametrized by coalgebras
• Intensional interpretations of functionals of finite type I
• Linear logic
• The algebraic lambda calculus
• The differential lambda-calculus
• Typing Quantum Superpositions and Measurement

Cited in

(5)

• A concrete model for a typed linear algebraic lambda calculus
• A concrete categorical semantics of lambda-\(\mathcal{S}\)
• 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

Describes a project that uses

Uses Software

• QML

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)