A Categorical Construction for the Computational Definition of Vector Spaces
- PDF / 974,364 Bytes
- 38 Pages / 439.37 x 666.142 pts Page_size
- 65 Downloads / 168 Views
A Categorical Construction for the Computational Definition of Vector Spaces Alejandro Díaz-Caro1,2
· Octavio Malherbe3
Received: 8 May 2019 / Accepted: 30 April 2020 © Springer Nature B.V. 2020
Abstract Lambda-S is an extension to first-order lambda calculus unifying two approaches of noncloning 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. Keywords Quantum computing · Algebraic lambda-calculus · Categorical semantics
Communicated by Thomas Streicher. A. Díaz-Caro has been partially supported by PICT 2015 1208, ECOS-Sud A17C03 QuCa and PEDECIBA. O. Malherbe has been partially supported by MIA CSIC UdelaR.
B
Alejandro Díaz-Caro [email protected] Octavio Malherbe [email protected]
1
Instituto de Ciencias de la Computación. CONICET-Universidad de Buenos Aires, Buenos Aires, Argentina
2
Departamento de Ciencia y Tecnología. Universidad Nacional de Quilmes, Bernal, Buenos Aires, Argentina
3
Departamento de Matemática y Afines, CURE & Instituto de Matemática y Estadística Rafael Laguardia, Facultad de Ingeniería, Universidad de la República, Montevideo, Uruguay
123
A. Díaz-Caro and O. Malherbe
1 Introduction Algebraic lambda calculi aim to embed to the lambda calculus, the notion of vector spaces over programs. This way a linear combination α.v + β.w of programs v and w, for some scalars α and β, is also a program [3]. This kind of construction has two independent origins. The Algebraic Lambda Calculus (ALC for short) [21] has been introduced as a fragment of the Differential Lambda Calculus [13], which is itself originated from Linear Logic [14]. ALC can be seen as the Differential Lambda Calculus without a differential operator. In the ALC the notion of vector spaces is embedded in the calculus with an equational theory, so the axioms of vector spaces, such as α.v + β.v = (α + β).v are seen as equalities between programs. On the other hand, the Linear Algebraic Lambda Calculus (Lineal for short) [2] was meant for quantum computation. The aim of Lineal is to provide a computational definition of vector space and bilinear functions, and so, it defines the axioms of vector spaces as rewrite rules, providing a confluent calculus. This way, an equality such as −v + v + 3.w
Data Loading...
